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@28913: of CVS or 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@28913: 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@28913: only added, but never deleted. There are special tools to manipulate wenzelm@28907: individual repositories via non-monotonic actions, but this does not wenzelm@28913: yet retrieve any changesets that have escaped into the public by wenzelm@28913: accident. wenzelm@28907: wenzelm@28918: Only global operations like "pull" and "push" fall into this critical wenzelm@28918: category. Note that "incoming" / "outgoing" allow to inspect wenzelm@28918: changesets before exchanging them globally. Anything else in wenzelm@28918: Mercurial is local to the user's repository clone (including "commit", wenzelm@28918: "update", "merge" etc.) and is in fact much simpler and safer to use wenzelm@28918: than the corresponding operations of CVS or SVN. wenzelm@28907: wenzelm@28907: wenzelm@28907: Initial configuration wenzelm@28907: ===================== wenzelm@28907: wenzelm@28913: Always use Mercurial version 1.0 or later, such as 1.0.1 or 1.0.2. wenzelm@28913: The old 0.9.x versions do not work in a multi-user environment with wenzelm@28913: shared file spaces. wenzelm@28907: 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@28907: by another clone operation! wenzelm@28907: wenzelm@28917: wenzelm@28913: There is also $HOME/.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@28917: Of course, the user identity can be also configured in wenzelm@28918: isabelle/.hg/hgrc on per-repository basis. Failing to specify the wenzelm@28917: username correctly makes the system invent funny machine names that wenzelm@28917: may persist indefinitely in the public flow of 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@28913: There are other useful configuration to go into $HOME/.hgrc, wenzelm@28913: e.g. defaults 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@28913: 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@28913: also quite easy to publish changed clones again on the web, using the wenzelm@28913: adhoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts wenzelm@28913: that are included in the Mercurial distribution. 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@28907: pushing anything onto the official Isabelle repository at TUM. wenzelm@28907: wenzelm@28907: wenzelm@28913: Write access to the Isabelle repository requires an account at TUM, wenzelm@28913: with properly configured ssh access to the local machines wenzelm@28913: (e.g. macbroy20, atbroy100). You also need to be a member of the wenzelm@28913: "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@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@28913: wenzelm@28907: wenzelm@28913: Default paths for push and pull can be configure in isabelle/.hg/hgrc, wenzelm@28913: 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@28907: Content discipline wenzelm@28907: ================== wenzelm@28907: wenzelm@28913: Old-style centralized version control is occasionally compared to "a wenzelm@28913: 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@28913: special headline 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@28913: repository version of Isabelle lacks textual version identifiers in wenzelm@28913: some sources and scripts, and various components produced by wenzelm@28913: Admin/build are missing. After applying that script with suitable wenzelm@28913: arguments, the regular user instructions for building and running wenzelm@28913: Isabelle from sources apply. wenzelm@28908: wenzelm@28913: Needless to say, the results from the build process must not be added wenzelm@28913: to the repository! wenzelm@28908: wenzelm@28908: wenzelm@28913: Makarius 30-Nov-2008