[opentheory-users] my first package

[Joe Hurd]

Hi Ramana,

Congratulations on uploading your first theory!

I should explain that the theory import mechanism is used to compose
theories, so in cl-0.2 your theory file declared a theory that was
essentially (base + cl-0.1). The OpenTheory toolset currently doesn't
have much support for checking that the assumptions of one theory are
satisfied by the theorems of another, so I sometimes use a theory like
(base + X) as a "test theory" to see what assumptions are not covered
by base (they show up as axioms), but X is a much more useful theory
than (base + X) for others to plug into their own theory compositions.

As an aside, I'm working on a better way to check that theory
assumptions are provable than creating test theories.

Cheers,

Joe

On Sat, Sep 17, 2011 at 1:43 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> I uploaded a new version
> (http://opentheory.gilith.com/opentheory/packages/cl-0.2/cl-0.2.html)
> where the only change is it now imports the base-1.2 package.
> This had some unexpected consequences. My intention was just to remove
> some of the assumptions.
> (Unfortunately not all the assumptions that should be base-provable
> are actually exports of base, so I didn't hope to remove them all.)
> But more surprisingly, opentheory now thinks that my theory is
> defining constants in the Data and Number namespaces.
> (My article only explicitly defines things in the
> combinatoryLogicExample namespace.)
> So all my assumptions have turned into axioms (and I get a warning
> about using 30 axioms!).
> Did I set the import up wrong? Should I not be importing base directly?
>
> On Fri, Sep 16, 2011 at 3:21 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>>> Yes indeed - the gilith repo is open for business
>>>
>>> http://opentheory.gilith.com/
>>>
>>> Make a theory file for your article, and use the opentheory tool to
>>> first install it locally and then upload it to the gilith repo.
>>
>> Uploaded! The summary is here
>> http://opentheory.gilith.com/opentheory/packages/cl-0.1/cl-0.1.html
>> The upload process thus seems to work pretty well.
>> There are a boatload of assumptions, many of which I should probably
>> be satisfying from the base package...
>> I'm going to try to iron out as many issues as we feel necessary on
>> this example package, both on the logging (HOL4) end and on the final
>> product (i.e. the package summary) with Michael, and then we might try
>> creating and uploading a package for something more interesting...
>> To that end, does anyone have comments on the summary as it stands?
>> Those input constants in the "HOL4" namespace are a bit of a worry for
>> anyone else who'd want to use the package...
>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>