# HG changeset patch # User wenzelm # Date 1617181540 -7200 # Node ID 01acd0eb29cef414659788de6de7a0f6db94c633 # Parent b7bb665fe850b6c69a8ea838153364e6d458e120 clarified name; diff -r b7bb665fe850 -r 01acd0eb29ce Admin/init --- /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 diff -r b7bb665fe850 -r 01acd0eb29ce Admin/setup --- 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 diff -r b7bb665fe850 -r 01acd0eb29ce README_REPOSITORY --- 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: