wenzelm@28907: Important notes on Mercurial repository access for Isabelle wenzelm@28907: =========================================================== wenzelm@28907: wenzelm@28907: Preamble wenzelm@28907: -------- wenzelm@28907: wenzelm@28907: Mercurial http://www.selenic.com/mercurial belongs to a new generation wenzelm@28907: of source code management systems, following the paradigm of wenzelm@28907: "distributed version control". Compared to the old centralized model wenzelm@28907: of CVS/SVN, this gives considerable more power and freedom in wenzelm@28907: organizing the flow of changes, both between individual developers and wenzelm@28907: designated pull/push areas that are shared with others. wenzelm@28907: wenzelm@28907: More power for the user also means more responsibility! Due to its wenzelm@28907: decentralized nature, changesets that have been published once, wenzelm@28907: e.g. via push to a shared repository that is visible on the net, wenzelm@28907: cannot be easily retracted from the public again. Regular Mercurial wenzelm@28907: operations are strictly monotonic, where changset transactions are wenzelm@28907: only added, but never deleted. There are special tools to "repair" wenzelm@28907: individual repositories via non-monotonic actions, but this does not wenzelm@28907: yet retrieve unwanted changesets that have escaped into the public. wenzelm@28907: wenzelm@28907: Only global operations like pull/push, unbundle/bundle etc. fall into wenzelm@28907: this critical category; incoming/outgoing or in/out may help to wenzelm@28907: inspect changesets before exchanging them globally. Anything else in wenzelm@28907: Mercurial is local to the user's repository clone (including wenzelm@28907: commit/update/merge etc.) and is in fact much simpler and safer to use wenzelm@28907: than the corresponding operations of CVS or SVN. wenzelm@28907: wenzelm@28907: wenzelm@28907: Initial configuration wenzelm@28907: ===================== wenzelm@28907: wenzelm@28907: Never use any Mercurial version before 1.0! At the moment, versions wenzelm@28907: 1.0, 1.0.1 and 1.0.2 all work equally well. wenzelm@28907: wenzelm@28907: wenzelm@28907: The public pull area of the Isabelle repository can be cloned like wenzelm@28907: 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@28907: by another clone operation! wenzelm@28907: wenzelm@28907: There is also ~/.hgrc for per-user Mercurial configuration. The wenzelm@28907: initial configuration should include at least an entry to identify wenzelm@28907: yourself. For example, something like this in /home/wenzelm/.hgrc: wenzelm@28907: wenzelm@28907: [ui] wenzelm@28907: username = wenzelm wenzelm@28907: wenzelm@28907: Failing to configure the username correctly makes the system invent wenzelm@28907: funny machine names that may persist eternally in the flow of wenzelm@28907: changesets. wenzelm@28907: wenzelm@28907: In principle, user names can be chosen freely, but for longterm wenzelm@28907: committers of the Isabelle repository the obvious choice is to keep wenzelm@28907: with the old CVS naming scheme. wenzelm@28907: wenzelm@28907: wenzelm@28907: There are other useful configuration to go into ~/.hgrc, e.g. defaults wenzelm@28907: for common commands: wenzelm@28907: wenzelm@28907: [defaults] wenzelm@28907: log = -l 10 wenzelm@28907: wenzelm@28907: The next example shows how to install some Mercurial extension: wenzelm@28907: wenzelm@28907: [extensions] wenzelm@28907: hgext.graphlog = wenzelm@28907: wenzelm@28907: Now the additional glog command will be available. wenzelm@28907: wenzelm@28907: wenzelm@28907: See also the fine documentation for further details, especially the wenzelm@28907: book http://hgbook.red-bean.com/ wenzelm@28907: wenzelm@28907: wenzelm@28907: Shared pull/push access wenzelm@28907: ======================= 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@28907: above. Anybody can produce a clone, change it arbitrarily, and then wenzelm@28907: use regular mechanisms of Mercurial to report changes "upstream", say wenzelm@28907: via e-mail to someone with write access to that file space. It is wenzelm@28907: also quite easy to publish changed clones again on the web, using hg wenzelm@28907: serve, or the hgweb.cgi or hgwebdir.cgi scripts that are included in wenzelm@28907: the Mercurial distribution. wenzelm@28907: wenzelm@28907: This 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@28907: pushing anything onto the official Isabelle repository at TUM. wenzelm@28907: wenzelm@28907: wenzelm@28907: Direct pull/push access requires an account at TUM, with properly wenzelm@28907: configured ssh access to the local machines (e.g. macbroy20, wenzelm@28907: atbroy100). wenzelm@28907: wenzelm@28907: The simple wrapper script /home/isabelle/mercurial/bin/hg provides a wenzelm@28907: uniform view on the different Linux installations on the local wenzelm@28907: network. Thus it is advisable to add that directory to the shell PATH wenzelm@28907: of the account at TUM: wenzelm@28907: wenzelm@28907: PATH="/home/isabelle/mercurial/bin:$PATH" wenzelm@28907: wenzelm@28907: Now a clone of the shared push/pull area can be produced like this, wenzelm@28907: using your user name instead of "wenzelm": wenzelm@28907: wenzelm@28907: hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle wenzelm@28907: wenzelm@28907: In fact, the only difference to the previous clone of wenzelm@28908: http://isabelle.in.tum.de/repos/isabelle is a different default wenzelm@28907: pull/push path in isabelle/.hg/hgrc: wenzelm@28907: wenzelm@28907: [paths] wenzelm@28907: default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle wenzelm@28907: wenzelm@28907: This means an earlier pull-only clone can be changed into a pull/push wenzelm@28907: version by editing this single line of the internal repository wenzelm@28907: configuration. wenzelm@28907: wenzelm@28907: wenzelm@28907: Content discipline wenzelm@28907: ================== wenzelm@28907: wenzelm@28907: Old-style centralized version control is occasionally compared with a wenzelm@28907: "library where everybody scribbles into the books". Or seen the other wenzelm@28907: way round, the centralized model discourages individual wenzelm@28907: experimentation (with local branches etc.), because everything is wenzelm@28907: forced to happen on a shared file space. With Mercurial, arbitrary wenzelm@28907: variations on local clones are no problem, but care is required again wenzelm@28907: when publishing changes eventually. wenzelm@28907: wenzelm@28907: The following principles should be kept in mind when producing wenzelm@28907: changesets that might become public at some point. wenzelm@28907: wenzelm@28907: * The author of changes should be properly identified, using wenzelm@28907: 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@28907: correctly. 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@28907: should not be published, unless they are really meant to become wenzelm@28907: universally available. wenzelm@28907: wenzelm@28907: Note that exchanging local experiments with some other users can wenzelm@28907: be done directly on peer-to-peer basis, without affecting the wenzelm@28907: central pull/push area. wenzelm@28907: wenzelm@28907: * Log messages are an integral part of the history of sources. wenzelm@28907: Other users will have to look there eventually, to understand why wenzelm@28907: things have been done in a certain way at some point. wenzelm@28907: wenzelm@28907: Mercurial provides nice web presentation of incoming changes with wenzelm@28908: a digest of log entries; this also includes RSS/Atom news feeds. wenzelm@28907: Users should be aware that others will actually read what is wenzelm@28907: written into log messages. wenzelm@28907: wenzelm@28907: The usual changelog presentation style for the Isabelle repository wenzelm@28907: admits log entries that consist of several lines, but without the wenzelm@28907: special head line that is used in Mercurial projects elsewhere. wenzelm@28907: Since some display styles strip newlines from text, it is wenzelm@28907: advisable to separate lines via punctuation, and not rely on wenzelm@28907: two-dimensional presentation too much. wenzelm@28907: wenzelm@28907: wenzelm@28908: Building Isabelle from the repository version wenzelm@28908: ============================================= wenzelm@28908: wenzelm@28910: Compared to a proper distribution or development snapshot, a wenzelm@28908: repository version of Isabelle lacks proper version identifiers in wenzelm@28910: various places, and some components produced by Admin/build. After wenzelm@28908: applying that script with suitable options, the regular user wenzelm@28908: instructions for building and running Isabelle from sources apply. wenzelm@28908: wenzelm@28908: Needless to say, the results from the build process must not be wenzelm@28908: committed back into the repository! wenzelm@28908: wenzelm@28908: wenzelm@28907: Makarius 29-Nov-2008