README_REPOSITORY
author wenzelm
Thu, 22 Apr 2021 23:40:22 +0200
changeset 73858 37243ad3ecb6
parent 73846 1aa9ef7a3eaf
permissions -rw-r--r--
fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
     1
Important notes on Mercurial repository access for Isabelle
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
     2
===========================================================
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
     3
54963
wenzelm
parents: 53359
diff changeset
     4
Quick start in 30min
49348
01d2d01bf9d1 instructions for quick start in 20min;
wenzelm
parents: 48986
diff changeset
     5
--------------------
01d2d01bf9d1 instructions for quick start in 20min;
wenzelm
parents: 48986
diff changeset
     6
73434
wenzelm
parents: 71800
diff changeset
     7
1. Platform prerequisites: ensure that "curl" and "hg" (Mercurial) are installed
wenzelm
parents: 71800
diff changeset
     8
wenzelm
parents: 71800
diff changeset
     9
  (a) Linux: e.g. "sudo apt install curl mercurial
49348
01d2d01bf9d1 instructions for quick start in 20min;
wenzelm
parents: 48986
diff changeset
    10
73434
wenzelm
parents: 71800
diff changeset
    11
  (b) macOS: e.g. "brew install mercurial" or download from https://www.mercurial-scm.org
49348
01d2d01bf9d1 instructions for quick start in 20min;
wenzelm
parents: 48986
diff changeset
    12
73434
wenzelm
parents: 71800
diff changeset
    13
  (c) Windows: use Cygwin64 with packages "curl" and "mercurial" (via Cygwin setup-x86_64.exe)
wenzelm
parents: 71800
diff changeset
    14
73769
01acd0eb29ce clarified name;
wenzelm
parents: 73759
diff changeset
    15
2. Initial repository clone (bash shell commands):
49348
01d2d01bf9d1 instructions for quick start in 20min;
wenzelm
parents: 48986
diff changeset
    16
67744
5c781dcd5864 prefer https;
wenzelm
parents: 66763
diff changeset
    17
    hg clone https://isabelle.in.tum.de/repos/isabelle
73769
01acd0eb29ce clarified name;
wenzelm
parents: 73759
diff changeset
    18
    isabelle/Admin/init
49348
01d2d01bf9d1 instructions for quick start in 20min;
wenzelm
parents: 48986
diff changeset
    19
73769
01acd0eb29ce clarified name;
wenzelm
parents: 73759
diff changeset
    20
3. Switch repository to particular version (bash shell commands):
50281
cbba16084784 further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents: 49443
diff changeset
    21
73840
1d4c9fa00821 clarified options;
wenzelm
parents: 73771
diff changeset
    22
    #latest official release
1d4c9fa00821 clarified options;
wenzelm
parents: 73771
diff changeset
    23
    isabelle/Admin/init -R
1d4c9fa00821 clarified options;
wenzelm
parents: 73771
diff changeset
    24
73845
479e9b17090e clarified options (again);
wenzelm
parents: 73841
diff changeset
    25
    #latest version from repository server
479e9b17090e clarified options (again);
wenzelm
parents: 73841
diff changeset
    26
    isabelle/Admin/init -u
73840
1d4c9fa00821 clarified options;
wenzelm
parents: 73771
diff changeset
    27
73845
479e9b17090e clarified options (again);
wenzelm
parents: 73841
diff changeset
    28
    #latest version from local history
479e9b17090e clarified options (again);
wenzelm
parents: 73841
diff changeset
    29
    isabelle/Admin/init -u -L
73753
f5e9ade80579 clarified;
wenzelm
parents: 73742
diff changeset
    30
f5e9ade80579 clarified;
wenzelm
parents: 73742
diff changeset
    31
    #explicit changeset id or tag (e.g. "Isabelle2021")
73846
1aa9ef7a3eaf updated example;
wenzelm
parents: 73845
diff changeset
    32
    isabelle/Admin/init -r 479e9b17090e
73753
f5e9ade80579 clarified;
wenzelm
parents: 73742
diff changeset
    33
