wenzelm@28907: Important notes on Mercurial repository access for Isabelle wenzelm@28907: =========================================================== wenzelm@28907: wenzelm@51468: Quick start in 25min wenzelm@50363: -------------------- wenzelm@50363: wenzelm@51668: 1a. Linux and Mac OS X: ensure that Mercurial (hg) is installed; see wenzelm@51668: also http://www.selenic.com/mercurial wenzelm@51668: wenzelm@51668: 1b. Windows: ensure that Cygwin with Mercurial and Perl is installed; wenzelm@51468: see also http://www.cygwin.com/ wenzelm@51468: wenzelm@51668: 2. Clone repository (bash shell commands): wenzelm@50363: wenzelm@50363: hg clone http://isabelle.in.tum.de/repos/isabelle wenzelm@50363: wenzelm@51590: cd isabelle wenzelm@50363: wenzelm@51668: ./bin/isabelle components -I wenzelm@51668: wenzelm@51590: ./bin/isabelle components -a wenzelm@50363: wenzelm@51590: ./bin/isabelle jedit -l HOL wenzelm@50363: wenzelm@51668: 3. Update repository (bash shell commands): wenzelm@51296: wenzelm@51296: cd isabelle wenzelm@51296: wenzelm@51296: hg pull -u wenzelm@51296: wenzelm@51590: ./bin/isabelle components -a wenzelm@51590: wenzelm@51590: ./bin/isabelle jedit -l HOL wenzelm@51590: wenzelm@50363: wenzelm@40849: Introduction wenzelm@40849: ------------ wenzelm@28907: wenzelm@40849: Mercurial http://www.selenic.com/mercurial belongs to the current wenzelm@40849: generation of source code management systems that follow the so-called wenzelm@40849: paradigm of "distributed version control". This is a terrific name wenzelm@40849: for plain revision control without the legacy of CVS or SVN. See also wenzelm@40849: http://hginit.com/ for an introduction to the main ideas. The wenzelm@40849: Mercurial book http://hgbook.red-bean.com/ explains many more details. wenzelm@28907: wenzelm@40849: Mercurial offers great flexibility in organizing the flow of changes, wenzelm@40849: both between individual developers and designated pull/push areas that wenzelm@40849: are shared with others. This additional power demands some additional wenzelm@40849: responsibility to maintain a certain development process that fits to wenzelm@40849: a particular project. wenzelm@28907: wenzelm@40849: Regular Mercurial operations are strictly monotonic, where changeset wenzelm@40849: transactions are only added, but never deleted. There are special wenzelm@40849: tools to manipulate repositories via non-monotonic actions (such as wenzelm@40849: "rollback" or "strip"), but recovering from gross mistakes that have wenzelm@40849: escaped into the public can be hard and embarrassing. It is much wenzelm@40849: easier to inspect and amend changesets routinely before pushing. wenzelm@40849: wenzelm@40849: The effect of the critical "pull" / "push" operations can be tested in wenzelm@40849: a dry run via "incoming" / "outgoing". The "fetch" extension includes wenzelm@40849: useful sanity checks beyond raw "pull" / "update" / "merge". Most wenzelm@40849: other operations are local to the user's repository clone. This gives wenzelm@40849: some freedom for experimentation without affecting anybody else. wenzelm@40849: wenzelm@40849: Mercurial provides nice web presentation of incoming changes with a wenzelm@40849: digest of log entries; this also includes RSS/Atom news feeds. There wenzelm@48320: are add-on history browsers such as "hg view" and TortoiseHg. Unlike wenzelm@48320: the default web view, some of these tools help to inspect the semantic wenzelm@48320: content of non-trivial merge nodes. wenzelm@28907: wenzelm@28907: wenzelm@28907: Initial configuration wenzelm@29481: --------------------- wenzelm@28907: wenzelm@28913: The official Isabelle repository can be cloned like this: wenzelm@28907: wenzelm@28907: hg clone http://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@40849: by another clone operation. wenzelm@28907: wenzelm@28917: wenzelm@28913: There is also $HOME/.hgrc for per-user Mercurial configuration. The wenzelm@40849: initial configuration requires at least an entry to identify yourself wenzelm@40849: as follows: wenzelm@28907: wenzelm@28907: [ui] wenzelm@40849: username = XXX wenzelm@28907: wenzelm@40849: Isabelle contributors are free to choose either a short "login name" wenzelm@40849: (for accounts at TU Munich) or a "full name" -- with or without mail wenzelm@40849: address. It is important to stick to this choice once and for all. wenzelm@40849: The machine default that Mercurial produces for unspecified wenzelm@40849: [ui]username is not appropriate. wenzelm@28907: wenzelm@40849: Such configuration can be given in $HOME/.hgrc (for each home wenzelm@40849: directory on each machine) or in .hg/hgrc (for each repository clone). wenzelm@28907: wenzelm@28907: wenzelm@40849: Here are some further examples for hgrc. This is how to provide wenzelm@40849: default options for common commands: wenzelm@28907: wenzelm@28907: [defaults] wenzelm@28907: log = -l 10 wenzelm@28907: wenzelm@40849: This is how to configure some extension, which is called "graphlog" wenzelm@40849: 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@28907: The entry point http://isabelle.in.tum.de/repos/isabelle is world wenzelm@28907: readable, both via plain web browsing and the hg client as described wenzelm@40849: above. Anybody can produce a clone, change it locally, and then use wenzelm@40849: regular mechanisms of Mercurial to report changes upstream, say via wenzelm@40849: mail to someone with write access to that file space. It is also wenzelm@40849: quite easy to publish changed clones again on the web, using the wenzelm@40849: ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts wenzelm@40849: that are included in the Mercurial distribution, and send a "pull wenzelm@40849: request" to someone else. There are also public hosting services for wenzelm@40849: Mercurial repositories. 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@40849: pushing anything onto the official Isabelle repository at TUM. Direct wenzelm@40849: pushes are also reviewed routinely in a post-hoc fashion; everybody wenzelm@40849: hooked on the main repository is called to keep an eye on incoming wenzelm@40849: changes. In any case, changesets need to be understandable, at the wenzelm@40849: time of writing and many years later. wenzelm@28907: wenzelm@40849: Push access to the Isabelle repository requires an account at TUM, wenzelm@51632: with properly configured ssh to the local machines (e.g. lxbroy10). wenzelm@51632: You also 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@28907: wenzelm@51632: hg out ssh://wenzelm@lxbroy10//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@51632: hg push ssh://wenzelm@lxbroy10//home/isabelle-repository/repos/isabelle wenzelm@28907: wenzelm@28913: wenzelm@40849: Default paths for push and pull can be configured in wenzelm@40849: isabelle/.hg/hgrc, for example: wenzelm@28907: wenzelm@28907: [paths] wenzelm@51632: default = ssh://wenzelm@lxbroy10//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@51632: hg clone ssh://wenzelm@lxbroy10//home/isabelle-repository/repos/isabelle wenzelm@28907: wenzelm@28907: wenzelm@40849: Simple merges wenzelm@40849: ------------- 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@40849: "fetch" extension accommodates this case nicely, automating trivial wenzelm@30182: merges and requiring manual intervention for actual conflicts only. wenzelm@30182: wenzelm@40849: 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@40849: To keep merges semantically trivial and prevent genuine merge wenzelm@40849: conflicts or lost updates, it is essential to observe to following wenzelm@40849: general discipline wrt. the public Isabelle push area: wenzelm@40849: wenzelm@40849: * Before editing, pull or fetch the latest version. wenzelm@40849: wenzelm@40849: * Accumulate private commits for a maximum of 1-3 days. wenzelm@40849: wenzelm@40849: * Start publishing again by pull or fetch, which normally produces wenzelm@40849: local merges. wenzelm@40849: wenzelm@51296: * Test the merged result, e.g. like this: wenzelm@51296: wenzelm@51296: isabelle build -a wenzelm@51296: wenzelm@51296: * Push back in real time. wenzelm@40849: wenzelm@40849: Piling private changes and public merges longer than 0.5-2 hours is wenzelm@40849: apt to produce some mess when pushing eventually! wenzelm@30182: wenzelm@51296: The pull-test-push cycle should not be repeated too fast, to avoid wenzelm@51296: delaying others from doing the same concurrently. wenzelm@51296: wenzelm@30182: wenzelm@28907: Content discipline wenzelm@29481: ------------------ wenzelm@28907: wenzelm@40849: The following principles should be kept in mind when producing wenzelm@40849: changesets that are meant to be published at some point. wenzelm@28907: wenzelm@40849: * The author of changes needs to be properly identified, using wenzelm@40849: [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@40849: 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@40849: should not be published by accident. Named branches are not wenzelm@40849: allowed on the public version. Note that old SVN-style branching wenzelm@40849: is replaced by regular repository clones in Mercurial. wenzelm@28907: wenzelm@40849: Exchanging local experiments with some other users can be done wenzelm@40849: directly on peer-to-peer basis, without affecting the central wenzelm@40849: pull/push area. wenzelm@28907: wenzelm@28907: * Log messages are an integral part of the history of sources. wenzelm@40849: Other people will have to inspect them routinely, to understand wenzelm@40849: why things have been done in a certain way at some point. wenzelm@28907: wenzelm@40849: Authors of log entries should be aware that published changes are wenzelm@40849: actually read. The main point is not to announce novelties, but wenzelm@40849: to describe faithfully what has been done, and provide some clues wenzelm@40849: about the motivation behind it. The main recipient is someone who wenzelm@40849: needs to understand the change in the distant future to isolate wenzelm@40849: problems. Sometimes it is helpful to reference past changes via wenzelm@40849: changeset ids in the log entry. wenzelm@28907: wenzelm@40849: * The standard changelog entry format of the Isabelle repository wenzelm@40849: admits several (vaguely related) items to be rolled into one wenzelm@40849: changeset. Each item is then described on a separate line that wenzelm@40849: may become longer as screen line and is terminated by punctuation. wenzelm@40849: These lines are roughly ordered by importance. wenzelm@40849: wenzelm@40849: This format conforms to established Isabelle tradition. In wenzelm@40849: contrast, the default of Mercurial prefers a single headline wenzelm@40849: followed by a long body text. The reason for that is a somewhat wenzelm@40849: different development model of typical "distributed" projects, wenzelm@40849: where external changes pass through a hierarchy of reviewers and wenzelm@40849: maintainers, until they end up in some authoritative repository. wenzelm@40849: Isabelle changesets can be more spontaneous, growing from the wenzelm@40849: bottom-up. wenzelm@40849: wenzelm@40849: The web style of http://isabelle.in.tum.de/repos/isabelle/ wenzelm@40849: accommodates the Isabelle changelog format. Note that multiple wenzelm@40849: lines will sometimes display as a single paragraph in HTML, so wenzelm@40849: some terminating punctuation is required. Do not squeeze multiple wenzelm@40849: items on the same line in the original text! wenzelm@28907: wenzelm@28907: wenzelm@32361: Building a repository version of Isabelle wenzelm@32361: ----------------------------------------- wenzelm@28908: wenzelm@50001: This first requires to resolve add-on components first, including the wenzelm@50001: ML system. Some extra configuration is required to approximate some wenzelm@50001: of the system integration of official Isabelle releases from a wenzelm@50001: bare-bones repository snapshot. The special directory Admin/ -- which wenzelm@50001: is absent in official releases -- might provide some further clues. wenzelm@28908: wenzelm@49859: Here is a reasonably easy way to include important Isabelle components wenzelm@49859: on the spot: wenzelm@49512: wenzelm@49869: (1) The bash script ISABELLE_HOME_USER/etc/settings is augmented by wenzelm@49859: some shell function invocations like this: wenzelm@49512: wenzelm@49859: init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main" wenzelm@49859: init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/optional" wenzelm@49512: wenzelm@49859: This uses some central place "$HOME/.isabelle/contrib" to keep wenzelm@49859: component directories that are shared by all Isabelle versions. wenzelm@49512: wenzelm@49859: (2) Missing components are resolved on the command line like this: wenzelm@49859: wenzelm@49859: isabelle components -a wenzelm@49859: wenzelm@49859: This will saturate the "$HOME/.isabelle/contrib" directory structure wenzelm@49870: according to $ISABELLE_COMPONENT_REPOSITORY. wenzelm@49859: wenzelm@49859: Since the given component catalogs in $ISABELLE_HOME/Admin/components wenzelm@49859: are subject to the Mercurial history, it is possible to bisect over a wenzelm@49859: range of Isabelle versions while references to the contributing wenzelm@49859: components change accordingly. wenzelm@50001: wenzelm@50001: The Isabelle build process is managed as follows: wenzelm@50001: wenzelm@51590: * regular "isabelle build" to build session images, for example: wenzelm@51590: wenzelm@51590: isabelle build -b HOL wenzelm@50001: wenzelm@50001: * administrative "isabelle build_doc" to populate the doc/ wenzelm@51590: directory, such that "isabelle doc" will find the results, for example: wenzelm@51590: wenzelm@51669: isabelle build_doc -p IsarRef wenzelm@51590: