diff --git a/doc/maintenance.md b/doc/maintenance.md --- a/doc/maintenance.md +++ b/doc/maintenance.md @@ -1,86 +1,85 @@ Maintaining an Entry in the AFP ------------------------------- To maintain an entry, you must have write access to the mercurial repository -of the archive at [Heptapod][hetpa]. To get access, [sign up at +of the archive at [Heptapod][hepta]. To get access, [sign up at Heptapod][hepta], and ask one of the [editors][editors] to add you to the AFP project. [hepta]: https://foss.heptapod.net [editors]: http://isa-afp.org/about.html#editors **Setup:** Check out the archive from the mercurial repository with: hg clone ssh://hg@foss.heptapod.net/isa-afp/afp-devel The command above will create a directory `afp-devel` where theories and additional files are located. You can register an ssh key for your account at Heptapod under "[Settings/SSH keys][keys]" from the avatar icon on the top right of the Heptapod interface. [keys]: https://foss.heptapod.net/profile/keys **Maintenance:** Maintaining an entry means making sure that this entry works with the current Isabelle development version. Maintainers are not supposed to check in and push new entries. New entries must be reviewed and formally accepted. They are created on the release branch by the editors. Depending on the type of the entry, you might want to work in close lock step with Isabelle development, i.e. fix the entry immediately each time it breaks, or loosely, i.e. only shortly before a new Isabelle release. The former is useful for libraries and base entries that are used by others, the latter is Ok for larger developments and leaf entries. Small changes might be done by the Isabelle development team for you as the change is introduced to Isabelle (don't be surprised when your entry changes slightly over time). You will be notified when an Isabelle release nears and your entry is broken. You can also choose to receive an automatic email notification each time your entry breaks (see below). **Technicalities:** - To get the current Isabelle development version, use hg clone http://isabelle.in.tum.de/repos/isabelle to clone the hg repository. See the README file inside for further instructions. - Set up your AFP repository as a component by adding `init_component "/path_to/afp-devel"` to your `~/.isabelle/etc/settings` (or use any other of the component adding mechanisms). You need this to get access to the AFP settings and the `afp_build` tool. - To check if entry `x` works, execute `isabelle afp_build x`. This assumes that the command `isabelle` would start up the current Isabelle development version. - To test all entries, run `isabelle afp_build -A`. (Running the script with `-?` will show options and usage information) - The changes you make to the mercurial repository will not show up on the AFP web pages immediately. This only happens when a new version of the archive is released (usually together with Isabelle). Please contact one of the editors if you feel there is something that should be made available immediately. The changes will show up with about 24h delay in the web development snapshot of the AFP. - If you make a change that is more than maintenance and that you think may be interesting to users of your entry, please add a manual change log in the file `afp-devel/metadata/metadata` by adding an `[extra-history]` section to your entry. If possible and sensible, this log should link to the relevant hg change set(s). See existing change logs like the one for JinjaThreads for examples. **Email Notification:** You can receive an automatic email notification if entry `x` breaks by -editing the file `afp-devel/thys/x/config`: +editing the file `afp-devel/metadata/metadata`: -- To switch on: add your email address to `NOTIFY`, hg commit, and hg - push the file. `NOTIFY` is a space separated list. If the entry is - marked as `FREQUENT`, the test will run daily. -- To switch off: remove your email address from `NOTIFY` and hg +- To switch on: find the your entry by searching for its short name, add your email address to `notify = `, hg commit, and hg push the file. Do not change meta data of other entries. + `notify` is a comma-separated list of email addresses. If the + entry is not in group `slow` or `very_slow` in the `ROOT` file, the test will run on every push to the repository. +- To switch off: remove your email address from `notify` and hg commit + push the file. - diff --git a/doc/the-archive.md b/doc/the-archive.md --- a/doc/the-archive.md +++ b/doc/the-archive.md @@ -1,96 +1,93 @@ How the Archive Works --------------------- Submission is by email to afp-submit@in.tum.de which is distributed to the archive committee (currently GK, TN, LCP, RT, and ME). One member will assume responsibility. This includes refereeing the submission, communicating with the authors, and installing it in the archive. Once it has been installed, it will be announced on isabelle-users. **Contents of submission:** 1. Title, authors, abstract, keywords in plain text (maybe html). 2. A short name, will become the directory name. 3. URL or email address of author to display on the web page 4. A tar file with the theory files, ROOT file, and README or document/. The theories should work with the current release. 5. A notice whether submission is LGPL **Submission procedure:** 1. Referee for content and form 2. Check if submission works with current released version of Isabelle. 3. Make sure submitter agrees to BSD or LGPL and potentially maintenance. -4. Check submission into repository (as release and development, we do - this, not the submitters) +4. Check submission into repository (as release and development, the editors do this, not the submitters) 5. Make available on web page 6. Give out maintenance access to submitter on development version 7. Announce on isabelle-users **The archive:** Will initially contain an unstructured collection of submissions. For each submission there is a page with title, authors, abstract, keywords, tar.file, and link to the generated html-files for -browsing. If it takes off, we can have fun imposing some structure on -it. But right from the beginning it will be encouraged and possible to -build on other contributions in the archive. The current released -archive should work with the current released Isabelle version. For -later: older archive versions should remain accessible (but maybe not on -the main page). +browsing. It is encouraged and possible to build on other contributions +in the archive. The current released archive should work with the +current released Isabelle version. For later: older archive versions +should remain accessible (but maybe not on the main page). **Roles:** - PC / archive admins (TN, GK, LCP, RT, ME, more) - responsibility: refereeing and initial setup of submissions, releases - access: everything - submitters (everybody) - responsibility: new submissions, become maintainer if accepted - access: email only - maintainers (former submitters, Isabelle team) - responsibility: keep development branch up to date with Isabelle - access: repository read/write - user (everybody) - responsibility: use archive - access: download via web page, anonymous hg read only of devel version available **Maintenance:** Usually only on development version of archive (in mercurial default branch). Released version of existing submissions should be stable. **Maintenance responsibility:** Mixed. Simple fixes by the Isabelle team, anything else by the maintainer of the contribution. The editors will give the maintainers advanced warning of a new release (after feature freeze) so they have time to update their contributions. - there should be an automated build. Important libraries nightly, larger developments less often (weekly?). Maintainers should be able to opt in to get email when Isabelle development version breaks archive development version. - there should be a simple build script so we can test if something breaks when we change Isabelle (before we check in) **Sync between Isabelle and archive:** - there is a current release version of the archive (eg. for Isabelle2003, it lives from release of Isabelle2003 until Isabelle2004) - the current release version of the archive will be updated multiple times in its life: for each submission and each time a maintainer fixes a broken submission (broken e.g. because they did not make the Isabelle release deadline). - submissions that do not work at release time are dropped from the archive (only temporarily until fixed, but things that don't work are never visible on the web page). - there is a development version of the archive that is not visible on the web (or only in the form of a development snapshot). It is in the repository and this is where the maintainers work. It becomes the release version when a new Isabelle version is released. How closely it is in sync with the Isabelle development version is the choice of each maintainer in a spectrum from very loose (only fix archive submission after Isabelle feature freeze) to very close (always fix archive submission after each Isabelle change). Very close should be the case for widely used base libraries, very loose is ok for standalone developments.