[opentheory-users] package versions

[Joe Hurd]

Hi Ramana,

Thanks for the quick response - it's great to get feedback on a
feature while it's still fresh in my mind.

> It seems like the check that the required theories are actually
> installed isn't done right away, so first the article is processed
> (possibly taking a long time) before failing because of the requires
> line?

Good point - I just released a version that checks that some version
of the required theories are installed, before beginning the
installation of the theory file.

> Also, after this happened to me and I had to install base, I then ran
> into this problem:
>
> FATAL ERROR: opentheory failed:
> Error: package cl-0.5 is already staged for installation
> package install from theory file failed
>
> Even though cl does not appear in the list of installed packages. Now
> I suppose I have to manually remove the "staged" installation by rm
> -rf $OPENTHEORY/staging/cl-0.5 ?

You could do this, but it's better to use the

opentheory cleanup

command.

> On the topic of staging, after I produce an article by proof-logging,
> would it be a good idea to immediately run
>  opentheory info --article -o foo.art foo.art
> to clean it up, or would that be redundant given that I might
> eventually create a .thy file for it and process it somewhere along
> the way with the tool?

Articles always get cleaned up as part of the theory installation
procedure, but when exporting theories from HOL Light I do an initial
clean-up as part of the step to rename type operators and constants
into the OpenTheory standard namespace.

> I would rather hope that parameterized theories would become so common
> as to be considered "the norm"... but I think your current default
> treatment of "requires" is fine for now.

I thought a little more about this, and have a new plan:

1. I added special code to ignore the 3 standard axioms of higher
order logic, so theories that are supposed to be at the base of the
theory hierarchy (such as base) can just say "requires: empty" and
they won't get warnings about standard axioms.

2. For parametric theories, I think the theory developer should be
responsible for constructing a "witness theory" that shows that it is
possible to satisfy the input parameters. So, for example, for the
"modular" parametric theory in the OpenTheory repo, the author should
make a trivial "modular-witness" theory that defines a non-zero
"modular" constant. Then modular-witness can be added to the requires
list, and all the assumptions are satisfiable. As a side-benefit, the
theory developer can be confident that the theory parameters are
satisfiable.

> I uploaded cl-0.5 just now with a requirement for base. Now it only
> has 30 unsatisfied assumptions left... some (but not all) I think
> should be in base, or rather, I need to think of a way to make my
> articles depend on base only (+ maybe some compatibility packages)
> without touching the HOL4 script files they are logged from.

Sure - this is what I do exporting from HOL Light. I see that you've
already renamed some of your constant names to the OpenTheory standard
namespace - if you would like to further standardize your theory I
have a few suggestions:

1. add confluent (and possibly other general constants) into the
Relation namespace

2. rename your example namespace to something like "CombinatoryLogic"
instead of "cl"

3. make sure that all your constant and type operator names are in
camel case and begin with a lower case letter

> But it seems like the "requires:" tags are being ignored in various
> places. Like on the repo's package summary, or if I ask the tool:
>  opentheory info --summary cl-0.5
> it still lists things like |- T as one of the assumptions (but base
> provides this).
> It seems like the only time I got the list of the 30 actually
> uncovered assumptions was when I issued the "install" command on my
> .thy file.

I'm deliberately keeping the new "requires" functionality contained
for now, but I like your suggestion of it being used to produce the
opentheory info --summary output. I'll implement this functionality.

> I think it would be better if the requires tags made a difference to
> the package summary...

In the opentheory info --summary case, agreed. But I'm reluctant to
use the "requires" information in the HTML "package document" on the
repo, because it would need to be updated every time a new version of
a required theory got added, and also because theories are supposed to
be useful in other contexts than the one the author used. However, I'm
willing to update this opinion if people don't actually do this in
practice.

Cheers,

Joe