25 February 2010

Online Prover Repositories

Most, if not all, of the interactive theorem-proving systems used today are open source, meaning that their source-code is freely available. Not only can you read the source code yourself, but you can also write your own systems based on that code if you wish. In addition, some make their development repositories available for browsing. John Harrison recently announced that HOL Light now has its Subversion repository being hosted on Google Code, so I thought I’d provide links to those systems' repositories I know of.

  • Coq is on Subversion, at INRIA, at svn://scm.gforge.inria.fr/svn/coq/

  • HOL4 is on Subversion, at Sourceforge, at https://hol.svn.sourceforge.net/svnroot/hol/HOL

    HOL4’s repository is also available via git, at github, at git://github.com/mn200/HOL.git

  • HOL Light is on Subversion, at Google Code, at http://hol-light.googlecode.com/svn/trunk/

  • Isabelle is on Mercurial, at Munich, at http://isabelle.in.tum.de/repos/isabelle

Note that all of those URLs above are for use by the respective version-control systems’ initialisation and cloning commands; they will not necessarily work as targets for web-browsers.