[isabelle] Build Isabelle from stock dependencies (Fedora 14)

Hi all,

I made some notes about 'building Isabelle on Fedora from stock
dependencies' and I thought it wouldn't hurt to share (see attachments).

Ignore this if there is a better guide around (or if there is a better
way of doing it in general).

Caveat 1: The current version of poly in Fedora 14 is 5.2.
Caveat 2: You might still have to download latest Scala (for older
Fedora versions; for example, it doesn't build on Fedora 11).

First you should install the usual development tools (via 'yum'):

    make, emacs, java, scala, polyml, gcc

    1.) Clone Isabelle from:

            hg clone http://isabelle.in.tum.de/repos/isabelle Isabelle

    2.) Edit 'Isabelle/etc/settings' to include this:


    3.) Build the 'rail' tool (requires bison and flex -- use 'yum'):

            mkdir rail-build
            cd rail-build
            wget 'http://mirror.ctan.org/support/rail.zip'
            unzip rail.zip
            rm rail.zip
            cd rail
            export PATH="$PATH:$(pwd)"

    4.) Create a symbolic link to scala in '/usr/lib':

            su -c 'ln -s /usr/share/scala/lib/{scala-swing.jar,scala-library.jar} /usr/lib/'

    5.) Finally run (in 'Isabelle/Admin'):

            export SCALA_HOME='/usr' && ./build all
            cd ..

    6.) Build ProofGeneral.

        i) Here's the repository (use password 'anon'):

                cvs -d :pserver:anon at cvs.inf.ed.ac.uk:/disk/cvs/proofgen login && cvs -d :pserver:anon at cvs.inf.ed.ac.uk:/disk/cvs/proofgen checkout ProofGeneral

        ii) Build it:

                cd ProofGeneral
                export PROOFGENERAL_HOME="$(pwd)"
                cd ..

            Note: I had to remove 'coq' from 'PROVERS' in 'Makefile', because of a compile error.

    7.) Finally, run (in 'Isabelle'):

            ./bin/isabelle emacs

        Note: If the script complains about missing ProofGeneral, do the following (in 'Isabelle/Admin'):

            sed --in-place=".backup.$(date '+%Y-%m-%d-%H-%M-%S')" "s|\[ -z \"\$PROOFGENERAL_HOME\" \].*|PROOFGENERAL_HOME=\"$PROOFGENERAL_HOME\"|" lib/Tools/emacs

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.