clarified options;
authorwenzelm
Fri, 16 Apr 2021 21:50:47 +0200
changeset 73840 1d4c9fa00821
parent 73839 ed5226fdf89d
child 73841 386416437ce9
clarified options;
Admin/init
README_REPOSITORY
--- a/Admin/init	Thu Apr 15 19:45:43 2021 +0000
+++ b/Admin/init	Fri Apr 16 21:50:47 2021 +0200
@@ -21,16 +21,17 @@
   echo
   echo "  Options are:"
   echo "    -C           force clean working directory (no backup!)"
+  echo "    -L           local history only: no pull from repository server"
   echo "    -R           version is current official release"
   echo "    -U URL       Isabelle repository server"
   echo "                 (default: \"$ISABELLE_REPOS\")"
-  echo "    -V PATH      version from explicit file, or directory that contains"
-  echo "                 the file \"ISABELLE_VERSION\""
+  echo "    -V PATH      version is taken from file, or directory"
+  echo "                 with 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 in Mercurial notation (changeset id or tag)"
-  echo "    -u           version is latest tip from repository server or local clone"
+  echo "    -r REV       version given in Mercurial notation (changeset id or tag)"
+  echo "    -t           version is latest tip"
   echo
   echo "  Initialize the current ISABELLE_HOME directory, which needs to be a"
   echo "  repository clone (all versions) or repository archive (fixed version)."
@@ -51,6 +52,7 @@
 #options
 
 BUILD_OPTIONS="-b"
+PULL="true"
 
 CLEAN_FORCE=""
 CLEAN_CHECK=""
@@ -60,12 +62,15 @@
 VERSION_PATH=""
 VERSION_REV=""
 
-while getopts "CRU:V:cfnr:u" OPT
+while getopts "CLRU:V:cfnr:t" OPT
 do
   case "$OPT" in
     C)
       CLEAN_FORCE="--clean"
       ;;
+    L)
+      PULL=""
+      ;;
     R)
       VERSION="true"
       VERSION_RELEASE="true"
@@ -96,7 +101,7 @@
       VERSION_PATH=""
       VERSION_REV="$OPTARG"
       ;;
-    u)
+    t)
       VERSION="true"
       VERSION_RELEASE=""
       VERSION_PATH=""
@@ -151,10 +156,12 @@
   export HGPLAIN=
 
   #Atomic exec: avoid inplace update of running script!
-  export CLEAN_FORCE CLEAN_CHECK REV ISABELLE_REPOS BUILD_OPTIONS
+  export PULL CLEAN_FORCE CLEAN_CHECK REV ISABELLE_REPOS BUILD_OPTIONS
   exec bash -c '
     set -e
-    "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" "$ISABELLE_REPOS"
+    if [ -n "$PULL" ]; then
+      "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" "$ISABELLE_REPOS"
+    fi
     "${HG:-hg}" -R "$ISABELLE_HOME" update -r "$REV" $CLEAN_FORCE $CLEAN_CHECK
     "$ISABELLE_HOME/bin/isabelle" components -a
     if [ -n "$BUILD_OPTIONS" ]; then
--- a/README_REPOSITORY	Thu Apr 15 19:45:43 2021 +0000
+++ b/README_REPOSITORY	Fri Apr 16 21:50:47 2021 +0200
@@ -19,15 +19,18 @@
 
 3. Switch repository to particular version (bash shell commands):
 
-    #remote tip version
-    isabelle/Admin/init -u
+    #latest official release
+    isabelle/Admin/init -R
+
+    #latest tip version from repository server
+    isabelle/Admin/init -t
+
+    #latest tip version from local history
+    isabelle/Admin/init -t -L
 
     #explicit changeset id or tag (e.g. "Isabelle2021")
     isabelle/Admin/init -r 7cdcf131699d
 
-    #current official release
-    isabelle/Admin/init -R
-
 4. Run application:
 
     #start Prover IDE and let it build session image