support repository archives (without full .hg directory);
authorwenzelm
Sat, 27 Mar 2021 17:13:15 +0100
changeset 73735 0e880b793db1
parent 73734 6e20976d58f5
child 73736 92db3e31fae3
support repository archives (without full .hg directory);
NEWS
lib/Tools/version
src/Doc/System/Misc.thy
--- a/NEWS	Sat Mar 27 17:05:36 2021 +0100
+++ b/NEWS	Sat Mar 27 17:13:15 2021 +0100
@@ -141,6 +141,12 @@
   - Isabelle_System.download
 
 
+*** System ***
+
+* Command-line tool "isabelle version" supports repository archives
+(without full .hg directory).
+
+
 
 New in Isabelle2021 (February 2021)
 -----------------------------------
--- a/lib/Tools/version	Sat Mar 27 17:05:36 2021 +0100
+++ b/lib/Tools/version	Sat Mar 27 17:13:15 2021 +0100
@@ -59,8 +59,12 @@
 if [ -n "$SHORT_ID" ]; then
   if [ -n "$ISABELLE_ID" ]; then
     echo "$ISABELLE_ID"
+  elif [ -d "$ISABELLE_HOME/.hg" ]; then
+    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || echo undefined
+  elif [ -f "$ISABELLE_HOME/.hg_archival.txt" ]; then
+    fgrep node: < "$ISABELLE_HOME/.hg_archival.txt" | cut -d " " -f2 | head -c12
   else
-    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || echo undefined
+    echo undefined
   fi
 else
   echo 'repository version'    # filled in automatically!
--- a/src/Doc/System/Misc.thy	Sat Mar 27 17:05:36 2021 +0100
+++ b/src/Doc/System/Misc.thy	Sat Mar 27 17:13:15 2021 +0100
@@ -375,7 +375,9 @@
   distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2021: February 2021\<close>.
 
   The \<^verbatim>\<open>-i\<close> option produces a short identification derived from the Mercurial
-  id of the @{setting ISABELLE_HOME} directory.
+  id of the @{setting ISABELLE_HOME} directory. This requires either a
+  repository clone or a repository archive (e.g. download of
+  \<^url>\<open>https://isabelle.sketis.net/repos/isabelle/archive/tip.tar.gz\<close>).
 \<close>
 
 end