--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/init Wed Mar 31 11:05:40 2021 +0200
@@ -0,0 +1,167 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: initialize Isabelle repository clone or repository archive
+
+
+## environment
+
+export ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
+
+ISABELLE_REPOS="https://isabelle.sketis.net/repos/isabelle"
+
+
+## diagnostics
+
+function usage()
+{
+ echo
+ echo "Usage: Admin/init [OPTIONS]"
+ echo
+ echo " Options are:"
+ echo " -C force clean working directory (no backup!)"
+ echo " -R version is current official release"
+ echo " -U URL Isabelle repository server (default: \"$ISABELLE_REPOS\")"
+ echo " -V PATH version from explicit file or directory (file \"ISABELLE_VERSION\")"
+ echo " -c check clean working directory"
+ echo " -f fresh build of Isabelle/Scala/jEdit"
+ echo " -n no build of Isabelle/Scala/jEdit"
+ echo " -r REV version according to Mercurial notation"
+ echo " -u version is tip (after pull from Isabelle repository server)"
+ echo
+ echo " Initialize the current ISABELLE_HOME directory, which needs to be a"
+ echo " repository clone (all versions) or repository archive (fixed version)."
+ echo " Download required components and build Isabelle/Scala/jEdit (default)."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+#options
+
+BUILD_OPTIONS="-b"
+
+CLEAN_FORCE=""
+CLEAN_CHECK=""
+
+VERSION=""
+VERSION_RELEASE=""
+VERSION_PATH=""
+VERSION_REV=""
+
+while getopts "CRU:V:cfnr:u" OPT
+do
+ case "$OPT" in
+ C)
+ CLEAN_FORCE="--clean"
+ ;;
+ R)
+ VERSION="true"
+ VERSION_RELEASE="true"
+ VERSION_PATH=""
+ VERSION_REV=""
+ ;;
+ U)
+ ISABELLE_REPOS="$OPTARG"
+ ;;
+ V)
+ VERSION="true"
+ VERSION_RELEASE=""
+ VERSION_PATH="$OPTARG"
+ VERSION_REV=""
+ ;;
+ c)
+ CLEAN_CHECK="--check"
+ ;;
+ f)
+ BUILD_OPTIONS="-b -f"
+ ;;
+ n)
+ BUILD_OPTIONS=""
+ ;;
+ r)
+ VERSION="true"
+ VERSION_RELEASE=""
+ VERSION_PATH=""
+ VERSION_REV="$OPTARG"
+ ;;
+ u)
+ VERSION="true"
+ VERSION_RELEASE=""
+ VERSION_PATH=""
+ VERSION_REV="tip"
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ "$#" -ne 0 ] && usage
+
+
+## main
+
+if [ -z "$VERSION" ]; then
+ "$ISABELLE_HOME/bin/isabelle" components -I || exit "?$"
+ "$ISABELLE_HOME/bin/isabelle" components -a || exit "?$"
+ if [ -n "$BUILD_OPTIONS" ]; then
+ "$ISABELLE_HOME/bin/isabelle" jedit $BUILD_OPTIONS
+ fi
+elif [ ! -d "$ISABELLE_HOME/.hg" ]; then
+ fail "Not a repository clone: cannot specify version"
+else
+ if [ -n "$VERSION_REV" ]; then
+ REV="$VERSION_REV"
+ elif [ -n "$VERSION_RELEASE" ]; then
+ URL="$ISABELLE_REPOS/raw-file/tip/Admin/Release/official"
+ REV="$(curl -s -f "$URL" | head -n1)"
+ [ -z "$REV" ] && fail "Failed to access \"$URL\""
+ 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
+
+ "$ISABELLE_HOME/bin/isabelle" components -I || exit "$?"
+
+ export LANG=C
+ export HGPLAIN=
+
+ #Atomic exec: avoid inplace update of running script!
+ export CLEAN_FORCE CLEAN_CHECK REV ISABELLE_REPOS BUILD_OPTIONS
+ exec bash -c '
+ set -e
+ "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" "$ISABELLE_REPOS"
+ "${HG:-hg}" -R "$ISABELLE_HOME" update -r "$REV" $CLEAN_FORCE $CLEAN_CHECK
+ "$ISABELLE_HOME/bin/isabelle" components -a
+ if [ -n "$BUILD_OPTIONS" ]; then
+ "$ISABELLE_HOME/bin/isabelle" jedit $BUILD_OPTIONS
+ fi
+ "${HG:-hg}" -R "$ISABELLE_HOME" log -r "$REV"
+ if [ ! -f "$ISABELLE_HOME/Admin/init" ]; then
+ echo >&2 "### The Admin/init script has disappeared in this version"
+ echo >&2 "### (need to invoke \"${HG:-hg} update\" before using it again)"
+ fi
+ '
+fi
--- a/Admin/setup Wed Mar 31 10:57:18 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,167 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: setup for Isabelle repository clone or repository archive
-
-
-## environment
-
-export ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
-
-ISABELLE_REPOS="https://isabelle.sketis.net/repos/isabelle"
-
-
-## diagnostics
-
-function usage()
-{
- echo
- echo "Usage: Admin/setup [OPTIONS]"
- echo
- echo " Options are:"
- echo " -C force clean working directory (no backup!)"
- echo " -R version is current official release"
- echo " -U URL Isabelle repository server (default: \"$ISABELLE_REPOS\")"
- echo " -V PATH version from explicit file or directory (file \"ISABELLE_VERSION\")"
- echo " -c check clean working directory"
- echo " -f fresh build of Isabelle/Scala/jEdit"
- echo " -n no build of Isabelle/Scala/jEdit"
- echo " -r REV version according to Mercurial notation"
- echo " -u version is tip (after pull from Isabelle repository server)"
- echo
- echo " Setup the current ISABELLE_HOME directory, which needs to be a"
- echo " repository clone (all versions) or repository archive (fixed version)."
- echo " Download required components and build Isabelle/Scala/jEdit (default)."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-#options
-
-BUILD_OPTIONS="-b"
-
-CLEAN_FORCE=""
-CLEAN_CHECK=""
-
-VERSION=""
-VERSION_RELEASE=""
-VERSION_PATH=""
-VERSION_REV=""
-
-while getopts "CRU:V:cfnr:u" OPT
-do
- case "$OPT" in
- C)
- CLEAN_FORCE="--clean"
- ;;
- R)
- VERSION="true"
- VERSION_RELEASE="true"
- VERSION_PATH=""
- VERSION_REV=""
- ;;
- U)
- ISABELLE_REPOS="$OPTARG"
- ;;
- V)
- VERSION="true"
- VERSION_RELEASE=""
- VERSION_PATH="$OPTARG"
- VERSION_REV=""
- ;;
- c)
- CLEAN_CHECK="--check"
- ;;
- f)
- BUILD_OPTIONS="-b -f"
- ;;
- n)
- BUILD_OPTIONS=""
- ;;
- r)
- VERSION="true"
- VERSION_RELEASE=""
- VERSION_PATH=""
- VERSION_REV="$OPTARG"
- ;;
- u)
- VERSION="true"
- VERSION_RELEASE=""
- VERSION_PATH=""
- VERSION_REV="tip"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -ne 0 ] && usage
-
-
-## main
-
-if [ -z "$VERSION" ]; then
- "$ISABELLE_HOME/bin/isabelle" components -I || exit "?$"
- "$ISABELLE_HOME/bin/isabelle" components -a || exit "?$"
- if [ -n "$BUILD_OPTIONS" ]; then
- "$ISABELLE_HOME/bin/isabelle" jedit $BUILD_OPTIONS
- fi
-elif [ ! -d "$ISABELLE_HOME/.hg" ]; then
- fail "Not a repository clone: cannot specify version"
-else
- if [ -n "$VERSION_REV" ]; then
- REV="$VERSION_REV"
- elif [ -n "$VERSION_RELEASE" ]; then
- URL="$ISABELLE_REPOS/raw-file/tip/Admin/Release/official"
- REV="$(curl -s -f "$URL" | head -n1)"
- [ -z "$REV" ] && fail "Failed to access \"$URL\""
- 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
-
- "$ISABELLE_HOME/bin/isabelle" components -I || exit "$?"
-
- export LANG=C
- export HGPLAIN=
-
- #Atomic exec: avoid inplace update of running script!
- export CLEAN_FORCE CLEAN_CHECK REV ISABELLE_REPOS BUILD_OPTIONS
- exec bash -c '
- set -e
- "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" "$ISABELLE_REPOS"
- "${HG:-hg}" -R "$ISABELLE_HOME" update -r "$REV" $CLEAN_FORCE $CLEAN_CHECK
- "$ISABELLE_HOME/bin/isabelle" components -a
- if [ -n "$BUILD_OPTIONS" ]; then
- "$ISABELLE_HOME/bin/isabelle" jedit $BUILD_OPTIONS
- fi
- "${HG:-hg}" -R "$ISABELLE_HOME" log -r "$REV"
- if [ ! -f "$ISABELLE_HOME/Admin/setup" ]; then
- echo >&2 "### The Admin/setup script has disappeared in this version"
- echo >&2 "### (need to invoke \"${HG:-hg} update\" before using it again)"
- fi
- '
-fi
--- a/README_REPOSITORY Wed Mar 31 10:57:18 2021 +0200
+++ b/README_REPOSITORY Wed Mar 31 11:05:40 2021 +0200
@@ -12,21 +12,21 @@
(c) Windows: use Cygwin64 with packages "curl" and "mercurial" (via Cygwin setup-x86_64.exe)
-2. Setup repository clone (bash shell commands):
+2. Initial repository clone (bash shell commands):
hg clone https://isabelle.in.tum.de/repos/isabelle
- isabelle/Admin/setup
+ isabelle/Admin/init
-3. Update repository to particular versions (bash shell commands):
+3. Switch repository to particular version (bash shell commands):
#remote tip version
- isabelle/Admin/setup -u
+ isabelle/Admin/init -u
#explicit changeset id or tag (e.g. "Isabelle2021")
- isabelle/Admin/setup -r 7cdcf131699d
+ isabelle/Admin/init -r 7cdcf131699d
#current official release
- isabelle/Admin/setup -R
+ isabelle/Admin/init -R
4. Run application: