--- 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
--- 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
--- 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 | \