wenzelm@28907: Important notes on Mercurial repository access for Isabelle wenzelm@28907: =========================================================== wenzelm@28907: wenzelm@50453: Quick start in 25min wenzelm@49348: -------------------- wenzelm@49348: wenzelm@50453: 1a. Windows: ensure that Cygwin with Mercurial and Perl is installed; wenzelm@50453: see also http://www.cygwin.com/ wenzelm@50453: wenzelm@50453: 1b. Mac OS X and Linux: ensure that Mercurial (hg) is installed; see wenzelm@50453: also http://www.selenic.com/mercurial wenzelm@49348: wenzelm@50457: 2. Create file $USER_HOME/.isabelle/etc/settings and insert the following wenzelm@49348: line near its beginning: wenzelm@49348: wenzelm@50457: init_components "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main" wenzelm@49348: wenzelm@50453: 3. Execute bash shell commands as follows: wenzelm@49348: wenzelm@49348: hg clone http://isabelle.in.tum.de/repos/isabelle wenzelm@49348: wenzelm@49348: ./isabelle/bin/isabelle components -a wenzelm@49348: wenzelm@49348: ./isabelle/bin/isabelle build -b HOL wenzelm@49348: wenzelm@49348: ./isabelle/bin/isabelle jedit wenzelm@49348: wenzelm@50281: 4. For later update replace "hg clone ..." above by: wenzelm@50281: wenzelm@50281: cd isabelle wenzelm@50281: wenzelm@50281: hg pull -u wenzelm@50281: wenzelm@49348: wenzelm@40601: Introduction wenzelm@40601: ------------ wenzelm@28907: wenzelm@40601: Mercurial http://www.selenic.com/mercurial belongs to the current wenzelm@40601: generation of source code management systems that follow the so-called wenzelm@40601: paradigm of "distributed version control". This is a terrific name wenzelm@40601: for plain revision control without the legacy of CVS or SVN. See also wenzelm@40601: http://hginit.com/ for an introduction to the main ideas. The wenzelm@40601: Mercurial book http://hgbook.red-bean.com/ explains many more details. wenzelm@40601: wenzelm@40601: Mercurial offers great flexibility in organizing the flow of changes, wenzelm@40601: both between individual developers and designated pull/push areas that wenzelm@40601: are shared with others. This additional power demands some 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@40601: transactions are only added, but never deleted. There are special wenzelm@40601: tools to manipulate repositories via non-monotonic actions (such as wenzelm@40601: "rollback" or "strip"), but recovering from gross mistakes that have wenzelm@40601: escaped into the public can be hard and embarrassing. It is much wenzelm@40601: 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@40601: useful sanity checks beyond raw "pull" / "update" / "merge". Most wenzelm@40601: other operations are local to the user's repository clone. This gives wenzelm@40601: some freedom for 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@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@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@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@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@40601: 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@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@40601: changes. In any case, changesets need to be understandable, at the wenzelm@40601: time of writing and many years later. wenzelm@28907: wenzelm@40601: Push access to the Isabelle repository requires an account at TUM, wenzelm@47449: with properly configured ssh to the local machines (e.g. macbroy20 .. wenzelm@47449: macbroy29). You also need to be a member of the "isabelle" Unix wenzelm@40601: 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@47449: hg out ssh://wenzelm@macbroy20//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@47449: hg push ssh://wenzelm@macbroy20//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@47449: default = ssh://wenzelm@macbroy20//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@47449: hg clone ssh://wenzelm@macbroy20//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@40601: problems. Sometimes it is helpful to reference past changes via wenzelm@40601: changeset ids in the log entry. wenzelm@28907: wenzelm@40601: * The standard changelog entry format of the Isabelle repository wenzelm@40601: admits several (vaguely 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@40601: The web style of http://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@32361: Building a repository version of Isabelle wenzelm@32361: ----------------------------------------- wenzelm@28908: wenzelm@48986: This first requires to resolve add-on components first, including the wenzelm@48986: ML system. Some extra configuration is required to approximate some wenzelm@48986: of the system integration of official Isabelle releases from a wenzelm@48986: bare-bones repository snapshot. The special directory Admin/ -- which wenzelm@48986: is absent in official releases -- might provide some further clues. wenzelm@48497: wenzelm@48844: Here is a reasonably easy way to include important Isabelle components wenzelm@48844: on the spot: wenzelm@48844: wenzelm@48854: (1) The bash script ISABELLE_HOME_USER/etc/settings is augmented by wenzelm@48844: some shell function invocations like this: wenzelm@28908: wenzelm@48844: init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main" wenzelm@48844: init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/optional" wenzelm@48844: wenzelm@48844: This uses some central place "$HOME/.isabelle/contrib" to keep wenzelm@48844: component directories that are shared by all Isabelle versions. wenzelm@48844: wenzelm@48844: (2) Missing components are resolved on the command line like this: wenzelm@48497: wenzelm@48844: isabelle components -a wenzelm@48844: wenzelm@48844: This will saturate the "$HOME/.isabelle/contrib" directory structure wenzelm@48855: according to $ISABELLE_COMPONENT_REPOSITORY. wenzelm@48497: wenzelm@48844: Since the given component catalogs in $ISABELLE_HOME/Admin/components wenzelm@48844: are subject to the Mercurial history, it is possible to bisect over a wenzelm@48844: range of Isabelle versions while references to the contributing wenzelm@48844: components change accordingly. wenzelm@48986: wenzelm@48986: The Isabelle build process is managed as follows: wenzelm@48986: wenzelm@48986: * regular "isabelle build" to build session images, e.g. HOL; wenzelm@48986: wenzelm@48986: * administrative "isabelle build_doc" to populate the doc/ wenzelm@48986: directory, such that "isabelle doc" will find the results.