|
1 It's a good idea to update the Metis source code regularly, to benefit |
|
2 from the latest developments, to avoid a permanent fork, and to detect |
|
3 Metis problems early. This file explains how to update the source code |
|
4 for Metis with the latest Metis package. The procedure is |
|
5 unfortunately somewhat involved and frustrating, and hopefully |
|
6 temporary. |
|
7 |
|
8 1. The directories "src/" and "script/" were initially copied from |
|
9 Joe Hurd's Metis package. (His "script/" directory has many files |
|
10 in it, but we only need "mlpp".) The package that was used when |
|
11 these notes where written was an unnumbered version of Metis, more |
|
12 recent than 2.2 and dated 19 July 2010. |
|
13 |
|
14 2. The license in each source file will probably not be something we |
|
15 can use in Isabelle. Lawrence C. Paulson's command |
|
16 |
|
17 perl -p -i~ -w -e 's/MIT license/BSD License/g' *sig *sml |
|
18 |
|
19 run in the "src/" directory should do the trick. In a 13 Sept. |
|
20 2010 email to Gerwin Klein, Joe Hurd, the sole copyright holder of |
|
21 Metis, wrote: |
|
22 |
|
23 I hereby give permission to the Isabelle team to release Metis as part |
|
24 of Isabelle, with the Metis code covered under the Isabelle BSD license. |
|
25 |
|
26 3. Some modifications have to be done manually to the source files. |
|
27 Some of these are necessary so that the sources compile at all |
|
28 with Isabelle, some are necessary to avoid race conditions in a |
|
29 multithreaded environment, and some affect the defaults of Metis's |
|
30 heuristics and are needed for backward compatibility with older |
|
31 Isabelle proofs and for performance reasons. These changes should |
|
32 be identified by a comment |
|
33 |
|
34 (* MODIFIED by ?Joe ?Blow *) |
|
35 |
|
36 but the ultimate way to track them down is to use Mercurial. The |
|
37 command |
|
38 |
|
39 hg diff -r2d0a4361c3ef: src |
|
40 |
|
41 should do the trick. (You might need to specify a different |
|
42 revision number if somebody updated the Metis sources without |
|
43 updating these instructions.) |
|
44 |
|
45 4. Isabelle itself only cares about "metis.ML", which is generated |
|
46 from the files in "src/" by the script "make_metis". The script |
|
47 relies on "src/", "scripts/", and a hand-crafted "FILES" file |
|
48 listing all the files needed to be included in "metis.ML". The |
|
49 "FILES" file should be updated to reflect the contents of "src/", |
|
50 although a few files in "src/" are not necessary. Also, the order |
|
51 of the file names in "FILES" matters; X must appear before Y if Y |
|
52 depends on X. |
|
53 |
|
54 5. The output of "make_metis" should then work as is with Isabelle, |
|
55 but there are of course no guarantees. The script "make_metis" has |
|
56 a few evil regex hacks that could go wrong. |
|
57 |
|
58 6. Once you have successfully regenerated "metis.ML", build all of |
|
59 Isabelle and keep an eye on the time taken by Metis. |
|
60 "HOL-Metis_Examples" is a good test case. Running the Judgement |
|
61 Day suite at this point is also a good idea. |
|
62 |
|
63 7. Once everything is fine and you are ready to push your changes to |
|
64 the main Isabelle repository, take the time to update these |
|
65 instructions, especially points 1 and 3 above. |
|
66 |
|
67 Good luck! |
|
68 |
|
69 Jasmin Blanchette |
|
70 15 Sept. 2010 |