src/Tools/Metis/README
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45778 df6e210fb44c
child 72004 913162a47d9f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39430
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
     1
It's a good idea to update the Metis source code regularly, to benefit
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
     2
from the latest developments, to avoid a permanent fork, and to detect
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
     3
Metis problems early. This file explains how to update the source code
42235
89571b08a427 updated instructions
blanchet
parents: 39504
diff changeset
     4
for Metis with the latest Metis package.
39430
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
     5
39448
64639ff50fcd streamlined "make_metis"
blanchet
parents: 39444
diff changeset
     6
 1. The files "Makefile" and "script/mlpp" and the directory "src/"
43269
3535f16d9714 new Metis version
blanchet
parents: 42235
diff changeset
     7
    must reflect the corresponding files in Joe Hurd's official Metis
3535f16d9714 new Metis version
blanchet
parents: 42235
diff changeset
     8
    package. The package that was used when these notes where written
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
     9
    was Metis 2.3 (release 20110926).
39430
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    10
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    11
 2. The license in each source file will probably not be something we
39444
beabb8443ee4 MIT license -> BSD License
blanchet
parents: 39433
diff changeset
    12
    can use in Isabelle. The "fix_metis_license" script can be run to
beabb8443ee4 MIT license -> BSD License
blanchet
parents: 39433
diff changeset
    13
    replace all occurrences of "MIT license" with "BSD License". In a
beabb8443ee4 MIT license -> BSD License
blanchet
parents: 39433
diff changeset
    14
    13 Sept. 2010 email to Gerwin Klein, Joe Hurd, the sole copyright
beabb8443ee4 MIT license -> BSD License
blanchet
parents: 39433
diff changeset
    15
    holder of Metis, wrote:
39430
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    16
39433
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES";
blanchet
parents: 39430
diff changeset
    17
        I hereby give permission to the Isabelle team to release Metis
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES";
blanchet
parents: 39430
diff changeset
    18
        as part of Isabelle, with the Metis code covered under the
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES";
blanchet
parents: 39430
diff changeset
    19
        Isabelle BSD license.
39430
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    20
39504
99d6cad53c7e update README
blanchet
parents: 39448
diff changeset
    21
 3. Some modifications might have to be done manually to the source
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
    22
    files (but probably not). The ultimate way to track them down is
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
    23
    to use Mercurial.
39430
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    24
39448
64639ff50fcd streamlined "make_metis"
blanchet
parents: 39444
diff changeset
    25
 4. Isabelle itself cares only about "metis.ML", which is generated
39430
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    26
    from the files in "src/" by the script "make_metis". The script
39448
64639ff50fcd streamlined "make_metis"
blanchet
parents: 39444
diff changeset
    27
    relies on "Makefile", "scripts/mlpp", and "src/", as well as
64639ff50fcd streamlined "make_metis"
blanchet
parents: 39444
diff changeset
    28
    the pseudo-makefile "Makefile.FILES" used to determine all the
64639ff50fcd streamlined "make_metis"
blanchet
parents: 39444
diff changeset
    29
    files needed to be included in "metis.ML".
39430
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    30
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    31
 5. The output of "make_metis" should then work as is with Isabelle,
39448
64639ff50fcd streamlined "make_metis"
blanchet
parents: 39444
diff changeset
    32
    but there are of course no guarantees. The script "make_metis" and
64639ff50fcd streamlined "make_metis"
blanchet
parents: 39444
diff changeset
    33
    the pseudo-makefile "Makefile.FILES" have a few regexes that could
64639ff50fcd streamlined "make_metis"
blanchet
parents: 39444
diff changeset
    34
    go wrong. They also produce a few temporary files ("FILES",
64639ff50fcd streamlined "make_metis"
blanchet
parents: 39444
diff changeset
    35
    "Makefile.dev", and "bin/mosml/Makefile.src") as side-effects; you
64639ff50fcd streamlined "make_metis"
blanchet
parents: 39444
diff changeset
    36
    can safely ignore them or delete them.
39430
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    37
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    38
 6. Once you have successfully regenerated "metis.ML", build all of
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    39
    Isabelle and keep an eye on the time taken by Metis.
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    40
    "HOL-Metis_Examples" is a good test case. Running the Judgement
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    41
    Day suite at this point is also a good idea.
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    42
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    43
 7. Once everything is fine and you are ready to push your changes to
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    44
    the main Isabelle repository, take the time to update these
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    45
    instructions, especially points 1 and 3 above.
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    46
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    47
Good luck!
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    48
afb4d5c672bd document Metis updating procedure
blanchet
parents:
diff changeset
    49
    Jasmin Blanchette
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
    50
    1 December 2011