73759
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73758
diff changeset
    34
4. Run application:
50575
ae1da46022d1 prefer implicit build_dialog of isabelle jedit;
wenzelm
parents: 50457
diff changeset
    35
73759
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73758
diff changeset
    36
    #start Prover IDE and let it build session image
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73758
diff changeset
    37
    isabelle/bin/isabelle jedit -l HOL
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73758
diff changeset
    38
73771
wenzelm
parents: 73769
diff changeset
    39
    #alternative: build session image separately
73759
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73758
diff changeset
    40
    isabelle/bin/isabelle build -b HOL
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73758
diff changeset
    41
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73758
diff changeset
    42
5. Build documentation (bash shell commands):
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
    43
73758
eda1d95ef538 misc tuning and clarification;
wenzelm
parents: 73754
diff changeset
    44
    isabelle/bin/isabelle build_doc -a
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
    45
73758
eda1d95ef538 misc tuning and clarification;
wenzelm
parents: 73754
diff changeset
    46
    isabelle/bin/isabelle doc system
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
    47
49348
01d2d01bf9d1 instructions for quick start in 20min;
wenzelm
parents: 48986
diff changeset
    48
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    49
Introduction
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    50
------------
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    51
68379
22680a3f8346 updated URLs;
wenzelm
parents: 67744
diff changeset
    52
Mercurial https://www.mercurial-scm.org belongs to source code
63985
wenzelm
parents: 63490
diff changeset
    53
management systems that follow the so-called paradigm of "distributed
71800
wenzelm
parents: 68379
diff changeset
    54
version control".  This means plain versioning without the legacy of
wenzelm
parents: 68379
diff changeset
    55
SVN and the extra complexity of GIT.  See also
wenzelm
parents: 68379
diff changeset
    56
https://www.mercurial-scm.org/learn
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    57
63985
wenzelm
parents: 63490
diff changeset
    58
Mercurial offers some flexibility in organizing the flow of changes,
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    59
both between individual developers and designated pull/push areas that
63985
wenzelm
parents: 63490
diff changeset
    60
are shared with others.  This additional freedom demands additional
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    61
responsibility to maintain a certain development process that fits to
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    62
a particular project.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    63
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    64
Regular Mercurial operations are strictly monotonic, where changeset
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
    65
transactions are only added, but never deleted or mutated.  There are
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
    66
special tools to manipulate repositories via non-monotonic actions
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
    67
(such as "rollback" or "strip"), but recovering from gross mistakes
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
    68
that have escaped into the public can be hard and embarrassing.  It is
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
    69
much easier to inspect and amend changesets routinely before pushing.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    70
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    71
The effect of the critical "pull" / "push" operations can be tested in
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    72
a dry run via "incoming" / "outgoing".  The "fetch" extension includes
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
    73
useful sanity checks beyond raw "pull" / "update" / "merge", although
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
    74
it has lost popularity in recent years.  Most other operations are
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
    75
local to the user's repository clone.  This gives some freedom for
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
    76
experimentation without affecting anybody else.
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    77
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    78
Mercurial provides nice web presentation of incoming changes with a
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    79
digest of log entries; this also includes RSS/Atom news feeds.  There
47449
5e1482296b12 misc tuning;
wenzelm
parents: 40601
diff changeset
    80
are add-on history browsers such as "hg view" and TortoiseHg.  Unlike
5e1482296b12 misc tuning;
wenzelm
parents: 40601
diff changeset
    81
the default web view, some of these tools help to inspect the semantic
5e1482296b12 misc tuning;
wenzelm
parents: 40601
diff changeset
    82
content of non-trivial merge nodes.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    83
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    84
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    85
Initial configuration
29481
3e8420c1124a tuned ASCII art;
wenzelm
parents: 28918
diff changeset
    86
---------------------
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    87
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
    88
