Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
#######
#
# E-scripts on Isabelle.
#
# Note 1: use the eev command (defined in eev.el) and the
# ee alias (in my .zshrc) to execute parts of this file.
# Executing this file as a whole makes no sense.
#
# Note 2: be VERY careful and make sure you understand what
# you're doing.
#
# Note 3: If you use a shell other than zsh things like |&
# and the for loops may not work.
#
# Note 4: I always run as root.
#
# Note 5: some parts are too old and don't work anymore. Some
# never worked.
#
# Note 6: the definitions for the find-xxxfile commands are on my
# .emacs.
#
# Note 7: if you see a strange command check my .zshrc -- it may
# be defined there as a function or an alias.
#
# Note 8: the sections without dates are always older than the
# sections with dates.
#
# This file is at <http://angg.twu.net/e/isabelle.e>
#           or at <http://angg.twu.net/e/isabelle.e.html>.
#        See also <http://angg.twu.net/emacs.html>,
#                 <http://angg.twu.net/.emacs[.html]>,
#                 <http://angg.twu.net/.zshrc[.html]>,
#                 <http://angg.twu.net/escripts.html>,
#             and <http://angg.twu.net/>.
#
#######




# (find-es "ml")


# «.isabelle99-polyml»	(to "isabelle99-polyml")
# «.isabelle99»		(to "isabelle99")
# «.polyml»		(to "polyml")
# «.isabelle-2008»	(to "isabelle-2008")
# «.isabelle-2011»	(to "isabelle-2011")


http://en.wikipedia.org/wiki/Isabelle_theorem_prover
http://isabelle.in.tum.de/download_x86-linux.html
http://isabelle.in.tum.de/dist/Isabelle2008.tar.gz



#####
#
# Isabelle99 with polyml
# 2000oct14
#
#####

# «isabelle99-polyml»  (to ".isabelle99-polyml")
# (find-shttpw3 "www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/packages.html")
#*
rm -Rv /usr/src/polyml/
rm -Rv /usr/src/Isabelle*

cd /usr/src/
tar -xvzf $S/http/www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/contrib/polyml_base.tar.gz
tar -xvzf $S/http/www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/contrib/polyml_x86-linux.tar.gz

cd /usr/src/
tar -xvzf $S/http/www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/Isabelle99-1.tar.gz
cd /usr/src/Isabelle99-1/
find * -type f > .files

rm -Rv /tmp/isabelle/

cd /usr/src/Isabelle99-1/
./configure
./bin/isatool install -p /tmp/isabelle

# Times: Pure 1:05
#        FOL  0:25
#        HOL  7:40

cd /usr/src/Isabelle99-1/
./build Pure	|& tee obPure
./build FOL	|& tee obFOL
./build HOL	|& tee obHOL

#*

rm -Rv /usr/src/ProofGeneral*
rm -Rv /usr/src/x-symbol/

cd /usr/src/
tar -xvzf $S/http/www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/contrib/ProofGeneral.tar.gz
tar -xvzf $S/http/www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/contrib/x-symbol.tar.gz

# (code-c-d "proofg" "/usr/src/ProofGeneral/")
# (find-proofgfile "")

#*





#####
#
# Isabelle99 with sml-nj
# 2000oct10
#
#####

# «isabelle99»  (to ".isabelle99")
# (to "sml-nj-isabelle")
# (find-shttpw3 "www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/packages.html")
#*
rm -Rv /usr/src/Isabelle99-1/
cd /usr/src/
tar -xvzf $S/http/www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/Isabelle99-1.tar.gz
cd /usr/src/Isabelle99-1/
find * -type f > .files

