author wenzelm
Tue, 31 Mar 2015 22:31:05 +0200
changeset 59886 e0dc738eb08c
parent 50576 325bf9073c59
permissions -rw-r--r--
support for explicit scope of private entries;

Notes on central Isabelle repository

* direct file-system access (locally or remotely via ssh)

* permissions via dedicated Unix group "isabelle"

* See on physical format, with
  conservative requirements for Mercurial 1.3 as lowest common denominator:


* See for old-fashioned
  CVS-like multiple committers configuration, "The filesystem method".

  A fresh multi-user clone is initialized like this:

    hg --config format.dotencode=0 init isabelle-clone
    cd isabelle-clone
    chgrp -R isabelle .hg
    chmod g+s .hg .hg/store
    mkdir .hg/strip-backup   ## Not to be used under normal circumstances!
    chmod -R g+w .hg

  Now isabelle-clone is ready for push of repository data (without making
  a working directory).

* Addressing technical issues: according to our shared disk
  configuration (after regular ssh login) is characterized as follows:

    Advantages: can use existing setup

    Disadvantages: generally restricted to intranets, not generally
    recommended due to general issues with network filesystem reliability

  Due to NFS instabilities of unknown origin at TUM, drop-outs have
  happened before. The following measures of last resort can be applied:

    (a) "hg verify" to find offending changesets
        "hg strip REV" to remove parts of the public history by vivisection

    (b) fresh clone from known-good source as explained above

  Note that any such non-monotonic changes on the central push area work
  under the assumption of sequential single-user mode!!

  See also for
  further background information.