hosting request for the AFP from bitbucket
Description of the projects to be hosted
- Project Name: AFP (Archive of Formal Proofs)
- Project URL: https://www.isa-afp.org and https://bitbucket.org/isa-afp/
- Project Maintainers: Gerwin Klein (lsf37 here and on bitbucket), Tobias Nipkow, Lawrence C Paulson, René Thieman, Manuel Eberl
- Project License: BSD 3-clause and LGPL 2.0
The AFP is an open source collection of formal proofs in the Isabelle/HOL theorem prover (also open source), that is continually maintained and developed by the Isabelle community.
The repository structure is one main development repository afp-devel
, and a current "release" repository that accepts new proof entries for review for the currently released Isabelle version (currently afp-2019
). It would be nice to also import earlier release repositories afp-20?? from bitbucket so they can still be referred to and browsed.
Please explain here why they meet our current criteria.
All details are in the invitation announcement
To recapitulate, these are:
Main criteria
-
Free / Open Source -
main development repositories -
agreement to acknowledge where appropriate the help provided by Octobus and Clever Cloud by hosting on foss.heptapod.net
All of these are fulfilled. The AFP has been open source and community-based from the start and we'd be happy to acknowledge sponsorship.
Priority Criteria
-
currently hosted on Bitbucket -
officially released
All of these are fulfilled. Isabelle development makes use of mercurial extensively, and the bitbucket move away from hg is going to be painful for the community around contributed proofs.
Post approval maintainer task list:
See README for explanations.
-
Heptapod / Bitbucket accounts link -
Reviewing Heptapod workflow
Post import maintainer task list:
-
Clone the project afresh from foss.heptapod.net. -
Check that the repository looks good: branches are as expected in the clone and the web interface, with no wild
branches unless there are known multiple heads. -
Check that issues are imported, and notably that all open issues are there. Watch for attachments etc. -
Check that Pull Requests are imported, and in particular take a close look at the resulting open Merge Requests - they should be backed by a topic. Make sure you can navigate these in the fresh clone. -
Check that against foss.heptapod.net, hg outgoing
andhg incoming
from a prior clone are as expected -
Add the Octobus and Clever cloud acknowledgement at the selected place.