README_REPOSITORY
author haftmann
Wed Sep 15 15:31:32 2010 +0200 (2010-09-15)
changeset 39401 887f4218a39a
parent 36858 8eac822dec6c
child 40601 021278fdd0a8
permissions -rw-r--r--
code_eval renamed to code_runtime
     1 Important notes on Mercurial repository access for Isabelle
     2 ===========================================================
     3 
     4 Preamble
     5 --------
     6 
     7 Mercurial http://www.selenic.com/mercurial belongs to a new generation
     8 of source code management systems, following the paradigm of
     9 "distributed version control".  Compared to the old centralized model
    10 of CVS or SVN, this gives considerable more power and freedom in
    11 organizing the flow of changes, both between individual developers and
    12 designated pull/push areas that are shared with others.
    13 
    14 More power for the user also means more responsibility!  Due to its
    15 decentralized nature, changesets that have been published once,
    16 e.g. via "push" to a shared repository that is visible on the net,
    17 cannot be easily retracted from the public again.  Regular Mercurial
    18 operations are strictly monotonic, where changset transactions are
    19 only added, but never deleted.  There are special tools to manipulate
    20 individual repositories via non-monotonic actions, but this does not
    21 yet retrieve any changesets that have escaped into the public by
    22 accident.
    23 
    24 Only global operations like "pull" and "push" fall into this critical
    25 category.  Note that "incoming" / "outgoing" allow to inspect
    26 changesets before exchanging them globally.  Anything else in
    27 Mercurial is local to the user's repository clone (including "commit",
    28 "update", "merge" etc.) and is in fact much simpler and safer to use
    29 than the corresponding operations of CVS or SVN.
    30 
    31 
    32 Initial configuration
    33 ---------------------
    34 
    35 The official Isabelle repository can be cloned like this:
    36 
    37   hg clone http://isabelle.in.tum.de/repos/isabelle
    38 
    39 This will create a local directory "isabelle", unless an alternative
    40 name is specified.  The full repository meta-data and history of
    41 changes is in isabelle/.hg; local configuration for this clone can be
    42 added to isabelle/.hg/hgrc, but note that hgrc files are never copied
    43 by another clone operation!
    44 
    45 
    46 There is also $HOME/.hgrc for per-user Mercurial configuration.  The
    47 initial configuration should include at least an entry to identify
    48 yourself.  For example, something like this in /home/wenzelm/.hgrc:
    49 
    50   [ui]
    51   username = wenzelm
    52 
    53 Of course, the user identity can be also configured in
    54 isabelle/.hg/hgrc on per-repository basis.  Failing to specify the
    55 username correctly makes the system invent funny machine names that
    56 may persist indefinitely in the public flow of changesets.
    57 
    58 In principle, user names can be chosen freely, but for longterm
    59 committers of the Isabelle repository the obvious choice is to keep
    60 with the old CVS naming scheme.  Others should use their regular "full
    61 name"; including an email address is optional.
    62 
    63 
    64 There are other useful configuration to go into $HOME/.hgrc,
    65 e.g. defaults for common commands:
    66 
    67   [defaults]
    68   log = -l 10
    69 
    70 The next example shows how to install some Mercurial extension:
    71 
    72   [extensions]
    73   hgext.graphlog =
    74 
    75 Now the additional glog command will be available.
    76 
    77 
    78 See also the fine documentation for further details, especially the
    79 book http://hgbook.red-bean.com/
    80 
    81 There is also a nice tutorial at http://hginit.com/
    82 
    83 
    84 Shared pull/push access
    85 -----------------------
    86 
    87 The entry point http://isabelle.in.tum.de/repos/isabelle is world
    88 readable, both via plain web browsing and the hg client as described
    89 above.  Anybody can produce a clone, change it arbitrarily, and then
    90 use regular mechanisms of Mercurial to report changes upstream, say
    91 via e-mail to someone with write access to that file space.  It is
    92 also quite easy to publish changed clones again on the web, using the
    93 adhoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts
    94 that are included in the Mercurial distribution.
    95 
    96 The downstream/upstream mode of operation is quite common in the
    97 distributed version control community, and works well for occasional
    98 changes produced by anybody out there.  Of course, upstream
    99 maintainers need to review and moderate changes being proposed, before
   100 pushing anything onto the official Isabelle repository at TUM.
   101 
   102 
   103 Write access to the Isabelle repository requires an account at TUM,
   104 with properly configured ssh access to the local machines
   105 (e.g. macbroy20, atbroy100).  You also need to be a member of the
   106 "isabelle" Unix group.
   107 
   108 Sharing a locally modified clone then works as follows, using your
   109 user name instead of "wenzelm":
   110 
   111   hg out ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   112 
   113 In fact, the "out" or "outgoing" command performs only a dry run: it
   114 displays the changesets that would get published.  An actual "push",
   115 with a lasting effect on the Isabelle repository, works like this:
   116 
   117   hg push ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   118 
   119 
   120 Default paths for push and pull can be configure in isabelle/.hg/hgrc,
   121 for example:
   122 
   123   [paths]
   124   default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   125 
   126 Now "hg pull" or "hg push" will use that shared file space, unless a
   127 different URL is specified explicitly.
   128 
   129 When cloning a repository, the default path is set to the initial
   130 source URL.  So we could have cloned via that ssh URL in the first
   131 place, to get exactly to the same point:
   132 
   133   hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   134 
   135 
   136 Simplified merges
   137 -----------------
   138 
   139 The main idea of Mercurial is to let individual users produce
   140 independent branches of development first, but merge with others
   141 frequently.  The basic hg merge operation is more general than
   142 required for the mode of operation with a shared pull/push area.  The
   143 hg fetch extension accommodates this case nicely, automating trivial
   144 merges and requiring manual intervention for actual conflicts only.
   145 
   146 The fetch extension can be configured via the user's ~/.hgrc like
   147 this:
   148 
   149   [extensions]
   150   hgext.fetch =
   151 
   152   [defaults]
   153   fetch = -m "merged"
   154 
   155 Note that the potential for merge conflicts can be greatly reduced by
   156 doing "hg fetch" before any starting local changes!
   157 
   158 
   159 Content discipline
   160 ------------------
   161 
   162 Old-style centralized version control is occasionally compared to "a
   163 library where everybody scribbles into the books".  Or seen the other
   164 way round, the centralized model discourages individual
   165 experimentation (with local branches etc.), because everything is
   166 forced to happen on a shared file space.  With Mercurial, arbitrary
   167 variations on local clones are no problem, but care is required again
   168 when publishing changes eventually.
   169 
   170 The following principles should be kept in mind when producing
   171 changesets that might become public at some point.
   172 
   173   * The author of changes should be properly identified, using
   174     ui/username configuration as described above.
   175 
   176     While Mercurial also provides means for signed changesets, we want
   177     to keep things simple and trust that users specify their identity
   178     correctly.
   179 
   180   * The history of sources is an integral part of the sources
   181     themselves.  This means that private experiments and branches
   182     should not be published, unless they are really meant to become
   183     universally available.
   184 
   185     Note that exchanging local experiments with some other users can
   186     be done directly on peer-to-peer basis, without affecting the
   187     central pull/push area.
   188 
   189   * Log messages are an integral part of the history of sources.
   190     Other users will have to look there eventually, to understand why
   191     things have been done in a certain way at some point.
   192 
   193     Mercurial provides nice web presentation of incoming changes with
   194     a digest of log entries; this also includes RSS/Atom news feeds.
   195     Users should be aware that others will actually read what is
   196     written into log messages.  There are also add-on browsers,
   197     notably hgtk that is part of the TortoiseHg distribution and works
   198     for generic Python/GTk platforms.
   199 
   200     The usual changelog presentation style for the Isabelle repository
   201     admits log entries that consist of several lines, but without the
   202     special headline that is used in Mercurial projects elsewhere.
   203     Since some display styles strip newlines from text, it is
   204     advisable to separate lines via punctuation, and not rely on
   205     two-dimensional presentation too much.
   206 
   207 
   208 Building a repository version of Isabelle
   209 -----------------------------------------
   210 
   211 Compared to a proper distribution or development snapshot, a
   212 repository version of Isabelle lacks textual version identifiers in
   213 some sources and scripts, and various components produced by
   214 Admin/build are missing.  After applying that script with suitable
   215 arguments, the regular user instructions for building and running
   216 Isabelle from sources apply.
   217 
   218 Needless to say, the results from the build process must not be added
   219 to the repository!