more robust: defer error in sessions structure to build process;
Important notes on Mercurial repository access for Isabelle===========================================================Quick start in 30min--------------------1a. Linux and Mac OS X: ensure that Mercurial is installed (see also https://www.mercurial-scm.org)1b. Windows: ensure that Cygwin64 with curl and Mercurial is installed (see also https://www.cygwin.com)2. Clone repository (bash shell commands): hg clone https://isabelle.in.tum.de/repos/isabelle cd isabelle ./bin/isabelle components -I ./bin/isabelle components -a ./bin/isabelle jedit -l HOL ./bin/isabelle build -b HOL #optional: build session image manually3. Update repository (bash shell commands): cd isabelle hg pull -u ./bin/isabelle components -a ./bin/isabelle jedit -l HOL4. Access documentation (bash shell commands): ./bin/isabelle build_doc -a ./bin/isabelle doc systemIntroduction------------Mercurial https://www.mercurial-scm.org belongs to source codemanagement systems that follow the so-called paradigm of "distributedversion control". This means plain versioning without the legacy ofSVN and the extra complexity of GIT. See alsohttps://www.mercurial-scm.org/learnMercurial offers some flexibility in organizing the flow of changes,both between individual developers and designated pull/push areas thatare shared with others. This additional freedom demands additionalresponsibility to maintain a certain development process that fits toa particular project.Regular Mercurial operations are strictly monotonic, where changesettransactions are only added, but never deleted or mutated. There arespecial tools to manipulate repositories via non-monotonic actions(such as "rollback" or "strip"), but recovering from gross mistakesthat have escaped into the public can be hard and embarrassing. It ismuch easier to inspect and amend changesets routinely before pushing.The effect of the critical "pull" / "push" operations can be tested ina dry run via "incoming" / "outgoing". The "fetch" extension includesuseful sanity checks beyond raw "pull" / "update" / "merge", althoughit has lost popularity in recent years. Most other operations arelocal to the user's repository clone. This gives some freedom forexperimentation without affecting anybody else.Mercurial provides nice web presentation of incoming changes with adigest of log entries; this also includes RSS/Atom news feeds. Thereare add-on history browsers such as "hg view" and TortoiseHg. Unlikethe default web view, some of these tools help to inspect the semanticcontent of non-trivial merge nodes.Initial configuration---------------------The main Isabelle repository can be cloned like this: hg clone https://isabelle.in.tum.de/repos/isabelleThis will create a local directory "isabelle", unless an alternativename is specified. The full repository meta-data and history ofchanges is in isabelle/.hg; local configuration for this clone can beadded to isabelle/.hg/hgrc, but note that hgrc files are never copiedby another clone operation.There is also $HOME/.hgrc for per-user Mercurial configuration. Theinitial configuration requires at least an entry to identify yourselfas follows: [ui] username = ABCIsabelle contributors are free to choose either a short "login name"(for accounts at TU Munich) or a "full name" -- with or without mailaddress. It is important to stick to this choice once and for all.The machine default that Mercurial produces for unspecified[ui]username is not appropriate.Such configuration can be given in $HOME/.hgrc (for each homedirectory on each machine) or in .hg/hgrc (for each repository clone).Here are some further examples for hgrc. This is how to providedefault options for common commands: [defaults] log = -l 10This is how to configure some extension, which is called "graphlog"and provides the "glog" command: [extensions] hgext.graphlog =Shared pull/push access-----------------------The entry point https://isabelle.in.tum.de/repos/isabelle is worldreadable, both via plain web browsing and the hg client as describedabove. Anybody can produce a clone, change it locally, and then useregular mechanisms of Mercurial to report changes upstream, say viamail to someone with write access to that file space. It is alsoquite easy to publish changed clones again on the web, using thead-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scriptsthat are included in the Mercurial distribution, and send a "pullrequest" to someone else.The downstream/upstream mode of operation is quite common in thedistributed version control community, and works well for occasionalchanges produced by anybody out there. Of course, upstreammaintainers need to review and moderate changes being proposed, beforepushing anything onto the official Isabelle repository at TUM. Directpushes are also reviewed routinely in a post-hoc fashion; everybodyhooked on the main repository is called to keep an eye on incomingchanges. In any case, changesets need to be understandable, both atthe time of writing and many years later.Push access to the Isabelle repository requires an account at TUM,with properly configured ssh to isabelle-server.in.tum.de. You alsoneed to be a member of the "isabelle" Unix group.Sharing a locally modified clone then works as follows, using youruser name instead of "wenzelm": hg out ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelleIn fact, the "out" or "outgoing" command performs only a dry run: itdisplays the changesets that would get published. An actual "push",with a lasting effect on the Isabelle repository, works like this: hg push ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelleDefault paths for push and pull can be configured inisabelle/.hg/hgrc, for example: [paths] default = ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelleNow "hg pull" or "hg push" will use that shared file space, unless adifferent URL is specified explicitly.When cloning a repository, the default path is set to the initialsource URL. So we could have cloned via that ssh URL in the firstplace, to get exactly to the same point: hg clone ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelleSimple merges-------------The main idea of Mercurial is to let individual users produceindependent branches of development first, but merge with othersfrequently. The basic hg merge operation is more general thanrequired for the mode of operation with a shared pull/push area. The"fetch" extension accommodates this case nicely, automating trivialmerges and requiring manual intervention for actual conflicts only.The fetch extension can be configured via $HOME/.hgrc like this: [extensions] hgext.fetch = [defaults] fetch = -m "merged"To keep merges semantically trivial and prevent genuine mergeconflicts or lost updates, it is essential to observe to followinggeneral discipline wrt. the public Isabelle push area: * Before editing, pull or fetch the latest version. * Accumulate private commits for a maximum of 1-3 days. * Start publishing again by pull or fetch, which normally produces local merges. * Test the merged result, e.g. like this: isabelle build -a * Push back in real time.Piling private changes and public merges longer than 0.5-2 hours isapt to produce some mess when pushing eventually!The pull-test-push cycle should not be repeated too fast, to avoiddelaying others from doing the same concurrently.Content discipline------------------The following principles should be kept in mind when producingchangesets that are meant to be published at some point. * The author of changes needs to be properly identified, using [ui]username configuration as described above. While Mercurial also provides means for signed changesets, we want to keep things simple and trust that users specify their identity correctly (and uniquely). * The history of sources is an integral part of the sources themselves. This means that private experiments and branches should not be published by accident. Named branches are not allowed on the public version. Note that old SVN-style branching is replaced by regular repository clones in Mercurial. Exchanging local experiments with some other users can be done directly on peer-to-peer basis, without affecting the central pull/push area. * Log messages are an integral part of the history of sources. Other people will have to inspect them routinely, to understand why things have been done in a certain way at some point. Authors of log entries should be aware that published changes are actually read. The main point is not to announce novelties, but to describe faithfully what has been done, and provide some clues about the motivation behind it. The main recipient is someone who needs to understand the change in the distant future to isolate problems. Sometimes it is helpful to reference past changes formally via changeset ids in the log entry. * The standard changelog entry format of the Isabelle repository admits several (somehow related) items to be rolled into one changeset. Each item is then described on a separate line that may become longer as screen line and is terminated by punctuation. These lines are roughly ordered by importance. This format conforms to established Isabelle tradition. In contrast, the default of Mercurial prefers a single headline followed by a long body text. The reason for that is a somewhat different development model of typical "distributed" projects, where external changes pass through a hierarchy of reviewers and maintainers, until they end up in some authoritative repository. Isabelle changesets can be more spontaneous, growing from the bottom-up. The web style of https://isabelle.in.tum.de/repos/isabelle accommodates the Isabelle changelog format. Note that multiple lines will sometimes display as a single paragraph in HTML, so some terminating punctuation is required. Do not squeeze multiple items on the same line in the original text!Testing of changes (before push)--------------------------------The integrity of the standard pull/push area of Isabelle needs the bepreserved at all time. This means that a complete test with defaultconfiguration needs to be finished successfully before push. If thepreparation of the push involves a pull/merge phase, its result needsto covered by the test as well.There are several possibilities to perform the test, e.g. using theIsabelle testboard at TUM. In contrast, the subsequent command-lineexamples are for tests on the local machine: ./bin/isabelle build -a #regular test ./bin/isabelle build -a -o document=pdf #test with document preparation (optional) ./bin/isabelle build -a -j2 -o threads=4 #test on multiple cores (example)See also the chapter on Isabelle sessions and build management in the"system" manual. The build option -S is particularly useful for quicktests of individual commits, e.g. for each step of a longer chain ofchanges, but the final push always requires a full test as above!Note that implicit dependencies on Isabelle components are specifiedvia catalog files in $ISABELLE_HOME/Admin/components/ as part of theMercurial history. This allows to bisect over a range of Isabelleversions while references to the contributing components changeaccordingly. Recall that "isabelle components -a" updates the localcomponent store monotonically according to that information, and thusresolves missing components.