README_REPOSITORY

clarified tests: omit somewhat pointless (unstable) results;

Important notes on Mercurial repository access for Isabelle
===========================================================

Quick start in 30min
--------------------

1. Platform prerequisites: ensure that "curl" and "hg" (Mercurial) are installed

  (a) Linux: e.g. "sudo apt install curl mercurial

  (b) macOS: e.g. "brew install mercurial" or download from https://www.mercurial-scm.org

  (c) Windows: use Cygwin64 with packages "curl" and "mercurial" (via Cygwin setup-x86_64.exe)

2. Initial repository clone (bash shell commands):

    hg clone https://isabelle.in.tum.de/repos/isabelle
    isabelle/Admin/init

3. Switch repository to particular version (bash shell commands):

    #latest official release
    isabelle/Admin/init -R

    #latest version from repository server
    isabelle/Admin/init -u

    #latest version from local history
    isabelle/Admin/init -u -L

    #explicit changeset id or tag (e.g. "Isabelle2021")
    isabelle/Admin/init -r 479e9b17090e

4. Run application:

    #start Prover IDE and let it build session image
    isabelle/bin/isabelle jedit -l HOL

    #alternative: build session image separately
    isabelle/bin/isabelle build -b HOL

5. Build documentation (bash shell commands):

    isabelle/bin/isabelle build_doc -a

    isabelle/bin/isabelle doc system


Introduction
------------

Mercurial https://www.mercurial-scm.org belongs to source code
management systems that follow the so-called paradigm of "distributed
version control".  This means plain versioning without the legacy of
SVN and the extra complexity of GIT.  See also
https://www.mercurial-scm.org/learn

Mercurial offers some flexibility in organizing the flow of changes,
both between individual developers and designated pull/push areas that
are shared with others.  This additional freedom demands additional
responsibility to maintain a certain development process that fits to
a particular project.

Regular Mercurial operations are strictly monotonic, where changeset
transactions are only added, but never deleted or mutated.  There are
special tools to manipulate repositories via non-monotonic actions
(such as "rollback" or "strip"), but recovering from gross mistakes
that have escaped into the public can be hard and embarrassing.  It is
much easier to inspect and amend changesets routinely before pushing.

The effect of the critical "pull" / "push" operations can be tested in
a dry run via "incoming" / "outgoing".  The "fetch" extension includes
useful sanity checks beyond raw "pull" / "update" / "merge", although
it has lost popularity in recent years.  Most other operations are
local to the user's repository clone.  This gives some freedom for
experimentation without affecting anybody else.

Mercurial provides nice web presentation of incoming changes with a
digest of log entries; this also includes RSS/Atom news feeds.  There
are add-on history browsers such as "hg view" and TortoiseHg.  Unlike
the default web view, some of these tools help to inspect the semantic
content of non-trivial merge nodes.


Initial configuration
---------------------

The main Isabelle repository can be cloned like this:

  hg clone https://isabelle.in.tum.de/repos/isabelle

This will create a local directory "isabelle", unless an alternative
name is specified.  The full repository meta-data and history of
changes is in isabelle/.hg; local configuration for this clone can be
added to isabelle/.hg/hgrc, but note that hgrc files are never copied
by another clone operation.


There is also $HOME/.hgrc for per-user Mercurial configuration.  The
initial configuration requires at least an entry to identify yourself
as follows:

  [ui]
  username = ABC

Isabelle contributors are free to choose either a short "login name"
(for accounts at TU Munich) or a "full name" -- with or without mail
address.  It is important to stick to this choice once and for all.
The machine default that Mercurial produces for unspecified
[ui]username is not appropriate.

Such configuration can be given in $HOME/.hgrc (for each home
directory on each machine) or in .hg/hgrc (for each repository clone).


Here are some further examples for hgrc.  This is how to provide
default options for common commands:

  [defaults]
  log = -l 10

This is how to configure some extension, which is called "graphlog"
and provides the "glog" command:

  [extensions]
  hgext.graphlog =


Shared pull/push access
-----------------------

The entry point https://isabelle.in.tum.de/repos/isabelle is world
readable, both via plain web browsing and the hg client as described
above.  Anybody can produce a clone, change it locally, and then use
regular mechanisms of Mercurial to report changes upstream, say via
mail to someone with write access to that file space.  It is also
quite easy to publish changed clones again on the web, using the
ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts
that are included in the Mercurial distribution, and send a "pull
request" to someone else.

The downstream/upstream mode of operation is quite common in the
distributed version control community, and works well for occasional
changes produced by anybody out there.  Of course, upstream
maintainers need to review and moderate changes being proposed, before
pushing anything onto the official Isabelle repository at TUM.  Direct
pushes are also reviewed routinely in a post-hoc fashion; everybody
hooked on the main repository is called to keep an eye on incoming
changes.  In any case, changesets need to be understandable, both at
the time of writing and many years later.

Push access to the Isabelle repository requires an account at TUM,
with properly configured ssh to isabelle-server.in.tum.de.  You also
need to be a member of the "isabelle" Unix group.

Sharing a locally modified clone then works as follows, using your
user name instead of "wenzelm":

  hg out ssh://[e-mail]//home/isabelle-repository/repos/isabelle

In fact, the "out" or "outgoing" command performs only a dry run: it