README_REPOSITORY
changeset 40601 021278fdd0a8
parent 36858 8eac822dec6c
child 47449 5e1482296b12
equal deleted inserted replaced
40600:c2ca0eb91d99 40601:021278fdd0a8
     1 Important notes on Mercurial repository access for Isabelle
     1 Important notes on Mercurial repository access for Isabelle
     2 ===========================================================
     2 ===========================================================
     3 
     3 
     4 Preamble
     4 Introduction
     5 --------
     5 ------------
     6 
     6 
     7 Mercurial http://www.selenic.com/mercurial belongs to a new generation
     7 Mercurial http://www.selenic.com/mercurial belongs to the current
     8 of source code management systems, following the paradigm of
     8 generation of source code management systems that follow the so-called
     9 "distributed version control".  Compared to the old centralized model
     9 paradigm of "distributed version control".  This is a terrific name
    10 of CVS or SVN, this gives considerable more power and freedom in
    10 for plain revision control without the legacy of CVS or SVN.  See also
    11 organizing the flow of changes, both between individual developers and
    11 http://hginit.com/ for an introduction to the main ideas.  The
    12 designated pull/push areas that are shared with others.
    12 Mercurial book http://hgbook.red-bean.com/ explains many more details.
    13 
    13 
    14 More power for the user also means more responsibility!  Due to its
    14 Mercurial offers great flexibility in organizing the flow of changes,
    15 decentralized nature, changesets that have been published once,
    15 both between individual developers and designated pull/push areas that
    16 e.g. via "push" to a shared repository that is visible on the net,
    16 are shared with others.  This additional power demands some additional
    17 cannot be easily retracted from the public again.  Regular Mercurial
    17 responsibility to maintain a certain development process that fits to
    18 operations are strictly monotonic, where changset transactions are
    18 a particular project.
    19 only added, but never deleted.  There are special tools to manipulate
    19 
    20 individual repositories via non-monotonic actions, but this does not
    20 Regular Mercurial operations are strictly monotonic, where changeset
    21 yet retrieve any changesets that have escaped into the public by
    21 transactions are only added, but never deleted.  There are special
    22 accident.
    22 tools to manipulate repositories via non-monotonic actions (such as
    23 
    23 "rollback" or "strip"), but recovering from gross mistakes that have
    24 Only global operations like "pull" and "push" fall into this critical
    24 escaped into the public can be hard and embarrassing.  It is much
    25 category.  Note that "incoming" / "outgoing" allow to inspect
    25 easier to inspect and amend changesets routinely before pushing.
    26 changesets before exchanging them globally.  Anything else in
    26 
    27 Mercurial is local to the user's repository clone (including "commit",
    27 The effect of the critical "pull" / "push" operations can be tested in
    28 "update", "merge" etc.) and is in fact much simpler and safer to use
    28 a dry run via "incoming" / "outgoing".  The "fetch" extension includes
    29 than the corresponding operations of CVS or SVN.
    29 useful sanity checks beyond raw "pull" / "update" / "merge".  Most
       
    30 other operations are local to the user's repository clone.  This gives
       
    31 some freedom for experimentation without affecting anybody else.
       
    32 
       
    33 Mercurial provides nice web presentation of incoming changes with a
       
    34 digest of log entries; this also includes RSS/Atom news feeds.  There
       
    35 are add-on browsers, notably hgtk that is part of the TortoiseHg
       
    36 distribution and works for generic Python/GTk platforms.  The
       
    37 alternative "view" utility helps to inspect the semantic content of
       
    38 merge nodes.
    30 
    39 
    31 
    40 
    32 Initial configuration
    41 Initial configuration
    33 ---------------------
    42 ---------------------
    34 
    43 
    38 
    47 
    39 This will create a local directory "isabelle", unless an alternative
    48 This will create a local directory "isabelle", unless an alternative
    40 name is specified.  The full repository meta-data and history of
    49 name is specified.  The full repository meta-data and history of
    41 changes is in isabelle/.hg; local configuration for this clone can be
    50 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
    51 added to isabelle/.hg/hgrc, but note that hgrc files are never copied
    43 by another clone operation!
    52 by another clone operation.
    44 
    53 
    45 
    54 
    46 There is also $HOME/.hgrc for per-user Mercurial configuration.  The
    55 There is also $HOME/.hgrc for per-user Mercurial configuration.  The
    47 initial configuration should include at least an entry to identify
    56 initial configuration requires at least an entry to identify yourself
    48 yourself.  For example, something like this in /home/wenzelm/.hgrc:
    57 as follows:
    49 
    58 
    50   [ui]
    59   [ui]
    51   username = wenzelm
    60   username = XXX
    52 
    61 
    53 Of course, the user identity can be also configured in
    62 Isabelle contributors are free to choose either a short "login name"
    54 isabelle/.hg/hgrc on per-repository basis.  Failing to specify the
    63 (for accounts at TU Munich) or a "full name" -- with or without mail
    55 username correctly makes the system invent funny machine names that
    64 address.  It is important to stick to this choice once and for all.
    56 may persist indefinitely in the public flow of changesets.
    65 The machine default that Mercurial produces for unspecified
    57 
    66 [ui]username is not appropriate.
    58 In principle, user names can be chosen freely, but for longterm
    67 
    59 committers of the Isabelle repository the obvious choice is to keep
    68 Such configuration can be given in $HOME/.hgrc (for each home
    60 with the old CVS naming scheme.  Others should use their regular "full
    69 directory on each machine) or in .hg/hgrc (for each repository clone).
    61 name"; including an email address is optional.
    70 
    62 
    71 
    63 
    72 Here are some further examples for hgrc.  This is how to provide
    64 There are other useful configuration to go into $HOME/.hgrc,
    73 default options for common commands:
    65 e.g. defaults for common commands:
       
    66 
    74 
    67   [defaults]
    75   [defaults]
    68   log = -l 10
    76   log = -l 10
    69 
    77 
    70 The next example shows how to install some Mercurial extension:
    78 This is how to configure some extension, which is called "graphlog"
       
    79 and provides the "glog" command:
    71 
    80 
    72   [extensions]
    81   [extensions]
    73   hgext.graphlog =
    82   hgext.graphlog =
    74 
    83 
    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 
    84 Shared pull/push access
    85 Shared pull/push access
    85 -----------------------
    86 -----------------------
    86 
    87 
    87 The entry point http://isabelle.in.tum.de/repos/isabelle is world
    88 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 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 above.  Anybody can produce a clone, change it locally, and then use
    90 use regular mechanisms of Mercurial to report changes upstream, say
    91 regular mechanisms of Mercurial to report changes upstream, say via
    91 via e-mail to someone with write access to that file space.  It is
    92 mail to someone with write access to that file space.  It is also
    92 also quite easy to publish changed clones again on the web, using the
    93 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 ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts
    94 that are included in the Mercurial distribution.
    95 that are included in the Mercurial distribution, and send a "pull
       
    96 request" to someone else.  There are also public hosting services for
       
    97 Mercurial repositories.
    95 
    98 
    96 The downstream/upstream mode of operation is quite common in the
    99 The downstream/upstream mode of operation is quite common in the
    97 distributed version control community, and works well for occasional
   100 distributed version control community, and works well for occasional
    98 changes produced by anybody out there.  Of course, upstream
   101 changes produced by anybody out there.  Of course, upstream
    99 maintainers need to review and moderate changes being proposed, before
   102 maintainers need to review and moderate changes being proposed, before
   100 pushing anything onto the official Isabelle repository at TUM.
   103 pushing anything onto the official Isabelle repository at TUM.  Direct
   101 
   104 pushes are also reviewed routinely in a post-hoc fashion; everybody
   102 
   105 hooked on the main repository is called to keep an eye on incoming
   103 Write access to the Isabelle repository requires an account at TUM,
   106 changes.  In any case, changesets need to be understandable, at the
   104 with properly configured ssh access to the local machines
   107 time of writing and many years later.
   105 (e.g. macbroy20, atbroy100).  You also need to be a member of the
   108 
   106 "isabelle" Unix group.
   109 Push access to the Isabelle repository requires an account at TUM,
       
   110 with properly configured ssh to the local machines (e.g. macbroy20,
       
   111 atbroy100).  You also need to be a member of the "isabelle" Unix
       
   112 group.
   107 
   113 
   108 Sharing a locally modified clone then works as follows, using your
   114 Sharing a locally modified clone then works as follows, using your
   109 user name instead of "wenzelm":
   115 user name instead of "wenzelm":
   110 
   116 
   111   hg out ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   117   hg out ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   115 with a lasting effect on the Isabelle repository, works like this:
   121 with a lasting effect on the Isabelle repository, works like this:
   116 
   122 
   117   hg push ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   123   hg push ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   118 
   124 
   119 
   125 
   120 Default paths for push and pull can be configure in isabelle/.hg/hgrc,
   126 Default paths for push and pull can be configured in
   121 for example:
   127 isabelle/.hg/hgrc, for example:
   122 
   128 
   123   [paths]
   129   [paths]
   124   default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   130   default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   125 
   131 
   126 Now "hg pull" or "hg push" will use that shared file space, unless a
   132 Now "hg pull" or "hg push" will use that shared file space, unless a
   131 place, to get exactly to the same point:
   137 place, to get exactly to the same point:
   132 
   138 
   133   hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   139   hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   134 
   140 
   135 
   141 
   136 Simplified merges
   142 Simple merges
   137 -----------------
   143 -------------
   138 
   144 
   139 The main idea of Mercurial is to let individual users produce
   145 The main idea of Mercurial is to let individual users produce
   140 independent branches of development first, but merge with others
   146 independent branches of development first, but merge with others
   141 frequently.  The basic hg merge operation is more general than
   147 frequently.  The basic hg merge operation is more general than
   142 required for the mode of operation with a shared pull/push area.  The
   148 required for the mode of operation with a shared pull/push area.  The
   143 hg fetch extension accommodates this case nicely, automating trivial
   149 "fetch" extension accommodates this case nicely, automating trivial
   144 merges and requiring manual intervention for actual conflicts only.
   150 merges and requiring manual intervention for actual conflicts only.
   145 
   151 
   146 The fetch extension can be configured via the user's ~/.hgrc like
   152 The fetch extension can be configured via $HOME/.hgrc like this:
   147 this:
       
   148 
   153 
   149   [extensions]
   154   [extensions]
   150   hgext.fetch =
   155   hgext.fetch =
   151 
   156 
   152   [defaults]
   157   [defaults]
   153   fetch = -m "merged"
   158   fetch = -m "merged"
   154 
   159 
   155 Note that the potential for merge conflicts can be greatly reduced by
   160 To keep merges semantically trivial and prevent genuine merge
   156 doing "hg fetch" before any starting local changes!
   161 conflicts or lost updates, it is essential to observe to following
       
   162 general discipline wrt. the public Isabelle push area:
       
   163 
       
   164   * Before editing, pull or fetch the latest version.
       
   165 
       
   166   * Accumulate private commits for a maximum of 1-3 days.
       
   167 
       
   168   * Start publishing again by pull or fetch, which normally produces
       
   169     local merges.
       
   170 
       
   171   * Test the merged result as usual and push back in real time.
       
   172 
       
   173 Piling private changes and public merges longer than 0.5-2 hours is
       
   174 apt to produce some mess when pushing eventually!
   157 
   175 
   158 
   176 
   159 Content discipline
   177 Content discipline
   160 ------------------
   178 ------------------
   161 
   179 
   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
   180 The following principles should be kept in mind when producing
   171 changesets that might become public at some point.
   181 changesets that are meant to be published at some point.
   172 
   182 
   173   * The author of changes should be properly identified, using
   183   * The author of changes needs to be properly identified, using
   174     ui/username configuration as described above.
   184     [ui]username configuration as described above.
   175 
   185 
   176     While Mercurial also provides means for signed changesets, we want
   186     While Mercurial also provides means for signed changesets, we want
   177     to keep things simple and trust that users specify their identity
   187     to keep things simple and trust that users specify their identity
   178     correctly.
   188     correctly (and uniquely).
   179 
   189 
   180   * The history of sources is an integral part of the sources
   190   * The history of sources is an integral part of the sources
   181     themselves.  This means that private experiments and branches
   191     themselves.  This means that private experiments and branches
   182     should not be published, unless they are really meant to become
   192     should not be published by accident.  Named branches are not
   183     universally available.
   193     allowed on the public version.  Note that old SVN-style branching
   184 
   194     is replaced by regular repository clones in Mercurial.
   185     Note that exchanging local experiments with some other users can
   195 
   186     be done directly on peer-to-peer basis, without affecting the
   196     Exchanging local experiments with some other users can be done
   187     central pull/push area.
   197     directly on peer-to-peer basis, without affecting the central
       
   198     pull/push area.
   188 
   199 
   189   * Log messages are an integral part of the history of sources.
   200   * Log messages are an integral part of the history of sources.
   190     Other users will have to look there eventually, to understand why
   201     Other people will have to inspect them routinely, to understand
   191     things have been done in a certain way at some point.
   202     why things have been done in a certain way at some point.
   192 
   203 
   193     Mercurial provides nice web presentation of incoming changes with
   204     Authors of log entries should be aware that published changes are
   194     a digest of log entries; this also includes RSS/Atom news feeds.
   205     actually read.  The main point is not to announce novelties, but
   195     Users should be aware that others will actually read what is
   206     to describe faithfully what has been done, and provide some clues
   196     written into log messages.  There are also add-on browsers,
   207     about the motivation behind it.  The main recipient is someone who
   197     notably hgtk that is part of the TortoiseHg distribution and works
   208     needs to understand the change in the distant future to isolate
   198     for generic Python/GTk platforms.
   209     problems.  Sometimes it is helpful to reference past changes via
   199 
   210     changeset ids in the log entry.
   200     The usual changelog presentation style for the Isabelle repository
   211 
   201     admits log entries that consist of several lines, but without the
   212   * The standard changelog entry format of the Isabelle repository
   202     special headline that is used in Mercurial projects elsewhere.
   213     admits several (vaguely related) items to be rolled into one
   203     Since some display styles strip newlines from text, it is
   214     changeset.  Each item is then described on a separate line that
   204     advisable to separate lines via punctuation, and not rely on
   215     may become longer as screen line and is terminated by punctuation.
   205     two-dimensional presentation too much.
   216     These lines are roughly ordered by importance.
       
   217 
       
   218     This format conforms to established Isabelle tradition.  In
       
   219     contrast, the default of Mercurial prefers a single headline
       
   220     followed by a long body text.  The reason for that is a somewhat
       
   221     different development model of typical "distributed" projects,
       
   222     where external changes pass through a hierarchy of reviewers and
       
   223     maintainers, until they end up in some authoritative repository.
       
   224     Isabelle changesets can be more spontaneous, growing from the
       
   225     bottom-up.
       
   226 
       
   227     The web style of http://isabelle.in.tum.de/repos/isabelle/
       
   228     accommodates the Isabelle changelog format.  Note that multiple
       
   229     lines will sometimes display as a single paragraph in HTML, so
       
   230     some terminating punctuation is required.  Do not squeeze multiple
       
   231     items on the same line in the original text!
   206 
   232 
   207 
   233 
   208 Building a repository version of Isabelle
   234 Building a repository version of Isabelle
   209 -----------------------------------------
   235 -----------------------------------------
   210 
   236 
   211 Compared to a proper distribution or development snapshot, a
   237 Compared to a proper distribution or development snapshot, it is
   212 repository version of Isabelle lacks textual version identifiers in
   238 relatively hard to build from the raw repository version.  Essential
   213 some sources and scripts, and various components produced by
   239 contributing components are missing and need to be reconstructed by
   214 Admin/build are missing.  After applying that script with suitable
   240 running the Admin/build script by hand.  Afterwards the main Isabelle
   215 arguments, the regular user instructions for building and running
   241 system and logic images can be compiled via the toplevel ./build
   216 Isabelle from sources apply.
   242 script.  Note that the repository lacks some textual version
   217 
   243 identifiers in the sources and scripts; this implies some changed
   218 Needless to say, the results from the build process must not be added
   244 behavior when processing settings etc.
   219 to the repository!
   245 
       
   246 There is no guarantee that the NEWS file is up to date at an arbitrary
       
   247 point in history.