Updating Entries



The Archive of Formal Proofs is an online resource and therefore more dynamic than a normal scientific journal. Existing entries can and do evolve and can also be updated significantly by their authors.

This conflicts with the purpose of archiving and preserving entries as they have been submitted and with the purpose of providing a clear and simple interface to readers.

The AFP deals with this by synchronizing such updates with Isabelle releases:

  • The entries released and visible on the main site are always working with the most recent stable Isabelle version and do not change.
  • In the background, the archive maintainers evolve all entries to be up to date with the current Isabelle development version. Authors can contribute changes to this version which is available as a bitbucket mercurial repository or as tar.gz package on the download page.
  • When a new Isabelle version is released, the above mentioned development version of AFP is frozen and turns into the main version displayed on the front page. Older versions (including the original submission) of all entries are archived and remain accessible.

If you are an author

The above means that if you are an author and would like to provide a new, better version of your AFP entry, you can do so.

To achieve this, you should base your changes on the mercurial development version of your AFP entry and test it against the current Isabelle development version.

If you would like to get write access to your entry in the mercurial repository or if you need assistance, please contact the editors.