patch -p0 etc/settings <<'%%%'
18,27c18,27
< POLYML_HOME=$(choosefrom \
<   "$ISABELLE_HOME/contrib/polyml" \
<   "$ISABELLE_HOME/../polyml" \
<   "/usr/share/polyml" \
<   "/usr/local/polyml" \
<   "/opt/polyml")
< ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
< ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null)
< ML_HOME="$POLYML_HOME/$ML_PLATFORM"
< ML_OPTIONS="-h 30000"
---
> #POLYML_HOME=$(choosefrom \
> #  "$ISABELLE_HOME/contrib/polyml" \
> #  "$ISABELLE_HOME/../polyml" \
> #  "/usr/share/polyml" \
> #  "/usr/local/polyml" \
> #  "/opt/polyml")
> #ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
> #ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null)
> #ML_HOME="$POLYML_HOME/$ML_PLATFORM"
> #ML_OPTIONS="-h 30000"
30c30
< #ML_SYSTEM=smlnj-110
---
> ML_SYSTEM=smlnj-110
32,33c32,34
< #ML_OPTIONS="@SMLdebug=/dev/null"
< #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
---
> ML_HOME="/usr/lib/sml-nj/bin"
> ML_OPTIONS="@SMLdebug=/dev/null"
> ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
%%%

cd /usr/src/Isabelle99-1/
./configure	|& tee oc
./bin/isatool install -p /tmp/isabelle	|& tee oi
# (find-fline "/tmp/isabelle/")

#*

# "build Pure" takes 3 minutes...
#bash -x ./build Pure	|& tee obPure
./build Pure	|& tee obPure

#*

cd /usr/src/Isabelle99-1/
for i in FOL CCL CTT Cube FOLP HOL HOLCF LCF Sequents ZF; do
  ./build $i |& tee ob$i
done
#*

bash -x ./build HOL	|& tee obH
# (find-isafile "heaps/smlnj-110_x86-linux/log/")
# (find-isalogfile "")
[opening session.ML]
# (find-isafile "src/HOL/")
# (find-isafile "obP")
# (find-isafile "obH")
# (find-isafile ".files")
# (find-isafile "")
# (find-isafile "bin/isatool")
# (find-isafile "lib/Tools/")
# (find-isafile "lib/Tools/make")
# (find-isafile "lib/Tools/makeall")
# (find-isafile "src/HOL/IsaMakefile")
# (find-isafile "src/FOL/IsaMakefile")


/tmp/isabelle/isabelle
#Unknown logic "HOL" -- no heap file found in:
#  /home/root/isabelle/heaps/smlnj_x86-linux
#  /usr/src/Isabelle99-1/heaps/smlnj_x86-linux

# (find-fline "/usr/src/Isabelle99-1/heaps/smlnj_x86-linux/log/")

#*

# (find-isalogfile "")
# (find-isafile "INSTALL")
# (find-isafile "INSTALL" "/build")
# (find-isafile "build")
# (find-isafile "")

# (find-isafile "")
# (find-isafile ".files")
# (find-isafile "ob")
# (find-isafile "src/Pure/")
# (find-isafile "heaps/smlnj-110/log/Pure")




#####
#
# Isabelle mailing list
# 2000oct13
#
#####

# (find-sftpfile "ftp.cl.cam.ac.uk/ml/")
# (find-sftpfile "ftp.cl.cam.ac.uk/ml/isabelle-users.00.gz")
# (find-sftpfile "ftp.cl.cam.ac.uk/ml/isabelle-users.99.gz")




#####
#
# PolyML
# 2008aug04
#
#####

# «polyml»  (to ".polyml")
# (find-es "ml" "polyml")
# http://www.polyml.org/download.html
# http://www.polyml.org/FAQ.html
# http://ufpr.dl.sourceforge.net/sourceforge/polyml/polyml.5.2.tar.gz
#*
rm -Rv ~/usrc/polyml.5.2/
tar -C ~/usrc/ -xvzf \
  $S/http/ufpr.dl.sourceforge.net/sourceforge/polyml/polyml.5.2.tar.gz
cd     ~/usrc/polyml.5.2/

./configure --prefix=$HOME/usrc/polyml.5.2/   |& tee oc
make                                          |& tee om
make install                                  |& tee omi

#*
# (code-c-d "polyml" "~/usrc/polyml.5.2/")
# (find-polymlfile "")
# (find-polymlfile "omi")
# (find-polymlfile "bin/")
# (find-polymlfile "lib/")
# (find-polymlfile "share/man/man1/")

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
~/usrc/polyml.5.2/bin/poly

# (find-status   "polyml")
# (find-vldifile "polyml.list")
# (find-udfile   "polyml/")
# (find-available "polyml")
# (find-zsh "availabledebs | sort | grep polyml")
# (find-zsh "grep-available polyml")




