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