[opentheory-users] Problems with the hol light Open Theory support

[Ramana Kumar]

On Thu, Aug 1, 2013 at 11:45 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Rob,
>
> > http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light
> >
> > That's very useful. Are there any analogous instructions for exporting
> from
> > HOL4?
>
> Ramana: you're the expert on this. If you put together a few notes
> I'll gladly add them as a new FAQ.
>

Under the assumption that some information is better than none, even if
it's not complete...
 here goes:

If you want to export a HOL4 theory as an OpenTheory article, you must
build HOL4 with the logging kernel.
To do that, pass --otknl to bin/build when you build your installation of
HOL4.

Then to export a theory, use the commands documented in
src/opentheory/logging/Logging.sig within your theory's script file.
Alternatively, pass the --ot flag to Holmake when you build your theory.
As long as your theory depends on bossLib, the --ot flag will replace the
new_theory and export_theory procedures with versions that log an article
(with the same name of the theory) and store every saved theorem in it.
(Thus you can log an article for a theory without modifying its script
file.)


>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20130805/07dd95e2/attachment.html>