#####
#
# Isabelle2008
# 2008aug04
#
#####

# «isabelle-2008»  (to ".isabelle-2008")
# http://isabelle.in.tum.de/dist/Isabelle2008.tar.gz
#*
rm -Rv ~/usrc/Isabelle/
tar -C ~/usrc/ -xvzf \
  $S/http/isabelle.in.tum.de/dist/Isabelle2008.tar.gz
cd     ~/usrc/Isabelle/

PATH=$HOME/usrc/polyml.5.2/bin:$PATH \
  build   |& tee ob

#*
# (code-c-d "isabelle" "~/usrc/Isabelle/")
# (find-isabellefile "")
# (find-isabellefile "INSTALL")
# (find-isabellefile "README")
# (find-isabellefile "build")
# (find-isabellefile "etc/settings")
# (find-isabellefile "etc/settings" "type -p poly")
# (find-isabellefile "doc/")
# (find-isabellefile "src/")
# (find-isabellefile "src/Sequents/")
# (find-isabellefile "src/Sequents/LK0.thy")

# (find-isabellefile "bin/isabelle-process")
# (find-isabellefile "lib/")
# (find-isabellefile "lib/scripts/")
# (find-isabellefile "lib/scripts/run-polyml")
# (find-isabellefile "lib/scripts/getsettings")
# (find-isabellesh "sh lib/scripts/getsettings")
# (find-isabellesh "cd lib/scripts\n sh $PWD/getsettings")

(setenv "ISABELLE_HOME" "/home/edrx/usrc/Isabelle")

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
export ISABELLE_HOME=$HOME/home/edrx/usrc/Isabelle


* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
export PATH=$HOME/usrc/polyml.5.2/bin:$PATH
bash
type -p poly
exit
exit



http://www.mail-archive.com/polyml@inf.ed.ac.uk/msg00007.html

http://www.nicta.com.au/news/home_page_content_listing/world-first_research_breakthrough_promises_safety-critical_software_of_unprecedented_reliability
http://ertos.nicta.com.au/research/l4.verified/
http://ertos.nicta.com.au/research/l4.verified/sqrt-2-proof.pdf
http://ertos.nicta.com.au/research/l4.verified/pubs.pml




#####
#
# Isabelle 2011
# 2011may08
#
#####

# «isabelle-2011»  (to ".isabelle-2011")

# http://isabelle.in.tum.de/
# http://isabelle.in.tum.de/download.html
# http://isabelle.in.tum.de/dist/Isabelle2011_bundle_x86-linux.tar.gz
cd /sda5/isabelle/
wget http://isabelle.in.tum.de/dist/Isabelle2011_bundle_x86-linux.tar.gz




# http://dl.dropbox.com/u/9291912/courses/2011-EBL/Isabelle1.pdf
# http://dl.dropbox.com/u/9291912/courses/2011-EBL/Isabelle2.pdf

(code-xpdf      "ijoao1" "$S/http/dl.dropbox.com/u/9291912/courses/2011-EBL/Isabelle1.pdf")
(code-pdftotext "ijoao1" "$S/http/dl.dropbox.com/u/9291912/courses/2011-EBL/Isabelle1.pdf")
;; (find-ijoao1page      1  "Contents")
;; (find-ijoao1page     47  "The Meta-Language")
;; (find-ijoao1page     89  "The Great Variable Hoax")
;; (find-ijoao1page    138  "The Meta-Logic: HOL")
;; (find-ijoao1page    195  "Resolution")
;; (find-ijoao1text "")
(code-xpdf      "ijoao2" "$S/http/dl.dropbox.com/u/9291912/courses/2011-EBL/Isabelle2.pdf")
(code-pdftotext "ijoao2" "$S/http/dl.dropbox.com/u/9291912/courses/2011-EBL/Isabelle2.pdf")
;; (find-ijoao2page      1  "Contents")
;; (find-ijoao2page     70  "Contents")
;; (find-ijoao2text "")


http://isabelle.in.tum.de/website-Isabelle2009-1/sledgehammer.html




#  Local Variables:
#  coding:               raw-text-unix
#  ee-delimiter-hash:    "\n#*\n"
#  ee-delimiter-percent: "\n%*\n"
#  ee-anchor-format:     "«%s»"
#  End: