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

Ramana Kumar ramana at member.fsf.org
Mon Aug 5 17:14:48 UTC 2013

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

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

> 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>

More information about the opentheory-users mailing list