The main Isabelle repository can be cloned like this:
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    89
67744
5c781dcd5864 prefer https;
wenzelm
parents: 66763
diff changeset
    90
  hg clone https://isabelle.in.tum.de/repos/isabelle
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    91
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    92
This will create a local directory "isabelle", unless an alternative
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    93
name is specified.  The full repository meta-data and history of
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    94
changes is in isabelle/.hg; local configuration for this clone can be
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    95
added to isabelle/.hg/hgrc, but note that hgrc files are never copied
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    96
by another clone operation.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    97
28917
wenzelm
parents: 28913
diff changeset
    98
28913
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
    99
There is also $HOME/.hgrc for per-user Mercurial configuration.  The
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   100
initial configuration requires at least an entry to identify yourself
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   101
as follows:
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   102
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   103
  [ui]
71800
wenzelm
parents: 68379
diff changeset
   104
  username = ABC
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   105
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   106
Isabelle contributors are free to choose either a short "login name"
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   107
(for accounts at TU Munich) or a "full name" -- with or without mail
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   108
address.  It is important to stick to this choice once and for all.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   109
The machine default that Mercurial produces for unspecified
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   110
[ui]username is not appropriate.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   111
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   112
Such configuration can be given in $HOME/.hgrc (for each home
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   113
directory on each machine) or in .hg/hgrc (for each repository clone).
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   114
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   115
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   116
Here are some further examples for hgrc.  This is how to provide
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   117
default options for common commands:
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   118
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   119
  [defaults]
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   120
  log = -l 10
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   121
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   122
This is how to configure some extension, which is called "graphlog"
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   123
and provides the "glog" command:
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   124
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   125
  [extensions]
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   126
  hgext.graphlog =
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   127
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   128
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   129
Shared pull/push access
29481
3e8420c1124a tuned ASCII art;
wenzelm
parents: 28918
diff changeset
   130
-----------------------
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   131
67744
5c781dcd5864 prefer https;
wenzelm
parents: 66763
diff changeset
   132
The entry point https://isabelle.in.tum.de/repos/isabelle is world
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   133
readable, both via plain web browsing and the hg client as described
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   134
above.  Anybody can produce a clone, change it locally, and then use
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   135
regular mechanisms of Mercurial to report changes upstream, say via
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   136
mail to someone with write access to that file space.  It is also
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   137
quite easy to publish changed clones again on the web, using the
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   138
ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   139
that are included in the Mercurial distribution, and send a "pull
71800
wenzelm
parents: 68379
diff changeset
   140
request" to someone else.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   141
28913
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   142
The downstream/upstream mode of operation is quite common in the
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   143
distributed version control community, and works well for occasional
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   144
changes produced by anybody out there.  Of course, upstream
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   145
maintainers need to review and moderate changes being proposed, before
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   146
pushing anything onto the official Isabelle repository at TUM.  Direct
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   147
pushes are also reviewed routinely in a post-hoc fashion; everybody
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   148
hooked on the main repository is called to keep an eye on incoming
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   149
changes.  In any case, changesets need to be understandable, both at
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   150
the time of writing and many years later.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   151
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   152
Push access to the Isabelle repository requires an account at TUM,
51072
0351cc781a26 standardized isabelle-server.in.tum.de;
wenzelm
parents: 50654
diff changeset
   153
with properly configured ssh to isabelle-server.in.tum.de.  You also
0351cc781a26 standardized isabelle-server.in.tum.de;
wenzelm
parents: 50654
diff changeset
   154
need to be a member of the "isabelle" Unix group.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   155
28913
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   156
Sharing a locally modified clone then works as follows, using your
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   157
user name instead of "wenzelm":
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   158
51072
0351cc781a26 standardized isabelle-server.in.tum.de;
wenzelm
parents: 50654
diff changeset
   159
  hg out ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   160
28913
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   161
In fact, the "out" or "outgoing" command performs only a dry run: it
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   162
displays the changesets that would get published.  An actual "push",
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   163
with a lasting effect on the Isabelle repository, works like this:
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   164
51072
0351cc781a26 standardized isabelle-server.in.tum.de;
wenzelm
parents: 50654
diff changeset
   165
  hg push ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
