search

theoremprover-museum / theoremprover-museum.github.io

https://theoremprover-museum.github.io
GNU General Public License v3.0
52 stars 7 forks source link

Update SAD and add Naproche(-SAD), Why3, Elfe, Egal #28

Closed adelon closed 3 years ago

adelon commented 3 years ago

Finally got around to making a pull request! Please let me know in case some of the submitted entries need fixing.

I obtained a copy of Egal from http://grid01.ciirc.cvut.cz/~chad/twosettheories.tgz, which was linked in the paper “A tale of two set theories”. I think this is the most recent version of Egal.

kohlhase commented 3 years ago

Thanks for the extensions. I am wondering why the original Naproche does not have a repository link. Does the source exist? If so, would you be willing to make a repository under the museum group (I would supply that) and commit the source there?

kohlhase commented 3 years ago

I obtained a copy of Egal from http://grid01.ciirc.cvut.cz/~chad/twosettheories.tgz, which was linked in the paper “A tale of two set theories”. I think this is the most recent version of Egal.

Does Egal have a license? Could we just make a repository for that on github? Would you be willing to chase this up and contact Chad to ask for allowancer? I know that this is difficult, but it may be worth it if the license does not expressly allow it.

adelon commented 3 years ago

Thanks for the extensions. I am wondering why the original Naproche does not have a repository link. Does the source exist? If so, would you be willing to make a repository under the museum group (I would supply that) and commit the source there?

I’ll talk with Peter about it! This may be a bit awkward and take a while: either the copyright belongs to the University of Bonn or to 11 different developers. As far as I know, the source was never released under an open license before.

Does Egal have a license? Could we just make a repository for that on github? Would you be willing to chase this up and contact Chad to ask for allowancer? I know that this is difficult, but it may be worth it if the license does not expressly allow it.

The egal directory of the *.tgz contains an MIT license and the README.txt explicitly mentions that the prover is open source, so I think we’re in the clear. I’ll try to contact Chad Brown anyways, just to let him know!

kohlhase commented 3 years ago

I’ll talk with Peter about it!

thanks for taking responsibility. You will probably find that now that Naproche is of mostly historic value, things may become easier.

kohlhase commented 3 years ago

prover is open source

then wen should go ahead and make a repository. I will make one and give you admin rights.

kohlhase commented 3 years ago

I have given you admin access to the new repos egal. Then you can put the sources there.

kohlhase commented 3 years ago

Once you have made progress with Naproche, we can do the same there.