diff --git a/doc/editors/new-entry-checkin.md b/doc/editors/new-entry-checkin.md --- a/doc/editors/new-entry-checkin.md +++ b/doc/editors/new-entry-checkin.md @@ -1,100 +1,99 @@ New Submissions (editors only) ------------------------------ **Mercurial Setup** As editor you have at least two working copies of the repository: current release branch and development version. - Start by making a directory `~/afp` where the different branches will go. - To set up the release version, in that directory do (fill in 20XX) hg clone ssh://hg@foss.heptapod.net/isa-afp/afp-20XX release - for development hg clone ssh://hg@foss.heptapod.net/isa-afp/afp-devel devel You might need to set up ssh keys on Heptapod for this to work. This can be done under "[Settings/SSH Keys][keys]". New submissions, changes to the web site and to admin scripts go into afp/release. About once a week, one of the editors should merge afp-release into afp-devel, ideally making sure after the merge that the entry works in the devel version, although that sometimes may be too much and be left for the authors to fix themselves. Maintenance and changes on existing submissions all occur in afp/devel and go properly public with the next Isabelle release (they are only available as (public) development tar.gz's) [keys]: https://foss.heptapod.net/profile/keys **New Submissions** Everything happens in the release branch `afp/release`. 1. unpack tar file and move new entry to `afp/release/thys` 2. make sure there is a `thys/entryname/ROOT` file and add `entryname` to `thys/ROOTS`. For the former see the template in `thys/Example-Submission/ROOT`. In particular the entry should be in chapter AFP, and group `(AFP)`, i.e. chapter AFP session foo (AFP) = bar + -3. to check, run in `afp/release/thys` +3. to check, run in `afp/release/thys` ../admin/testall -c (be sure to have `ISABELLE_RELEASES` set to the path where Isabelle releases are kept, e.g. `/home/proj/isabelle/`) -4. check license headers: if the authors want the code released under +4. check license headers: if the authors want the code released under LGPL instead of BSD, each file should mention "License: LGPL" in the header. We only accept the BSD 3-Clause and LPGPL version 2.1 licenses as they are printed in `thys/LICENSE` and `thys/LICENSE.LGPL`. -5. `hg add` and `hg commit` the new submission -6. Enter data for author/abstract/index/etc in the file - `metadata/metadata`. Make sure that your editor uses UTF-8 encoding - for this file to preserve special characters. If the entry uses a - new topic or category, add it to metadata/topics (make sure there is - an empty line at the end of the file). -7. Generate the new web site by running `../admin/sitegen` . -8. Use `hg st` and `hg diff` to make sure the generated html makes +5. `hg add` and `hg commit` the new submission +6. Enter data for author/abstract/index/etc in the `metadata` dir. + Make sure that your editor uses UTF-8 encoding to preserve special + characters. If the entry uses a new topic or category, add it to + metadata/topics. +7. Generate the new web site by running `../admin/sitegen` . +8. Use `hg st` and `hg diff` to make sure the generated html makes sense. The diff should be small and concern the new entry only. 9. `hg add` and `hg commit` the web site updates. 10. finally, when you are happy with everything, `hg push` all changes to Heptapod. The publish script will refuse to publish if the changes aren't pushed. 11. to publish the changes to the web, run ../admin/publish This will check out the Isabelle202X (=release) version of the archive from Heptapod, will run the session `name` to generate HTML, produce a `.tar.gz` for the archive and for the entry, and will update the web pages on the server. The script will ask before it copies, so you can check locally if everything is as you want it. 12. That's it. Changes should show up at **New submission in devel** Although it is a condition of submission that the entry works with the current stable Isabelle version, occasionally it happens that a submission does not work with the stable version and cannot be backported, but is important/good enough to include anyway. In this case, we can't release the submission on the main web site yet, but we can add it to the development version of the archive, such that it is at least available to those who are working with the current Isabelle development snapshot. The check-in procedure is the same as for a normal release entry, apart from the fact that everything happens in the devel instead of release directory and that the last step (publish) is omitted. The authors of the entry should be notified that the entry will only show up on the front page when the next Isabelle version is released. diff --git a/doc/editors/web.md b/doc/editors/web.md --- a/doc/editors/web.md +++ b/doc/editors/web.md @@ -1,25 +1,24 @@ Web site & Site generator ------------------------- -The web site is generated by a set of Python scripts. As input, they take +The site generation can be run directly with `isabelle afp_site_gen`. +Note that you need to have installed the AFP as an Isabelle component +(`isabelle components -u `) and resolved all component dependencies +(`isabelle components -a`). +To run the site generation without any arguments, you can invoke the script: -- the metadata of the entries (as specified in the `metadata` folder), -- dependencies between entries (as generated by the `afp_dependencies` tool), - and -- static templates (in `metadata/templates`) + ./admin/sitegen The output will be written to the `web` folder, which is supposed to be committed into the repository. It can be inspected by opening any of the contained HTML files in the browser. -The script can be invoked without any arguments: - - ./admin/sitegen - Changing static content, e.g. the submission guidelines, works by editing the -appropriate template file (see above) and re-running the `sitegen` script. +appropriate markdown file in `admin/site/content` and re-running the `sitegen` script. +The `afp_site_gen` tool also has a development mode which makes changes in content +immediately visible. To publish website changes without publishing a new entry, you can use the `publish` script with the `-` argument: ./admin/publish - diff --git a/doc/maintenance.md b/doc/maintenance.md --- a/doc/maintenance.md +++ b/doc/maintenance.md @@ -1,85 +1,90 @@ Maintaining an Entry in the AFP ------------------------------- To maintain an entry, you must have write access to the mercurial repository 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 +- 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 +- 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 + mechanisms), and download the required components with + `isabelle components -a`. 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 +- 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 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 +- 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. + change log in the file `afp-devel/metadata/entries/.toml` by adding + an `--
= "note"` entry to the `[history]` section of 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/metadata/metadata`: + editing the file `afp-devel/metadata/entries/.toml`: -- 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. +- To switch on: make sure your email address is in your author entry in + `afp-devel/metadata/authors.toml` and add it to the `notify` section as + ` = `, hg commit, and hg push the file. + Do not change meta data of other entries. + 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.