[opentheory-users] my first package

Ramana Kumar ramana.kumar at gmail.com
Fri Sep 16 14:21:22 UTC 2011


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



More information about the opentheory-users mailing list