<div dir="ltr">After sending this last email, I noticed that the bool-def theory block was accidentally included in the thm.thy file, please ignore that theory block.<div><br></div><div>Cheers,</div><div><br></div><div>Joe</div>
</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Mar 20, 2014 at 10:55 AM, 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"><div dir="ltr">Hi Rob,<div><br></div><div class="gmail_extra"><div class="gmail_quote"><div class=""><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div style="word-wrap:break-word"><div>I am now trying to follow this procedure and am having one or two problems.</div><div><br></div><div>The packages natural-numeral and natural-dest seem to be exceptions to the rule that all the definition live in packages with names of the form XYZ-def.</div>
</div></blockquote><div><br></div></div><div>That's a bug, I will fix this in the standard theory library.</div><div class=""><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div style="word-wrap:break-word"><div>The packages don’t seem to come out in dependency order. E.g., the first few leaf packages in the natural package come out like this:</div><div><br></div><div>natural-add-def-1.18<br>
natural-add-sub-def-1.3<br>natural-add-sub-thm-1.3<br>natural-add-thm-1.47<br>natural-def-1.23<br><br></div><div>But the definition of addition in natural-add-def depends on suc from natural-def.</div></div></blockquote>
<div>
<br></div></div><div>They seem to be in alphabetical order (the default), did you give the --dependency-order argument:</div><div class=""><div><blockquote type="cite" style="color:rgb(80,0,80);font-family:arial,sans-serif;font-size:12.800000190734863px">
<div dir="ltr">opentheory list --dependency-order '(Identity - IncludedBy) (Includes* base)</div></blockquote></div></div><div>If so then there's a bug in your version of opentheory: it works on the latest version (opentheory 1.2 (release 20131211)).</div>
<div class="">
<div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div style="word-wrap:break-word"><div>When you say “the remaining theory packages in the list can be converted to an article using opentheory info —article”, do you mean that I can create a single article for them all? If so how do I do it? (opentheory info seem only to support a single INPUT.)</div>
</div></blockquote><div><br></div></div><div>There are a few options here:</div><div><br></div><div>1. In ProofPower read in all the leaf article files one by one.</div><div><br></div><div>2. Create a theory file thm.thy of the form</div>
<div><br></div><div>bool-def {</div><div> package: bool-def-1.10<br></div><div>}</div><div><br></div><div><div>axiom-choice {</div><div> package: axiom-choice-1.7</div><div>}</div><div><br></div><div>axiom-extensionality {</div>
<div> import: axiom-choice</div><div> package: axiom-extensionality-1.8</div><div>}</div><div><br></div><div>bool-int {</div><div> import: axiom-choice</div><div> import: axiom-extensionality</div><div> package: bool-int-1.17</div>
<div>}</div></div><div><br></div><div>...repeat for each leaf theory...</div><div><br></div><div>main {</div><div><div> import: axiom-choice</div><div> import: axiom-extensionality</div><div> import: bool-int</div></div>
<div> ...<br></div><div>}</div><div><br></div><div>and then run</div><div><br></div><div>opentheory info --article -o thm.art thm.thy</div><div><br></div><div>3. Here's an ugly line of perl that does the whole thing in one go:</div>
<div><br></div><div>opentheory list --dependency-order '(Identity - IncludedBy) (Includes* base)' | grep -v -- '-def-[0-9.]\+$' | perl -ne 'BEGIN { $b = "{\n"; } chomp; $_ =~ /^(.*)-[0-9.]+$/; print "$1 $b package: $_\n}\n\n"; $b .= " import: $1\n"; END { print "main $b}\n" }' | opentheory info --article -o thm.art theory:-<br>
</div><div><br></div><div>Note this relies on being able to distinguish 'definition' leaf theories by the -def suffix, which as you point out is not the case in the current standard theory library, but that bug will soon be fixed.</div>
<div><br></div><div>The above command takes about 45 seconds to complete on my machine and the resulting thm.art is 6Mb in size.</div><div><br></div><div>Cheers,</div><div><br></div><div>Joe</div><div><br></div><div><br>
</div>
<div><br></div></div></div></div>
</blockquote></div><br></div>