[isabelle] RC3: patch to get wwwfind running again



So, here is a minimal patch to get the wwwfind tool working again. It
helps that there was nothing wrong with the code itself, only the way it
was being invoked.

For those who care: when working with isabelle-process directly, the
following scenario breaks:
 use_thy "MyTheory"; MyStructure.blah ();
i.e.
 1. passing use_thy "MyTheory" to isabelle-process
 2. MyTheory uses ML_file "blah.ML" to define ML structures
 3. trying to refer to structures from (2) after the use_thy from (1)

I don't know why exactly this is (due to contexts and thread safety?),
but I don't object to it. Just makes it hard to pass parameters in.

I would be interested in the current canonical way to write isabelle
tools which take some parameters, pass them to ML code to do stuff, then
at some future point exit. The old route of
isabelle-process -r -e "use_thy \"my_thy\"; Thing.do_stuff \"$PARAM\";"
appears deprecated. This took me a while to grasp.

Keeping a back door to make this pattern possible will make it easier to
keep the ML tools going which are unlikely to be rewritten in scala
anytime soon.

Makarius:
I don't know what your plan for the "ROOT" file in WWW_Find is. I have
assumed that it is for testing purposes, so that "isabelle build" will
run over the ML files and make sure they at least typecheck. Thus I have
left it, and WWW_Find.thy unchanged, creating a "launcher" in
Start_WWW_Find.thy.
If my assumption is incorrect, you can delete ROOT and merge
Start_WWW_Find.thy into WWW_Find.thy quite easily.
Any other problems, let me know.

On 11/02/13 21:20, Makarius wrote:
> There is also the Isabelle system manual, with a whole chapter on
> Isabelle sessions and build management, including real-life examples.

Yes, I know. I just assumed that "build" builds an image, got it wrong
and apologised.

>> I'll go back to fixing wwwfind now, which definitely does not work.
> 
> You have approx. 24h left.  I had reported its broken state almost 3
> months ago.  The Isabelle2013 release train will not wait for latecomers.

Please don't treat me as if I broke it.

Sincerely,

Rafal Kolanski.
# HG changeset patch
# User Rafal Kolanski <rafal.kolanski at nicta.com.au>
# Date 1360584642 -39600
# Node ID d2788fcf8d181829e992fb439904b4ffe3d0077c
# Parent  cbae5c5ffd234c591c8048b385fc35086d5ca2b7
Fix wwwfind tool startup.

diff --git a/src/Tools/WWW_Find/doc/design.tex b/src/Tools/WWW_Find/doc/design.tex
--- a/src/Tools/WWW_Find/doc/design.tex
+++ b/src/Tools/WWW_Find/doc/design.tex
@@ -267,8 +267,6 @@
 print mode of Isabelle, but the form fields and page structure were manually 
 implemented.
 
-The module is built by using a \texttt{ROOT.ML} file inside a heap that 
-contains the theories to be searched.
 The server is started by calling \texttt{ScgiServer.server}.
 Scripts have been created to automate this process.
 
diff --git a/src/Tools/WWW_Find/lib/Tools/wwwfind b/src/Tools/WWW_Find/lib/Tools/wwwfind
--- a/src/Tools/WWW_Find/lib/Tools/wwwfind
+++ b/src/Tools/WWW_Find/lib/Tools/wwwfind
@@ -124,17 +124,20 @@
 
 WWWPORT=`sed -e 's/[ 	]*//g' -ne 's/server.port=\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
 SCGIPORT=`sed -e 's/[ 	]*//g' -ne 's/"port"=>\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
-MLSTARTSERVER="YXML_Find_Theorems.init (); ScgiServer.server' 10 \"/\" $SCGIPORT;"
+
+# inform theory which SCGI port to use via environment variable
+export SCGIPORT
+MLSTARTSERVER="use_thy \"Start_WWW_Find\";"
 
 case "$COMMAND" in
   start)
     "$LIGHTTPD" -f "$WWWCONFIG"
     if [ "$LOGFILE" = true ]; then
       (cd "$WWWFINDDIR"; \
-       nohup "$ISABELLE_PROCESS" -r -u -e "$MLSTARTSERVER" "$INPUT") &
+       nohup "$ISABELLE_PROCESS" -r -e "$MLSTARTSERVER" "$INPUT") &
     else
       (cd "$WWWFINDDIR"; \
-       nohup "$ISABELLE_PROCESS" -r -u -e "$MLSTARTSERVER" \
+       nohup "$ISABELLE_PROCESS" -r -e "$MLSTARTSERVER" \
          "$INPUT" > /dev/null 2> /dev/null) &
     fi
     ;;
diff --git a/src/Tools/WWW_Find/scgi_server.ML b/src/Tools/WWW_Find/scgi_server.ML
--- a/src/Tools/WWW_Find/scgi_server.ML
+++ b/src/Tools/WWW_Find/scgi_server.ML
@@ -103,7 +103,7 @@
         loop ()
       end;
   in
-    tracing ("SCGI server started.");
+    tracing ("SCGI server started on port " ^ string_of_int port ^ ".");
     dump_handlers ();
     loop ();
     Socket.close passive_sock


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.