Thanks & DECLARE

[dsyme]

Thank you for this site. I once had a dream of hunting down exotic archaic LCF theorem provers. So I'm impressed to see it already done.

If it would be welcome, at some point I'd like to donate the source code for DECLARE, a theorem prover described in my thesis here

https://www.repository.cam.ac.uk/handle/1810/252967

[kohlhase]

Don, this donation would certainly be welcome. I would just make a repository and give you admin. Then you would make a pull request on https://github.com/theoremprover-museum/theoremprover-museum.github.io/blob/master/_data/provers.yml introducing declare and pointing to the repository, then the site is updated automatically. Is this what you want to do?

[dsyme]

Yes that would be fine, thanks. It might take me ages as I may port it all to F# and give it a new gui.

[kohlhase]

Before you do this, you should just commit the current code to the repository as a historical artefact. And then you can continue development. Actually, if the repository at cambridge can be converted to git, it would be best to do that (there should be standard tools) and then commit the full history as a historical artefact.

[kohlhase]

I just made a theoremprover-museum repository for you: https://github.com/theoremprover-museum/declare/ and gave you admin access. Please fill out the details in https://github.com/theoremprover-museum/theoremprover-museum.github.io/blob/master/_data/provers.yml (by analogy).