<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Joe,<div><br></div><div><div><div>On 24 Mar 2014, at 05:07, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">Hi Rob,<div><br></div><div class="gmail_extra"><div class="gmail_quote"><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; position: static; z-index: auto;">
<div style="word-wrap:break-word"><div><div class=""><blockquote type="cite"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><div>The above command takes about 45 seconds to complete on my machine and the resulting thm.art is 6Mb in size.</div>
</div></div></div></blockquote><br></div></div><div>This looks like it will be useful when you have sorted out the glitches in the package names.</div></div></blockquote></div></div></div></blockquote><div><br></div>In the mean time I carried on processing the leaf package articles one by one. I succeeded in getting the whole thing in with out any new axioms. Initially, because the only definition of something like Set.Fold I had to hand was quite a bit different from the one in the repo, I did a devious trick whereby I included the articles that define Set.Fold and Set.size, and then used the new pragma feature to arrange to run a script just after processing those articles that did the proofs that equate the imported Set.size to the native ProofPower size function.</div><div><br><blockquote type="cite"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><div><br></div><div>Over the weekend I made a new release of the standard theory library</div>
<div><br></div><div><a href="http://opentheory.gilith.com/?pkg=base-1.158">http://opentheory.gilith.com/?pkg=base-1.158</a><br></div><div><br></div><div>so this command now works as intended to extract the "pure theorem" content.</div>
</div></div></div></blockquote><br></div><div>Many thanks for that. I have now defined a set fold operation like the one in the repo and I can import the whole base package conservatively without any devious tricks in one go using the article file that your perl magic generates.</div><div><br></div><div>I have just one outstanding concern: there are no theorems in the sum package and only one in the real package (and the only operators it uses are <= and sup. There don’t seem to be any uses of real or sum in the other packages in the repo, so I haven’t really been able to test that I have got the mappings right for these packages. Any suggestions would be welcome.</div><div><br></div><div>I am trying with some success to load the other packages in the repo. In each case, I constructed an article for each package XYZ in the 35 package other than those included in the base package with the command:</div><div><br></div><div> opentheory info —article -o XYZ.art XYZ.</div><div><br></div><div>The package modular seems to expect a constant called Number.Modular.modulus to be defined, but nothing defines it, so modular won’t load. The package word seems to expect a constant called “Data.Word.width” but nothing defines it. byte will load, but the word10, word12 and word16 packages won’t, apparently because they are trying to redefine a constant called Number.Modular.equivalent.</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div><br></div></body></html>