# HG changeset patch # User wenzelm # Date 1616873044 -3600 # Node ID 47f055b40ab9a8aaa706e974872ea00a8c536655 # Parent 1a6637572b708b0102d1f321bb39e3a365c8796d more convenient repository setup; diff -r 1a6637572b70 -r 47f055b40ab9 README_REPOSITORY --- a/README_REPOSITORY Sat Mar 27 19:46:02 2021 +0100 +++ b/README_REPOSITORY Sat Mar 27 20:24:04 2021 +0100 @@ -18,25 +18,17 @@ cd isabelle - ./bin/isabelle components -I - - ./bin/isabelle components -a + ./bin/isabelle setup - ./bin/isabelle jedit -l HOL + ./bin/isabelle jedit -l HOL #start Prover IDE and let it build session image - ./bin/isabelle build -b HOL #optional: build session image manually + ./bin/isabelle build -b HOL #alternative: build session image manually 3. Update repository to particular version (bash shell commands): cd isabelle - hg pull https://isabelle.in.tum.de/repos/isabelle - - hg update -r VERSION #for VERSION e.g. "tip", "Isabelle2021", "9e967acf8f0f" - - ./bin/isabelle components -a - - ./bin/isabelle jedit -l HOL + ./bin/isabelle -r VERSION #for VERSION e.g. "tip", "Isabelle2021", "9e967acf8f0f" 4. Build documentation (bash shell commands): diff -r 1a6637572b70 -r 47f055b40ab9 lib/Tools/setup --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/Tools/setup Sat Mar 27 20:24:04 2021 +0100 @@ -0,0 +1,110 @@ +#!/usr/bin/env bash +# +# Author: Makarius +# +# DESCRIPTION: setup for Isabelle repository clone or repository archive + + +## diagnostics + +PRG="$(basename "$0")" + +function usage() +{ + echo + echo "Usage: isabelle $PRG [OPTIONS]" + echo + echo " Options are:" + echo " -r REV explicit Mercurial version" + echo " -V PATH version from explicit file or directory (file \"ISABELLE_VERSION\")" + echo + echo " Setup the current ISABELLE_HOME directory, which needs to be a" + echo " repository clone (all versions) or repository archive (fixed version)." + echo + exit 1 +} + +function fail() +{ + echo "$1" >&2 + exit 2 +} + + +## process command line + +#options + +VERSION_REV="" +VERSION_PATH="" + +while getopts "r:V:" OPT +do + case "$OPT" in + r) + VERSION_REV="$OPTARG" + ;; + V) + VERSION_PATH="$OPTARG" + ;; + \?) + usage + ;; + esac +done + +shift $(($OPTIND - 1)) + + +# args + +[ "$#" -ne 0 ] && usage + + +## main + +if [ -z "$VERSION_REV" -a -z "$VERSION_PATH" ]; then + isabelle components -I && isabelle components -a +elif [ -n "$VERSION_REV" -a -n "$VERSION_PATH" ]; then + fail "Duplicate version specification (options -r and -V)" +elif [ ! -d "$ISABELLE_HOME/.hg" ]; then + fail "Not a repository clone: cannot specify version" +else + export REV="" + if [ -n "$VERSION_REV" ]; then + REV="$VERSION_REV" + elif [ -f "$VERSION_PATH" ]; then + REV="$(cat "$VERSION_PATH")" + elif [ -d "$VERSION_PATH" ]; then + if [ -f "$VERSION_PATH/ISABELLE_VERSION" ]; then + REV="$(cat "$VERSION_PATH/ISABELLE_VERSION")" + else + fail "Missing file \"$VERSION_PATH/ISABELLE_VERSION\"" + fi + else + fail "Missing file \"$VERSION_PATH\"" + fi + + export LANG=C + export HGPLAIN= + + if "${HG:-hg}" id -r "$REV" >/dev/null 2>/dev/null + then + export PULL="" + else + export PULL=true + fi + + isabelle components -I + + #Atomic exec: avoid inplace update of running script! + exec bash -c ' + set -e + if [ -n "$PULL" ]; then + "${HG:-hg}" pull -r "$REV" + fi + "${HG:-hg}" update -r "$REV" + "${HG:-hg}" log -r "$REV" + isabelle components -a + ' +fi