[opentheory-users] the Unwanted namespace

[Michael Norrish]

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

On 15/01/2012, at 0:19, Joe Hurd <joe at gilith.com> 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
>> <Michael.Norrish at nicta.com.au> 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
>>>> <michael.norrish at nicta.com.au> wrote:
>>>>> On 07/12/2011, at 20:01, Ramana Kumar <ramana.kumar at gmail.com> 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
>>>>> opentheory-users at gilith.com
>>>>> http://www.gilith.com/opentheory/mailing-list
>>>>> 
>>>> 
>>>> _______________________________________________
>>>> opentheory-users mailing list
>>>> opentheory-users at gilith.com
>>>> http://www.gilith.com/opentheory/mailing-list
>>> 
>>> 
>>> 
>>> _______________________________________________
>>> opentheory-users mailing list
>>> opentheory-users at gilith.com
>>> http://www.gilith.com/opentheory/mailing-list
>>> 
>> 
>> 
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>> 
> 
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list