Dear Isabelle Developers,
The problem:
There exist situations whereupon we find ourselves with an Isabelle
image file without knowing what exactly it is.
One such situation is using wwwfind to present multiple images on
multiple ports. One cannot expect users to remember which is which just
based on the port number. It is much more useful to have the image name
in the title.
Combined with a regression test system which automatically refreshes
such images, it is also pertinent to know which repository revision the
particular image was built from. This is also true when copying images
between machines that would normally take hours to build (e.g. grabbing
them from the regression test server in the morning).
Isabelle (well, the normal release one) currently does not have such a
feature.
An approach:
Now, Makarius will doubtless tell me I've done it wrong, but within our
project I have added a global val image_identifier string in every
image which at least has the name of the image, along with any other
identifying features. Then I added the -I option to isabelle usedir
which allows one to specify those identifying features. I then modified
wwwfind to display this string in the title.
So for example, when we build one of our images, we use:
IMAGE_IDENTIFIER_TAG = `hg log -l 1 --template '{node} {date|isodate}\n'
-r .`
USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -I
$(IMAGE_IDENTIFIER_TAG)
Then if we connect to our wwwfind server on a given port, the title reads:
Find Theorems: CREFINE (7a95fca6ca33e071fd1c948a559898af7e21697e
2011-06-24 20:11 +1000)
If we pull the image off the server, we can also get this string by
evaluating image_identifier.
I think that this style of feature would be really nice in Isabelle. I
am also attaching a patch for Isabelle 2009-1 for your consideration.
If there is interest, I can port it to 2011, but I'd like to get some
feedback first.
Sincerely,
Rafal Kolanski.
summary: Added image_identifier functionality to isabelle images.
diff --git a/lib/Tools/usedir b/lib/Tools/usedir
--- a/lib/Tools/usedir
+++ b/lib/Tools/usedir
@@ -33,6 +33,7 @@
echo -s NAME override session NAME
echo -t BOOL internal session timing (default false)
echo -v BOOL be verbose (default false)
+ echo -I STRINGadd STRING to image_identifier val in image (default \\)
echo
echo Build object-logic or run examples. Also creates browsing
echo information (HTML etc.) according to settings.
@@ -87,11 +88,12 @@
PARALLEL_PROOFS=1
TIMING=false
VERBOSE=false
+IMAGE_IDENTIFIER_TAG=
function getoptions()
{
OPTIND=1
- while getopts C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v: OPT
+ while getopts C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:I: OPT
do
case $OPT in
C)
@@ -169,6 +171,9 @@
check_bool $OPTARG
VERBOSE=$OPTARG
;;
+ I)
+IMAGE_IDENTIFIER_TAG= ($OPTARG)
+;;
\?)
usage
;;
@@ -236,7 +241,7 @@
LOG=$LOGDIR/$ITEM
$ISABELLE_PROCESS \
--e Session.use_dir \$ITEM\ \$ROOT_FILE\ true [$MODES] $RESET $INFO \$DOC\ $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \$PARENT\ \$SESSION\ ($COPY_DUMP, \$DUMP\) \$RPATH\ $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; \
+-e val image_identifier = \${NAME}${IMAGE_IDENTIFIER_TAG}\; Session.use_dir \$ITEM\ \$ROOT_FILE\ true [$MODES] $RESET $INFO \$DOC\ $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \$PARENT\ \$SESSION\ ($COPY_DUMP, \$DUMP\) \$RPATH\ $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; \
-q -w $LOGIC $NAME $LOG
RC=$?
else
diff --git a/src/Pure/mk b/src/Pure/mk
--- a/src/Pure/mk
+++ b/src/Pure/mk
@@ -93,6 +93,7 @@
-e use\$COMPAT\ handle _ = exit 1; \
-e structure Isar = struct fun main () = () end; \
-e ml_prompts \ML \ \ML# \; \
+-e val image_identifier = \RAW\; \
-q -w RAW_ML_SYSTEM RAW $LOG 21
RC=$?
elif [ -n $RAW_SESSION ]; then
@@ -114,6 +115,7 @@
-e val ml_platform = \$ML_PLATFORM\; \
-e (use\$COMPAT\; use\ROOT.ML\) handle _ = exit 1; \
-e ml_prompts \ML \ \ML# \; \
+-e val image_identifier = \Pure\; \
-f -q -w RAW_ML_SYSTEM Pure $LOG 21
RC=$?
fi
diff --git a/src/Tools/WWW_Find/find_theorems.ML b/src/Tools/WWW_Find/find_theorems.ML
--- a/src/Tools/WWW_Find/find_theorems.ML
+++ b/src/Tools/WWW_Find/find_theorems.ML
@@ -66,7 +66,9 @@
fun html_header thy_name args =
html { lang = en } [
-head { title = Find Theorems: results, stylesheet_href = /basic.css }
+(* use global image_identifier which should be defined in all images *)
+head { title = Find Theorems: ^ image_identifier,
+ stylesheet_href = /basic.css }
[script (noid, { script_type=text/javascript,
src=/find_theorems.js })],
add_script (OnLoad, encodequery(document.getElementById('query')))
___
isabelle-dev
