<div class="gmail_quote">If we store terms in articles as-is and then clean tags up later (or not), then I imagine Opentheory repos would offer different versions of packages: either the raw one that might include prover-specific constants for some prover, or the cleaned up one with all tags removed. If you're lucky enough to be using the prover the package was made on, you get the specific version, otherwise you get the generic one. If tags are inferable, though, then there could be more options, tailoring a package to the prover you want to use it on. Does this sound right? On Mon, Dec 12, 2011 at 2:13 AM, Michael Norrish <<a href="mailto:Michael.Norrish@nicta.com.au">Michael.Norrish@nicta.com.au</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I think it’s clear that there’s no end of cruft that systems might like to put into theory files. Even the “names” field you mention below may vary from system to system. Given that, we need some generic way of stuffing arbitrary, well-delimited strings into theory files. I’d probably prefer these strings to be inline, but it could also be done with associated files if necessary. I like the default being the storage of everything. </blockquote><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> Another example of a tag-like thing is the way we use K T x to store arbitrary terms x in a theory so that the term can be referred to by the LaTeX machinery we have. Michael <div class="HOEnZb"><div class="h5"> On 08/12/11 21:32, Ramana Kumar wrote: > Can we make a comprehensive list of the kind of stuff we might want to > store in a theory package? > I suspect there will be different recovery methods suitable for > different kinds of data, and looking at the requirements will help see > if and how opentheory might have to be modified or extended. > > - Tag-free theorems, definitions, low-level proofs. > : already handled by article format > > - theory name and description and dependencies > : already handled by theory package format > > - NUMERAL tags > : reconstructible on reading? > > - Abbrev tags > > - Other tags? (Such as?) > : An alternative approach might be to store terms in an article as-is > (with tags) and then have different processing options for cleaning up > an article like do-nothing, remove all tags, remove all of the > following tags, or even possibly introduce tags for a specific prover > (if they are inferable). > > - theorem names > : could be stored in a separate file mapping names to statements? > > - automatic rewrites > : could be stored in a separate file containing a list of theorems? > > - parsing and printing rules, and overloads > : also could be in a separate file? > > - derived rules and other functionality associated with a theory > - tactics, provers/decision procedures > - syntax manipulation functions > - what else? > : again, could be in a separate file of code, possibly using > opentheory article format to interface with the required > constants/theorems in the theory? > > - what else? > > At the moment it looks like almost everything could be handled by > extra files that would be mentioned in a theory package but wouldn't > interfere with article files in their current form. Only tag constants > are a problem because they change the terms the article is dealing > with. > > Are there examples of tags that are definitely not reconstructible if > they are thrown away during cleanup? > > > On Thu, Dec 8, 2011 at 9:50 AM, Michael Norrish > <<a href="mailto:michael.norrish@nicta.com.au">michael.norrish@nicta.com.au</a>> wrote: >> On 07/12/2011, at 20:01, Ramana Kumar <<a href="mailto:ramana.kumar@gmail.com">ramana.kumar@gmail.com</a>> wrote: >> >> >> It would be worth thinking about how to do all that with opentheory. >> I wouldn't want to compromise the goal of storing prover-independent >> theories without a good reason, though... >> >> >> My concern is that the resulting system might forget things that can't be >> recovered. Then it will never be usable as a theory storage mechanism. Is >> it possible to create a faithful representation of what's there that does >> support getting back exactly what was put in, and to *then* work on >> forgetting stuff that doesn't belong in theories meant for sharing with >> other systems? >> >> Michael >> >> _______________________________________________ >> opentheory-users mailing list >> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >> > > _______________________________________________ > opentheory-users mailing list > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> > <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> </div></div> _______________________________________________ opentheory-users mailing list <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> </blockquote></div>