<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Mon, Mar 10, 2014 at 12:04 PM, Rob Arthan <span dir="ltr"><<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div><div>1) Even though you never, ever, ever want to change it again, allow for the possibility by adding a new command “version” that pops a number off the stack. The number tells the virtual machine what version of the format the input file conforms to. In the absence of a “version” command, the default is 5 (i.e., the version before the “version” command was introduced).</div>
</div></div></blockquote><div><br></div><div>I second this request! I believe Michael Norrish made a similar request earlier - oh, actually it was in a private email.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div style="word-wrap:break-word"><div><div></div><div>2) Have a new command “diag” that is identical with “pop” as far as the virtual machine semantics is concerned but can be used in an implementation of the virtual machine to trigger some kind of diagnostic activity, like printing a report on the state of the virtual machine.</div>
<div><br></div><div>I implemented “diag” in the ProofPower reader and writer and I don’t believe I would have been able to get the writer working without it. It also gives a simple way of adding commentary to an article (you put the comment as a string followed by the diag command). Another reason for wanting it is that I think the article format has a potential use to do some useful application-specific things, e.g., I have clients who are interested in porting between a subset of Z in ProofPower and HOL4. “diag" would be helpful to give some application-specific hints to the reader, e.g., to tell it the name to use when it saves a theorem, without preventing the articles being compatible with other systems.</div>
</div></div></blockquote><div><br></div><div>I also agree this would be useful. This has been discussed before: <a href="http://www.gilith.com/opentheory/mailing-list/2011-October/000167.html">http://www.gilith.com/opentheory/mailing-list/2011-October/000167.html</a>.<br>
</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div>
<div><div><blockquote type="cite"><div dir="ltr">
<div></div><div>I would consider changing the OpenTheory logical kernel to support it, particularly if HOL4 or ProofPower incorporated it as the primitive constant definition mechanism, but I'd be interested to hear what John has to say about it.</div>
</div></blockquote><div><br></div></div><div>John, Ramana, Scott Owens and I talked about this a few months ago. There was general agreement to adopt the new constant definition mechanism once someone had confirmed my informal proof of correctness with a formal proof. Ramana has done that now. It is certainly only a matter of time before I implement it in ProofPower. It would be nice to be able to extend my OpenTheory reader/writer to handle it at the same time. </div>
</div></div></div></blockquote><div><br></div><div>Well, I have proved something about it, but I'm not sure it is as strong as what your informal proof said (which was conservativity) ;) Nevertheless I expect to prove that soon.<br>
</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div><div>
<div></div><div>Over to John and Ramana for the plans for HOL Light and ProofPower.</div></div></div></div></blockquote><div><br></div><div>I have implemented the revised new_specification for HOL4 and plan to integrate it with the master development branch as soon as it is supported by OpenTheory. I don't want to do it before then because that would break HOL4's OpenTheory exporter (since I replaced new_definition with the new rule for specification, which has no OpenTheory analogue to export to as yet).<br>
</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div><div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div>
<div><br></div></div></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>
<br></blockquote></div><br></div></div>