28913
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   166
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   167
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   168
Default paths for push and pull can be configured in
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   169
isabelle/.hg/hgrc, for example:
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   170
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   171
  [paths]
51072
0351cc781a26 standardized isabelle-server.in.tum.de;
wenzelm
parents: 50654
diff changeset
   172
  default = ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   173
28913
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   174
Now "hg pull" or "hg push" will use that shared file space, unless a
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   175
different URL is specified explicitly.
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   176
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   177
When cloning a repository, the default path is set to the initial
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   178
source URL.  So we could have cloned via that ssh URL in the first
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   179
place, to get exactly to the same point:
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   180
51072
0351cc781a26 standardized isabelle-server.in.tum.de;
wenzelm
parents: 50654
diff changeset
   181
  hg clone ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   182
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   183
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   184
Simple merges
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   185
-------------
30182
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   186
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   187
The main idea of Mercurial is to let individual users produce
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   188
independent branches of development first, but merge with others
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   189
frequently.  The basic hg merge operation is more general than
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   190
required for the mode of operation with a shared pull/push area.  The
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   191
"fetch" extension accommodates this case nicely, automating trivial
30182
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   192
merges and requiring manual intervention for actual conflicts only.
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   193
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   194
The fetch extension can be configured via $HOME/.hgrc like this:
30182
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   195
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   196
  [extensions]
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   197
  hgext.fetch =
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   198
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   199
  [defaults]
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   200
  fetch = -m "merged"
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   201
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   202
To keep merges semantically trivial and prevent genuine merge
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   203
conflicts or lost updates, it is essential to observe to following
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   204
general discipline wrt. the public Isabelle push area:
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   205
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   206
  * Before editing, pull or fetch the latest version.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   207
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   208
  * Accumulate private commits for a maximum of 1-3 days.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   209
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   210
  * Start publishing again by pull or fetch, which normally produces
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   211
    local merges.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   212
50281
cbba16084784 further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents: 49443
diff changeset
   213
  * Test the merged result, e.g. like this:
cbba16084784 further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents: 49443
diff changeset
   214
cbba16084784 further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents: 49443
diff changeset
   215
      isabelle build -a
cbba16084784 further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents: 49443
diff changeset
   216
cbba16084784 further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents: 49443
diff changeset
   217
  * Push back in real time.
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   218
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   219
Piling private changes and public merges longer than 0.5-2 hours is
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   220
apt to produce some mess when pushing eventually!
30182
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   221
50281
cbba16084784 further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents: 49443
diff changeset
   222
The pull-test-push cycle should not be repeated too fast, to avoid
cbba16084784 further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents: 49443
diff changeset
   223
delaying others from doing the same concurrently.
cbba16084784 further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents: 49443
diff changeset
   224
30182
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   225
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   226
Content discipline
29481
3e8420c1124a tuned ASCII art;
wenzelm
parents: 28918
diff changeset
   227
