[opentheory-users] my first package

[Ramana Kumar]

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...
>