wenzelm@28907: Important notes on Mercurial repository access for Isabelle wenzelm@28907: =========================================================== wenzelm@28907: 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@40849: are add-on browsers, notably hgtk that is part of the TortoiseHg wenzelm@40849: distribution and works for generic Python/GTk platforms. The wenzelm@40849: alternative "view" utility helps to inspect the semantic content of wenzelm@40849: 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@40849: with properly configured ssh to the local machines (e.g. macbroy20, wenzelm@40849: atbroy100). You also need to be a member of the "isabelle" Unix wenzelm@40849: 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@28913: hg out ssh://wenzelm@atbroy100//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@28913: hg push ssh://wenzelm@atbroy100//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@28907: default = ssh://wenzelm@atbroy100//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@28913: hg clone ssh://wenzelm@atbroy100//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@40849: * Test the merged result as usual and 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@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@40849: Compared to a proper distribution or development snapshot, it is wenzelm@40849: relatively hard to build from the raw repository version. Essential wenzelm@40849: contributing components are missing and need to be reconstructed by wenzelm@40849: running the Admin/build script by hand. Afterwards the main Isabelle wenzelm@40849: system and logic images can be compiled via the toplevel ./build wenzelm@40849: script. Note that the repository lacks some textual version wenzelm@40849: identifiers in the sources and scripts; this implies some changed wenzelm@40849: behavior when processing settings etc. wenzelm@28908: wenzelm@40849: There is no guarantee that the NEWS file is up to date at an arbitrary wenzelm@40849: point in history.