------------------
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   228
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   229
The following principles should be kept in mind when producing
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   230
changesets that are meant to be published at some point.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   231
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   232
  * The author of changes needs to be properly identified, using
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   233
    [ui]username configuration as described above.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   234
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   235
    While Mercurial also provides means for signed changesets, we want
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   236
    to keep things simple and trust that users specify their identity
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   237
    correctly (and uniquely).
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   238
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   239
  * The history of sources is an integral part of the sources
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   240
    themselves.  This means that private experiments and branches
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   241
    should not be published by accident.  Named branches are not
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   242
    allowed on the public version.  Note that old SVN-style branching
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   243
    is replaced by regular repository clones in Mercurial.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   244
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   245
    Exchanging local experiments with some other users can be done
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   246
    directly on peer-to-peer basis, without affecting the central
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   247
    pull/push area.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   248
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   249
  * Log messages are an integral part of the history of sources.
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   250
    Other people will have to inspect them routinely, to understand
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   251
    why things have been done in a certain way at some point.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   252
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   253
    Authors of log entries should be aware that published changes are
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   254
    actually read.  The main point is not to announce novelties, but
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   255
    to describe faithfully what has been done, and provide some clues
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   256
    about the motivation behind it.  The main recipient is someone who
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   257
    needs to understand the change in the distant future to isolate
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   258
    problems.  Sometimes it is helpful to reference past changes
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   259
    formally via changeset ids in the log entry.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   260
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   261
  * The standard changelog entry format of the Isabelle repository
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   262
    admits several (somehow related) items to be rolled into one
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   263
    changeset.  Each item is then described on a separate line that
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   264
    may become longer as screen line and is terminated by punctuation.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   265
    These lines are roughly ordered by importance.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   266
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   267
    This format conforms to established Isabelle tradition.  In
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   268
    contrast, the default of Mercurial prefers a single headline
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   269
    followed by a long body text.  The reason for that is a somewhat
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   270
    different development model of typical "distributed" projects,
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   271
    where external changes pass through a hierarchy of reviewers and
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   272
    maintainers, until they end up in some authoritative repository.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   273
    Isabelle changesets can be more spontaneous, growing from the
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   274
    bottom-up.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   275
67744
5c781dcd5864 prefer https;
wenzelm
parents: 66763
diff changeset
   276
    The web style of https://isabelle.in.tum.de/repos/isabelle
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   277
    accommodates the Isabelle changelog format.  Note that multiple
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   278
    lines will sometimes display as a single paragraph in HTML, so
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   279
    some terminating punctuation is required.  Do not squeeze multiple
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   280
    items on the same line in the original text!
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   281
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   282
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   283
Testing of changes (before push)
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   284
--------------------------------
48497
ba61aceaa18a some updates on "Building a repository version of Isabelle";
wenzelm
parents: 47449
diff changeset
   285
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   286
The integrity of the standard pull/push area of Isabelle needs the be
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   287
preserved at all time.  This means that a complete test with default
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   288
configuration needs to be finished successfully before push.  If the
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   289
preparation of the push involves a pull/merge phase, its result needs
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   290
to covered by the test as well.
28908
4571302e1594 further notes;
wenzelm
parents: 28907
diff changeset
   291
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   292
There are several possibilities to perform the test, e.g. using the
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   293
Isabelle testboard at TUM.  In contrast, the subsequent command-line
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   294
examples are for tests on the local machine:
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48497
diff changeset
   295
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   296
  ./bin/isabelle build -a  #regular test
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48497
diff changeset
   297
63985
wenzelm
parents: 63490
diff changeset
   298
  ./bin/isabelle build -a -o document=pdf  #test with document preparation (optional)
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48497
diff changeset
   299
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   300
  ./bin/isabelle build -a -j2 -o threads=4  #test on multiple cores (example)
48497
ba61aceaa18a some updates on "Building a repository version of Isabelle";
wenzelm
parents: 47449
diff changeset
   301
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   302
See also the chapter on Isabelle sessions and build management in the
66753
f7759beab4f2 more documentation;
wenzelm
parents: 63985
diff changeset
   303
"system" manual. The build option -S is particularly useful for quick
f7759beab4f2 more documentation;
wenzelm
parents: 63985
diff changeset
   304
tests of individual commits, e.g. for each step of a longer chain of
f7759beab4f2 more documentation;
wenzelm
parents: 63985
diff changeset
   305
changes, but the final push always requires a full test as above!
48986
037d32448e29 update on "isabelle build" and "isabelle build_doc";
wenzelm
parents: 48855
diff changeset
   306
51502
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   307
Note that implicit dependencies on Isabelle components are specified
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   308
via catalog files in $ISABELLE_HOME/Admin/components/ as part of the
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   309
Mercurial history.  This allows to bisect over a range of Isabelle
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   310
versions while references to the contributing components change
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   311
accordingly.  Recall that "isabelle components -a" updates the local
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   312
component store monotonically according to that information, and thus
ed5d96d01b2f more "quick start" hints;
wenzelm
parents: 51072
diff changeset
   313
resolves missing components.