<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 8 Nov 2014, at 09:12, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">Hi Mario,<br><br>Thanks for your feedback on the proposal. I have given a lot of<br>thought to your email, and in reply let me explain a little about my<br>vision for the OpenTheory project.<br><br>Firstly, I see the goal of the project as evolving a set of standards<br>for proofs and theories to capture the needs of people wanting to<br>exchange theories between theorem prover implementations. So I'm not<br>too worried about maintaining backward compatibility if there's a<br>measurable improvement, just like the situation with removing the<br>unnecessary free variables from the theorems produced by defineTypeOp.<br><br>Rob's suggestion of a version command makes incompatible changes in<br>articles easy to deal with, and I will commit to ensuring that the<br>opentheory tool will support all released versions of OpenTheory<br>standards. My hope is that people developing tools will always choose<br>the latest version of the standards, and not have to worry about<br>processing earlier versions (perhaps using the opentheory tool to<br>upgrade earlier versions if necessary).</blockquote><br></div><div>I am looking forward to seeing how this works out when I finish</div><div>upgrading my reader/writer for ProofPower to version 6. Will</div><div>it be possible to do the conversion with the opentheory tool</div><div>as a filter (so a script to import an article can just convert it</div><div>to its preferred version on the fly)?</div><div><br></div><div><blockquote type="cite"><br>So in the context of an evolving set of standards I see the pragma<br>article command as a laboratory for testing out new ideas in different<br>article readers, with the idea that once new features are tested they<br>can be standardized as new commands that every reader must implement<br>in the same way. For example, if most readers support a debug pragma<br>then I see no problem with creating a debug command in future versions<br>of the article standard that all readers must respect. In this role of<br>a test laboratory that different readers process in different ways, it<br>seems that the opentheory tool has no choice but to discard pragma<br>commands when producing articles.<br><br>In the light of the above, and the requests I have heard to include<br>theorem metadata in articles, I still see it as a good idea to propose<br>an extra argument to the thm article command that all readers must<br>process in the same way. I'd be interested in hearing your thoughts<br>(and the thoughts of others on the list) on whether the specific<br>proposal captures specific theorem metadata needs, or indeed whether<br>there is enough added value to justify making a change at all.<br><br></blockquote><div><br></div><div>I agree with the idea that readers must implement each command in</div><div>the same way, but I take this as being relative to the representation</div><div>chosen for the OpenTheory virtual machine in a particular reader.</div><div>If you are going to say that the extra argument to the thm command</div><div>must be processed in the same way, then you are going to have</div><div>to extend the OpenTheory virtual machine to include the theorem</div><div>metadata, so that you can define that processing. Were you planning</div><div>to do that?</div><div><br></div><div>If you weren’t planning to change the virtual machine, then</div><div>this seems to me like a good candidate for a standardised</div><div>pragma as Mario suggests. First that means there is no</div><div>implementation overhead for anyone maintaining a reader</div><div>and who doesn’t want to use the metadata. Secondly, the</div><div>opentheory tool could duck the question of how to</div><div>combine multiple metadata: it could just include all the</div><div>relevant pragmas. Finally it seems intuitively right. since</div><div>readers that do use the metadata are likely to use it in</div><div>different ways, so it is a pragmatic matter, aside from</div><div>the core semantics of OpenTheory.</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div><div><br></div></div></div></body></html>