#  15 juni 2005, installation log, TYPES Summerschool 2005
#  This is not exactly how is was done, but it should work the same...
#  Thanks to Nils Anders Danielsson and Pierre Hyvernat
#  for help with various installation tasks !

# Reading this file could help those who want to install 
# Isabelle, Coq and Agda for the TYPES Summerschool 2005.


###################################################################
#                   Install yum package manager                   #
###################################################################

rpm -Uvh http://linux.duke.edu/projects/yum/download/2.2/yum-2.2.0-1.noarch.rpm
cat > /etc/yum.repos.d/haskell.repo <<EOF
[haskell-stable]
name=Haskell Packages (stable)
baseurl=http://haskell.org/fedora/haskell/4/$basearch
gpgkey=http://haskell.org/fedora/RPM-GPG-KEY
gpgcheck=1
EOF

###################################################################
#                   Install haskell stuff by means of yum         #
###################################################################
yum install hugs98
yum install hugs98-doc
yum install darcs
yum install ghc64 ghc64-prof ghc-doc   # ghc mandatory to build agda
yum install happy alex haddock
# Answer yes to all questions.
ln -s /usr/bin/ghc-6.4 /usr/local/bin/ghc
ln -s /usr/bin/ghci-6.4 /usr/local/bin/ghci
cat > /etc/yum.repos.d/extras.repo <<EOF
[extras]
name=Fedora Extras - 4 - $basearch
baseurl=http://download.fedora.redhat.com/pub/fedora/linux/extras/4/$basearch/
gpgcheck=1
gpgkey=http://download.fedora.redhat.com/pub/fedora/linux/extras/RPM-GPG-KEY-Fedora-Extras

[extras-debug]
name=Fedora Extras - 4 - $basearch - Debugging packages
baseurl=http://download.fedora.redhat.com/pub/fedora/linux/extras/4/$basearch/debug/
gpgcheck=1
gpgkey=http://download.fedora.redhat.com/pub/fedora/linux/extras/RPM-GPG-KEY-Fedora-Extras
enabled=0
EOF

###################################################################
#             Install ocaml stuff -- needed to compile coq        #
###################################################################
yum install ocaml ocaml-docs ocaml-emacs ocaml-ocamldoc
# Answer yes to all questions.

###################################################################
#         Install proofgeneral (for isabelle)                     #
###################################################################
rpm -Uvh http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-3.5-1.noarch.rpm
rpm -Uvh http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-xemacs-elc-3.5-1.noarch.rpm
rpm -Uvh http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-emacs-elc-3.5-1.noarch.rpm

###################################################################
#          Install Isabelle                                       #
###################################################################
mkdir /tmp/download
cd /tmp/download
wget http://isabelle.in.tum.de/dist/packages/Isabelle2004.tar.gz
wget http://isabelle.in.tum.de/dist/packages/contrib/ProofGeneral.tar.gz
wget http://isabelle.in.tum.de/dist/packages/contrib/polyml_base.tar.gz
wget http://isabelle.in.tum.de/dist/packages/contrib/polyml_x86-linux.tar.gz
wget http://isabelle.in.tum.de/dist/packages/HOL_x86-linux.tar.gz
tar -C /usr/local/share -xzf Isabelle2004.tar.gz
tar -C /usr/local/share -xzf ProofGeneral.tar.gz
tar -C /usr/local/share -xzf polyml_base.tar.gz
tar -C /usr/local/share -xzf polyml_x86-linux.tar.gz
tar -C /usr/local/share -xzf HOL_x86-linux.tar.gz
cd /usr/local/share/Isabelle
./configure
./bin/isatool install -p /usr/local/bin
./build HOLCF
# Press return when asked to do so.

###################################################################
#             Compile Coq from source (but not install)           #
###################################################################
#install camlp4 (required to compile coq)
yum install camlp4

#compile coq
cd /usr/local/
wget ftp://ftp.inria.fr/INRIA/coq/V8.0pl2/coq-8.0pl2.tar.gz
tar xfz coq-8.0pl2.tar.gz
cd coq-8.0pl2
./configure -local
make world > world.log 2>&1

#to make coq available:
# this is *not* done: for i in *; do ln -s /usr/local/coq-8.0pl2/bin/$i /usr/local/bin/$i ; done

# test Coq:
cd
# wget http://www.labri.fr/Perso/~casteran/CoqArt/coqart.tar.gz
cd CoqArt
make test 2>&1 | \
  perl -ne 'if(/(make.*directory ).*(CoqArt.*)/){print "$1$2\n"}' \
        -e 'elsif(/Finished transaction/){print "Finished transaction\n"}' \
        -e 'else {print}' > test.log

# seems to work fine (takes some time)

###################################################################
#             Install Coq binaries using rpm                      #
###################################################################
#Install Coq with rpm: (the files are in /root/coq-install/)
rpm -i coq-8.0pl2-1.i386.rpm
rpm -i coqide-8.0pl2-1.i386.rpm

#make a directory for resources about coq:

mkdir /usr/local/share/summerschool/coq
cd ~root/coq_install
wget http://www.labri.fr/Perso/~casteran/CoqArt/coqart.tar.gz
tar xfz coqart.tar.gz
cp -r CoqArt /usr/local/share/summerschool/coq/
# download Bertot's extensions:
wget ftp://ftp-sop.inria.fr/lemme/Yves.Bertot/filters.tar.gz
tar xfz filters.tar.gz -C /usr/local/share/summerschool/coq/filters/
wget ftp://ftp-sop.inria.fr/lemme/Yves.Bertot/reals.v
cp reals.v /usr/local/share/summerschool/coq/

########################################################################
#                            Install Agda                              #
########################################################################

mkdir /tmp/agdainst
cd /tmp/agdainst
wget http://www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/resources/agda/Agda-TYPES-2005.tgz
tar xvfz Agda-TYPES-2005.tgz
cd Agda
./configure
cd src
make emacsagda
make install
cd ../elisp
mkdir /usr/share/emacs/site-lisp/agda-mode
cp agda-mode.el haskell-mode.el haskell-indent.el /usr/share/emacs/site-lisp/agda-mode
cat > /usr/share/emacs/site-lisp/site-start.d/agda-mode-init.el <<EOF
(setq load-path (nconc '("/usr/share/emacs/site-lisp/agda-mode/") load-path))
(autoload 'agda-mode "agda-mode.el"
                "Major mode for Agda files" t)
      (unless (assoc "\\\\.agda" auto-mode-alist)
        (setq auto-mode-alist
              (nconc '(("\\\\.agda" . agda-mode)
                       ("\\\\.alfa" . agda-mode)) auto-mode-alist)))
(custom-set-variables
 '(agda-include-path (quote ("/usr/local/share/summerschool/agda"))))
EOF