Yes I think the theory package *-file lines allow any kind of file to be attached to a package. The only reason to have an extra hol4 article file is tags like Abbrev and NUMERAL. Everything else, as I mentioned before, can be done separately from the article. So, to summarise what's required on the HOL4 side to package an existing HOL4 theory: 1. Log the article without translating any constants to Unwanted.id (i.e. don't mark anything as tags); maybe just put constants that won't be in a standard namespace into the HOL4 namespace. 2. In the theory package file, name the article from step 1 as the hol4-theory-file. Probably post-process it with the opentheory tool too. 3. Create a new copy of the article file from step 1, and rename the tags (I'm thinking just a search+replace taking "HOL4.Abbrev" -> "Unwanted.id", etc. might be enough, right?), then postprocess with opentheory to remove them. 4. Name the article from step 3 as the main article in the package. 5. For any additional information (theorem names, exported rewrites, etc., which should probably also be recorded in step 1) add appropriate extra hol4-something-files to the package. Unfortunately, that still doesn't solve the problem when a tag shows up not fully applied (like in a point-free term). <div class="gmail_quote">On Sat, Jan 14, 2012 at 8:32 PM, 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">This would be my preference (thus my "associated files if necessary"). I don't know if everything HOL4-ish could necessarily be encoded in an "art" file though. Presumably, files mentioned in the package could contain other stuff. Michael <div class="HOEnZb"><div class="h5"> On 15/01/2012, at 0:19, Joe Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: > Hi Ramana, > > My preference would be that the theorem prover interface handles as > much as possible of the standardization during theory export and then > localization during theory import (the inverse operation). But I can > see that there might be some HOL4 specific theory information that > can't be reconstructed on theory import. > > I wonder if you could achieve your goal by exporting an extra file > hol4.art declared in the package theory file > > hol4-theory-file: hol4.art > > that contained a version of the proof article file for the theory with > the HOL4 specific theory information you want to preserve? > > Cheers, > > Joe > >> 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: >>> >>> 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. >>> >>> >>> 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 >>> >>> 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/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a> >>>>> >>>> >>>> _______________________________________________ >>>> opentheory-users mailing list >>>> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>>> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a> >>> >>> >>> >>> _______________________________________________ >>> opentheory-users mailing list >>> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a> >>> >> >> >> _______________________________________________ >> opentheory-users mailing list >> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a> >> > > _______________________________________________ > opentheory-users mailing list > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> > <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a> _______________________________________________ opentheory-users mailing list <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a> </div></div></blockquote></div>