wenzelm@28907: Important notes on Mercurial repository access for Isabelle wenzelm@28907: =========================================================== wenzelm@28907: wenzelm@54963: Quick start in 30min wenzelm@49348: -------------------- wenzelm@49348: wenzelm@63490: 1a. Linux and Mac OS X: ensure that Mercurial is installed wenzelm@63490: (see also http://www.selenic.com/mercurial) wenzelm@49348: wenzelm@66763: 1b. Windows: ensure that Cygwin64 with curl and Mercurial is installed wenzelm@63490: (see also http://www.cygwin.com) wenzelm@49348: wenzelm@50653: 2. Clone repository (bash shell commands): wenzelm@49348: wenzelm@67744: hg clone https://isabelle.in.tum.de/repos/isabelle wenzelm@49348: wenzelm@50575: cd isabelle wenzelm@49348: wenzelm@50653: ./bin/isabelle components -I wenzelm@50653: wenzelm@50575: ./bin/isabelle components -a wenzelm@49348: wenzelm@50575: ./bin/isabelle jedit -l HOL wenzelm@49348: wenzelm@51502: ./bin/isabelle build -b HOL #optional: build session image manually wenzelm@51502: wenzelm@50653: 3. Update repository (bash shell commands): wenzelm@50281: wenzelm@50281: cd isabelle wenzelm@50281: wenzelm@50281: hg pull -u wenzelm@50281: wenzelm@50575: ./bin/isabelle components -a wenzelm@50575: wenzelm@50575: ./bin/isabelle jedit -l HOL wenzelm@50575: wenzelm@51502: ./bin/isabelle jedit -b -f #optional: force fresh build of Isabelle/Scala wenzelm@51502: wenzelm@51502: 4. Access documentation (bash shell commands): wenzelm@51502: wenzelm@53359: ./bin/isabelle build_doc -a wenzelm@51502: wenzelm@51502: ./bin/isabelle doc system wenzelm@51502: wenzelm@49348: wenzelm@40601: Introduction wenzelm@40601: ------------ wenzelm@28907: wenzelm@63985: Mercurial http://www.selenic.com/mercurial belongs to source code wenzelm@63985: management systems that follow the so-called paradigm of "distributed wenzelm@63985: version control". This means plain revision control without the wenzelm@63985: legacy of CVS or SVN (and without the extra complexity introduced by wenzelm@63985: git). See also http://hginit.com/ for an introduction to the main wenzelm@63985: ideas. The Mercurial book http://hgbook.red-bean.com/ explains many wenzelm@63985: more details. wenzelm@40601: wenzelm@63985: Mercurial offers some flexibility in organizing the flow of changes, wenzelm@40601: both between individual developers and designated pull/push areas that wenzelm@63985: are shared with others. This additional freedom demands additional wenzelm@40601: responsibility to maintain a certain development process that fits to wenzelm@40601: a particular project. wenzelm@28907: wenzelm@40601: Regular Mercurial operations are strictly monotonic, where changeset wenzelm@51502: transactions are only added, but never deleted or mutated. There are wenzelm@51502: special tools to manipulate repositories via non-monotonic actions wenzelm@51502: (such as "rollback" or "strip"), but recovering from gross mistakes wenzelm@51502: that have escaped into the public can be hard and embarrassing. It is wenzelm@51502: much easier to inspect and amend changesets routinely before pushing. wenzelm@28907: wenzelm@40601: The effect of the critical "pull" / "push" operations can be tested in wenzelm@40601: a dry run via "incoming" / "outgoing". The "fetch" extension includes wenzelm@51502: useful sanity checks beyond raw "pull" / "update" / "merge", although wenzelm@51502: it has lost popularity in recent years. Most other operations are wenzelm@51502: local to the user's repository clone. This gives some freedom for wenzelm@51502: experimentation without affecting anybody else. wenzelm@40601: wenzelm@40601: Mercurial provides nice web presentation of incoming changes with a wenzelm@40601: digest of log entries; this also includes RSS/Atom news feeds. There wenzelm@47449: are add-on history browsers such as "hg view" and TortoiseHg. Unlike wenzelm@47449: the default web view, some of these tools help to inspect the semantic wenzelm@47449: content of non-trivial merge nodes. wenzelm@28907: wenzelm@28907: wenzelm@28907: Initial configuration wenzelm@29481: --------------------- wenzelm@28907: wenzelm@51502: The main Isabelle repository can be cloned like this: wenzelm@28907: wenzelm@67744: hg clone https://isabelle.in.tum.de/repos/isabelle wenzelm@28907: wenzelm@28907: This will create a local directory "isabelle", unless an alternative wenzelm@28907: name is specified. The full repository meta-data and history of wenzelm@28907: changes is in isabelle/.hg; local configuration for this clone can be wenzelm@28907: added to isabelle/.hg/hgrc, but note that hgrc files are never copied wenzelm@40601: by another clone operation. wenzelm@28907: wenzelm@28917: wenzelm@28913: There is also $HOME/.hgrc for per-user Mercurial configuration. The wenzelm@40601: initial configuration requires at least an entry to identify yourself wenzelm@40601: as follows: wenzelm@28907: wenzelm@28907: [ui] wenzelm@40601: username = XXX wenzelm@28907: wenzelm@40601: Isabelle contributors are free to choose either a short "login name" wenzelm@40601: (for accounts at TU Munich) or a "full name" -- with or without mail wenzelm@40601: address. It is important to stick to this choice once and for all. wenzelm@40601: The machine default that Mercurial produces for unspecified wenzelm@40601: [ui]username is not appropriate. wenzelm@28907: wenzelm@40601: Such configuration can be given in $HOME/.hgrc (for each home wenzelm@40601: directory on each machine) or in .hg/hgrc (for each repository clone). wenzelm@28907: wenzelm@28907: wenzelm@40601: Here are some further examples for hgrc. This is how to provide wenzelm@40601: default options for common commands: wenzelm@28907: wenzelm@28907: [defaults] wenzelm@28907: log = -l 10 wenzelm@28907: wenzelm@40601: This is how to configure some extension, which is called "graphlog" wenzelm@40601: and provides the "glog" command: wenzelm@28907: wenzelm@28907: [extensions] wenzelm@28907: hgext.graphlog = wenzelm@28907: wenzelm@28907: wenzelm@28907: Shared pull/push access wenzelm@29481: ----------------------- wenzelm@28907: wenzelm@67744: The entry point https://isabelle.in.tum.de/repos/isabelle is world wenzelm@28907: readable, both via plain web browsing and the hg client as described wenzelm@40601: above. Anybody can produce a clone, change it locally, and then use wenzelm@40601: regular mechanisms of Mercurial to report changes upstream, say via wenzelm@40601: mail to someone with write access to that file space. It is also wenzelm@40601: quite easy to publish changed clones again on the web, using the wenzelm@40601: ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts wenzelm@40601: that are included in the Mercurial distribution, and send a "pull wenzelm@40601: request" to someone else. There are also public hosting services for wenzelm@51502: Mercurial repositories, notably Bitbucket. wenzelm@28907: wenzelm@28913: The downstream/upstream mode of operation is quite common in the wenzelm@28907: distributed version control community, and works well for occasional wenzelm@28907: changes produced by anybody out there. Of course, upstream wenzelm@28907: maintainers need to review and moderate changes being proposed, before wenzelm@40601: pushing anything onto the official Isabelle repository at TUM. Direct wenzelm@40601: pushes are also reviewed routinely in a post-hoc fashion; everybody wenzelm@40601: hooked on the main repository is called to keep an eye on incoming wenzelm@51502: changes. In any case, changesets need to be understandable, both at wenzelm@51502: the time of writing and many years later. wenzelm@28907: wenzelm@40601: Push access to the Isabelle repository requires an account at TUM, wenzelm@51072: with properly configured ssh to isabelle-server.in.tum.de. You also wenzelm@51072: need to be a member of the "isabelle" Unix group. wenzelm@28907: wenzelm@28913: Sharing a locally modified clone then works as follows, using your wenzelm@28913: user name instead of "wenzelm": wenzelm@28913: wenzelm@51072: hg out ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle wenzelm@28907: wenzelm@28913: In fact, the "out" or "outgoing" command performs only a dry run: it wenzelm@28913: displays the changesets that would get published. An actual "push", wenzelm@28913: with a lasting effect on the Isabelle repository, works like this: wenzelm@28907: wenzelm@51072: hg push ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle wenzelm@28913: wenzelm@28907: wenzelm@40601: Default paths for push and pull can be configured in wenzelm@40601: isabelle/.hg/hgrc, for example: wenzelm@28907: wenzelm@28907: [paths] wenzelm@51072: default = ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle wenzelm@28907: wenzelm@28913: Now "hg pull" or "hg push" will use that shared file space, unless a wenzelm@28913: different URL is specified explicitly. wenzelm@28913: wenzelm@28913: When cloning a repository, the default path is set to the initial wenzelm@28913: source URL. So we could have cloned via that ssh URL in the first wenzelm@28913: place, to get exactly to the same point: wenzelm@28913: wenzelm@51072: hg clone ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle wenzelm@28907: wenzelm@28907: wenzelm@40601: Simple merges wenzelm@40601: ------------- wenzelm@30182: wenzelm@30182: The main idea of Mercurial is to let individual users produce wenzelm@30182: independent branches of development first, but merge with others wenzelm@30182: frequently. The basic hg merge operation is more general than wenzelm@30182: required for the mode of operation with a shared pull/push area. The wenzelm@40601: "fetch" extension accommodates this case nicely, automating trivial wenzelm@30182: merges and requiring manual intervention for actual conflicts only. wenzelm@30182: wenzelm@40601: The fetch extension can be configured via $HOME/.hgrc like this: wenzelm@30182: wenzelm@30182: [extensions] wenzelm@30182: hgext.fetch = wenzelm@30182: wenzelm@30182: [defaults] wenzelm@30182: fetch = -m "merged" wenzelm@30182: wenzelm@40601: To keep merges semantically trivial and prevent genuine merge wenzelm@40601: conflicts or lost updates, it is essential to observe to following wenzelm@40601: general discipline wrt. the public Isabelle push area: wenzelm@40601: wenzelm@40601: * Before editing, pull or fetch the latest version. wenzelm@40601: wenzelm@40601: * Accumulate private commits for a maximum of 1-3 days. wenzelm@40601: wenzelm@40601: * Start publishing again by pull or fetch, which normally produces wenzelm@40601: local merges. wenzelm@40601: wenzelm@50281: * Test the merged result, e.g. like this: wenzelm@50281: wenzelm@50281: isabelle build -a wenzelm@50281: wenzelm@50281: * Push back in real time. wenzelm@40601: wenzelm@40601: Piling private changes and public merges longer than 0.5-2 hours is wenzelm@40601: apt to produce some mess when pushing eventually! wenzelm@30182: wenzelm@50281: The pull-test-push cycle should not be repeated too fast, to avoid wenzelm@50281: delaying others from doing the same concurrently. wenzelm@50281: wenzelm@30182: wenzelm@28907: Content discipline wenzelm@29481: ------------------ wenzelm@28907: wenzelm@40601: The following principles should be kept in mind when producing wenzelm@40601: changesets that are meant to be published at some point. wenzelm@28907: wenzelm@40601: * The author of changes needs to be properly identified, using wenzelm@40601: [ui]username configuration as described above. wenzelm@28907: wenzelm@28907: While Mercurial also provides means for signed changesets, we want wenzelm@28907: to keep things simple and trust that users specify their identity wenzelm@40601: correctly (and uniquely). wenzelm@28907: wenzelm@28907: * The history of sources is an integral part of the sources wenzelm@28907: themselves. This means that private experiments and branches wenzelm@40601: should not be published by accident. Named branches are not wenzelm@40601: allowed on the public version. Note that old SVN-style branching wenzelm@40601: is replaced by regular repository clones in Mercurial. wenzelm@28907: wenzelm@40601: Exchanging local experiments with some other users can be done wenzelm@40601: directly on peer-to-peer basis, without affecting the central wenzelm@40601: pull/push area. wenzelm@28907: wenzelm@28907: * Log messages are an integral part of the history of sources. wenzelm@40601: Other people will have to inspect them routinely, to understand wenzelm@40601: why things have been done in a certain way at some point. wenzelm@40601: wenzelm@40601: Authors of log entries should be aware that published changes are wenzelm@40601: actually read. The main point is not to announce novelties, but wenzelm@40601: to describe faithfully what has been done, and provide some clues wenzelm@40601: about the motivation behind it. The main recipient is someone who wenzelm@40601: needs to understand the change in the distant future to isolate wenzelm@51502: problems. Sometimes it is helpful to reference past changes wenzelm@51502: formally via changeset ids in the log entry. wenzelm@28907: wenzelm@40601: * The standard changelog entry format of the Isabelle repository wenzelm@51502: admits several (somehow related) items to be rolled into one wenzelm@40601: changeset. Each item is then described on a separate line that wenzelm@40601: may become longer as screen line and is terminated by punctuation. wenzelm@40601: These lines are roughly ordered by importance. wenzelm@28907: wenzelm@40601: This format conforms to established Isabelle tradition. In wenzelm@40601: contrast, the default of Mercurial prefers a single headline wenzelm@40601: followed by a long body text. The reason for that is a somewhat wenzelm@40601: different development model of typical "distributed" projects, wenzelm@40601: where external changes pass through a hierarchy of reviewers and wenzelm@40601: maintainers, until they end up in some authoritative repository. wenzelm@40601: Isabelle changesets can be more spontaneous, growing from the wenzelm@40601: bottom-up. wenzelm@40601: wenzelm@67744: The web style of https://isabelle.in.tum.de/repos/isabelle wenzelm@40601: accommodates the Isabelle changelog format. Note that multiple wenzelm@40601: lines will sometimes display as a single paragraph in HTML, so wenzelm@40601: some terminating punctuation is required. Do not squeeze multiple wenzelm@40601: items on the same line in the original text! wenzelm@28907: wenzelm@28907: wenzelm@51502: Testing of changes (before push) wenzelm@51502: -------------------------------- wenzelm@48497: wenzelm@51502: The integrity of the standard pull/push area of Isabelle needs the be wenzelm@51502: preserved at all time. This means that a complete test with default wenzelm@51502: configuration needs to be finished successfully before push. If the wenzelm@51502: preparation of the push involves a pull/merge phase, its result needs wenzelm@51502: to covered by the test as well. wenzelm@28908: wenzelm@51502: There are several possibilities to perform the test, e.g. using the wenzelm@51502: Isabelle testboard at TUM. In contrast, the subsequent command-line wenzelm@51502: examples are for tests on the local machine: wenzelm@48844: wenzelm@51502: ./bin/isabelle build -a #regular test wenzelm@48844: wenzelm@63985: ./bin/isabelle build -a -o document=pdf #test with document preparation (optional) wenzelm@48844: wenzelm@51502: ./bin/isabelle build -a -j2 -o threads=4 #test on multiple cores (example) wenzelm@48497: wenzelm@51502: See also the chapter on Isabelle sessions and build management in the wenzelm@66753: "system" manual. The build option -S is particularly useful for quick wenzelm@66753: tests of individual commits, e.g. for each step of a longer chain of wenzelm@66753: changes, but the final push always requires a full test as above! wenzelm@48986: wenzelm@51502: Note that implicit dependencies on Isabelle components are specified wenzelm@51502: via catalog files in $ISABELLE_HOME/Admin/components/ as part of the wenzelm@51502: Mercurial history. This allows to bisect over a range of Isabelle wenzelm@51502: versions while references to the contributing components change wenzelm@51502: accordingly. Recall that "isabelle components -a" updates the local wenzelm@51502: component store monotonically according to that information, and thus wenzelm@51502: resolves missing components.