[opentheory-users] theory file format specification

[Joe Leslie-Hurd]

Hi Ramana,

> Another question/comment: why must there be a unique author (as
> opposed to, say, at least one)?

The unique author is really the "corresponding author" for the theory
package: when packages are uploaded to the repo the system uses the
author email to confirm the upload (and then uses it again if someone
else uploads a later version of the package to check the earlier
author has given permission).

If there are multiple authors of a package I'd suggest adding
co-author fields to the theory file as follows:

author: Euclid <euclid at alexandria.gr>
co-author: Alfred Tarski <tarski at berkeley.edu>
co-author: Bertrand Russell <russell at cam.ac.uk>

> Also, the intent of the "license" information is a little unclear (and
> why is it mandatory?).

I consider it important that someone wanting to use a theory package
should know how it is licensed. I don't want to get in a situation
where someone uses a theory in some application only to find out later
it has some restrictive license that prevents it being used in that
way.

To ensure that people can freely use theory packages without worrying
about this kind of thing, the gilith repo currently only accepts
packages with the MIT or HOL Light licenses:

http://www.gilith.com/research/opentheory/licenses/

These two licenses play nicely with each other, place very few
restrictions on uses of the package, and protect the author by
disclaiming any warranty.

> Which copyrighted work is the license intended
> for: the package file itself, or one or more of the files it refers
> to, or something else?

The copyrighted work is the theory package and the files it contains.
If the package refers to other packages then they are separate
copyrighted works.

> (Presumably for this purpose the author is
> supposed to represent the copyright holder...)

Yes, although if there are co-author: fields as above then the author
and co-authors are the copyright holders.

Cheers,

Joe