We don’t track logical dependencies. Rather, we record what theories have been
loaded. This loading is “irreversible”, so using the default setup will force
you to have all those theories as ancestors.
Both the command-line --holstate= and Holmakefile HOLHEAP= methods seem fine to
me. Using the Holmakefile is probably easier (as it is a “set and forget”
method).
Michael
On 23/10/17, 09:18, "Mario Castelán Castro" <marioxcc...@yandex.com> wrote:
On 22/10/17 13:04, Konrad Slind wrote:
> Some of these are support for other proof infrastructure, but the main
> theories give you booleans, products, sums, options, numbers, lists,
> and sets. This is a useful basis on which to begin most formalizations.
Thanks. I thought “export_theory” computed the actual dependencies, as
opposed to using all loaded theories indiscriminately.
> […] Then you will have to explicitly load in all the needed tools and
theories.
> For use of Holmake, I am pretty sure there is an option to support
> hol.bare, but I am not sure what it is.
There is the “--holstate” command line option of Holmake and the special
variable HOLHEAP in a Holmakefile which can be used to employ the bare
heap. But I do not know what is the preferred method.
Regards.
--
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
