# HG changeset patch
# User blanchet
# Date 1284616952 -7200
# Node ID 64639ff50fcdea49e6626180c6196600c648f8da
# Parent  61033a8004e2f3493101e76674e900d55d4cdf54
streamlined "make_metis"

diff -r 61033a8004e2 -r 64639ff50fcd src/Tools/Metis/Makefile.FILES
--- a/src/Tools/Metis/Makefile.FILES	Thu Sep 16 07:54:18 2010 +0200
+++ b/src/Tools/Metis/Makefile.FILES	Thu Sep 16 08:02:32 2010 +0200
@@ -4,7 +4,7 @@
 	echo > $@
 refresh_FILES:
 	echo $(POLYML_SRC) | \
-	sed "s/src\///g" | \
-	sed "s/ Tptp\.s[a-z][a-z]//g" | \
-	sed "s/ Options\.s[a-z][a-z]//g" \
+	sed "s/src\/PortablePolyml/PortableIsabelle/g" | \
+	sed "s/ src\/Tptp\.s[a-z][a-z]//g" | \
+	sed "s/ src\/Options\.s[a-z][a-z]//g" \
 	> FILES
diff -r 61033a8004e2 -r 64639ff50fcd src/Tools/Metis/README
--- a/src/Tools/Metis/README	Thu Sep 16 07:54:18 2010 +0200
+++ b/src/Tools/Metis/README	Thu Sep 16 08:02:32 2010 +0200
@@ -5,12 +5,10 @@
 unfortunately somewhat involved and frustrating, and hopefully
 temporary.
 
- 1. The file "Makefile" and the directory "src/" and "script/" were
-    initially copied from Joe Hurd's Metis package. (His "script/"
-    directory has many files in it, but we only need "mlpp".) The
-    package that was used when these notes where written was an
-    unnumbered version of Metis, more recent than 2.2 and dated 19
-    July 2010.
+ 1. The files "Makefile" and "script/mlpp" and the directory "src/"
+    were initially copied from Joe Hurd's official Metis package. The
+    package that was used when these notes where written was Metis 2.3
+    (15 Sept. 2010).
 
  2. The license in each source file will probably not be something we
     can use in Isabelle. The "fix_metis_license" script can be run to
@@ -23,36 +21,27 @@
         Isabelle BSD license.
 
  3. Some modifications have to be done manually to the source files.
-    Some of these are necessary so that the sources compile at all
-    with Isabelle, some are necessary to avoid race conditions in a
-    multithreaded environment, and some affect the defaults of Metis's
-    heuristics and are needed for backward compatibility with older
-    Isabelle proofs and for performance reasons. These changes should
-    be identified by a comment
-
-        (* MODIFIED by ?Joe ?Blow *)
-
-    but the ultimate way to track them down is to use Mercurial. The
+    The ultimate way to track them down is to use Mercurial. The
     command
 
-        hg diff -r2d0a4361c3ef: src
+        hg diff -rbeabb8443ee4: src
 
-    should do the trick. (You might need to specify a different
+    should do the trick. You might need to specify a different
     revision number if somebody updated the Metis sources without
-    updating these instructions.)
+    updating these instructions; consult the history in case of doubt.
 
- 4. Isabelle itself only cares about "metis.ML", which is generated
+ 4. Isabelle itself cares only about "metis.ML", which is generated
     from the files in "src/" by the script "make_metis". The script
-    relies on "Makefile", "src/", and "scripts/", as well as a special
-    file "Makefile.FILES" used to determine all the files needed to be
-    included in "metis.ML".
+    relies on "Makefile", "scripts/mlpp", and "src/", as well as
+    the pseudo-makefile "Makefile.FILES" used to determine all the
+    files needed to be included in "metis.ML".
 
  5. The output of "make_metis" should then work as is with Isabelle,
-    but there are of course no guarantees. The script "make_metis" has
-    a few evil regex hacks that could go wrong. It also produces a
-    few temporary files ("FILES", "Makefile.dev", and
-    "bin/mosml/Makefile.src") as side-effects; you can safely ignore
-    them or delete them.
+    but there are of course no guarantees. The script "make_metis" and
+    the pseudo-makefile "Makefile.FILES" have a few regexes that could
+    go wrong. They also produce a few temporary files ("FILES",
+    "Makefile.dev", and "bin/mosml/Makefile.src") as side-effects; you
+    can safely ignore them or delete them.
 
  6. Once you have successfully regenerated "metis.ML", build all of
     Isabelle and keep an eye on the time taken by Metis.
@@ -66,4 +55,4 @@
 Good luck!
 
     Jasmin Blanchette
-    15 Sept. 2010
+    16 Sept. 2010
diff -r 61033a8004e2 -r 64639ff50fcd src/Tools/Metis/make_metis
--- a/src/Tools/Metis/make_metis	Thu Sep 16 07:54:18 2010 +0200
+++ b/src/Tools/Metis/make_metis	Thu Sep 16 08:02:32 2010 +0200
@@ -7,8 +7,8 @@
 # compile within Isabelle on Poly/ML and SML/NJ.
 
 THIS=$(cd "$(dirname "$0")"; echo $PWD)
-
 make -f Makefile.FILES refresh_FILES
+FILES=$(cat "$THIS/FILES")
 
 (
   cat <<EOF
@@ -32,19 +32,17 @@
 
 EOF
 
-  for FILE in $(cat "$THIS/FILES")
+  for FILE in $FILES
   do
     echo
     echo "(**** Original file: $FILE ****)"
     echo
     echo -e "$FILE" >&2
-    "$THIS/scripts/mlpp" -c polyml "src/$FILE" | \
+    "$THIS/scripts/mlpp" -c polyml "$FILE" | \
     perl -p -e \
 's/type name$/type name = string/;'\
 's/\bref\b/Unsynchronized.ref/g;'\
-'s/\bPolyML.pointerEq\b/pointer_eq/g;'\
-'s/\bRL\b/Metis_RL/g;'\
-"`grep "^\(signature\|structure\|functor\)" src/*.{sig,sml} | \
+"`grep "^\(signature\|structure\|functor\)" $FILES | \
   sed "s/[^:]*:[a-z]* \([A-Za-z0-9_]*\).*/\1/" | \
   tr " " "\n" | \
   sort | \