src/Tools/Metis/README

streamlined "make_metis"

It's a good idea to update the Metis source code regularly, to benefit
from the latest developments, to avoid a permanent fork, and to detect
Metis problems early. This file explains how to update the source code
for Metis with the latest Metis package. The procedure is
unfortunately somewhat involved and frustrating, and hopefully
temporary.

 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
    replace all occurrences of "MIT license" with "BSD License". In a
    13 Sept. 2010 email to Gerwin Klein, Joe Hurd, the sole copyright
    holder of Metis, wrote:

        I hereby give permission to the Isabelle team to release Metis
        as part of Isabelle, with the Metis code covered under the
        Isabelle BSD license.

 3. Some modifications have to be done manually to the source files.
    The ultimate way to track them down is to use Mercurial. The
    command

        hg diff -rbeabb8443ee4: src

    should do the trick. You might need to specify a different
    revision number if somebody updated the Metis sources without
    updating these instructions; consult the history in case of doubt.

 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", "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" 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.
    "HOL-Metis_Examples" is a good test case. Running the Judgement
    Day suite at this point is also a good idea.

 7. Once everything is fine and you are ready to push your changes to
    the main Isabelle repository, take the time to update these
    instructions, especially points 1 and 3 above.

Good luck!

    Jasmin Blanchette
    16 Sept. 2010