<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Thu, Aug 1, 2013 at 11:45 PM, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br>


<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Rob,<br>
<div><br>
> <a href="http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light" target="_blank">http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light</a><br>
><br>
> That's very useful. Are there any analogous instructions for exporting from<br>
> HOL4?<br>
<br>
</div>Ramana: you're the expert on this. If you put together a few notes<br>
I'll gladly add them as a new FAQ.<br></blockquote><div><br></div><div>Under the assumption that some information is better than none, even if it's not complete...<br></div><div> here goes:<br></div><div><br>If you want to export a HOL4 theory as an OpenTheory article, you must build HOL4 with the logging kernel.<br>


To do that, pass --otknl to bin/build when you build your installation of HOL4.<br><br></div><div>Then to export a theory, use the commands documented in src/opentheory/logging/Logging.sig within your theory's script file.<br>


Alternatively, pass the --ot flag to Holmake when you build your theory.<br>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.)<br>


</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Cheers,<br>
<br>
Joe<br>
<div><div><br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</div></div></blockquote></div><br></div></div>