<div dir="ltr"><div><div><div><div>I think I'm starting to see the philosophical distinction that Rob is trying to make. The main body of commands in the current spec all change the state of the OT virtual machine in some way, with the only exception being the "pragma" command, which by contrast is required *not* to change anything which is tracked by the virtual machine. That is, you are not allowed to define a pragma that puts something on the stack, because then the machine wouldn't operate correctly if you took the command out or used a reader that didn't respect that pragma. The idea is simply to make this division remain true in later versions of the standard.<br><br></div>Thus, "debug" can never be made an official command, because unless standard out is made a part of the virtual machine, it will always be a no-op with respect to the state variables which *are* in the virtual machine specification. Similarly,  "thmName" can only be made an official command if the exported theorem list in the virtual machine state contains name information.<br><br></div>In this case, it seems that the best way to incorporate "metadata" the way you are trying to do would involve a new type annotated_thm, which contains a thm object and a map of name -> object entries. The virtual machine assumption list would still be a list of thm, but the theorem list would be a list of annotated_thm, and your two-argument "thm" command would package the theorem and metadata together and appendthe resulting annotated_thm object to the theorem list.<br><br></div>This way, it becomes mandatory to respect the metadata of a theorem in order to have correct semantics, so by the above-mentioned philosophy it would have to be an "official" command and not a pragma. Under the current model of the virtual machine, any metadata would have to be tracked outside the machine itself, which falls under the behavior of a pragma.<br><br>One more remark: this is not a concern for article readers, but what should an article merger do if the theorem is mentioned with the same metadata key and different values? Your merging algorithm only works if the metadata is for different keys or is the same in both theorem objects.<br><br></div>Mario<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Nov 8, 2014 at 7:24 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>
<span class=""><br>
> I am looking forward to seeing how this works out when I finish<br>
> upgrading my reader/writer for ProofPower to version 6.  Will<br>
> it be possible to do the conversion with the opentheory tool<br>
> as a filter (so a script to import an article can just convert it<br>
> to its preferred version on the fly)?<br>
<br>
</span>Indeed, this is already supported. This command reads an article (of<br>
any version) from stdin and writes an equivalent article on stdout<br>
using version 6:<br>
<br>
opentheory info --article --output-version 6 article:-<br>
<span class=""><br>
> If you are going to say that the extra argument to the thm command<br>
> must be processed in the same way, then you are going to have<br>
> to extend the OpenTheory virtual machine to include the theorem<br>
> metadata, so that you can define that processing. Were you planning<br>
> to do that?<br>
<br>
</span>No, I wasn't: my intention was that the theorem meta-data would be<br>
interpreted in a reader-dependent way. The proposal was merely a<br>
standard format for representing meta-data as finite maps represented<br>
by nested lists of names, not processing it.<br>
<span class=""><br>
> If you weren't planning to change the virtual machine, then<br>
> this seems to me like a good candidate for a standardised<br>
> pragma as Mario suggests.<br>
<br>
</span>It would certainly be possible to specify theorem meta-data using<br>
pragmas, and perhaps this is after all the best way to do it.<br>
<br>
However, in the spirit of yesterday's unsolicited philosophy lecture,<br>
I would like to take a stand against "standardized pragmas". Once a<br>
particular pragma has demonstrated its usefulness, my favoured<br>
approach would be to define a new command in the next version of the<br>
article spec standardizing its behaviour, rather than adding it to a<br>
set of standardized pragmas. This is what I meant when I said I saw<br>
pragmas as an experimental laboratory for new commands.<br>
<br>
Given this approach, there is no standardized behaviour for pragmas,<br>
and so the opentheory tool does not have the information to maintain<br>
them in articles it processes. Consider maintaining a "debug" pragma<br>
during processing that compresses an article by merging equivalent<br>
objects, or maintaining a "thmName" pragma during processing that<br>
reorders the exported theorems.<br>
<br>
My theorem meta-data proposal was an attempt to standardize the<br>
behaviour of thmName as a new command (i.e., the existing thm command<br>
with an extra argument) so that the opentheory tool could maintain the<br>
information during processing, but this discussion is persuading me<br>
that the benefit of the change may not be worth its cost.<br>
<br>
Cheers,<br>
<br>
Joe<br>
<div class="HOEnZb"><div class="h5"><br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">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>