|
Warning: this is an htmlized version!
The original is here, 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.
# An introduction to eev can be found here:
#
# (find-eev-quick-intro)
# http://angg.twu.net/eev-intros/find-eev-quick-intro.html
#
# 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
https://www.isa-afp.org/
http://concrete-semantics.org/
http://concrete-semantics.org/concrete-semantics.pdf
https://www.isa-afp.org/entries/IMP_Compiler.html
https://lawrencecpaulson.github.io//2022/05/18/Formalising-Incompleteness-I.html
# Local Variables:
# coding: utf-8-unix
# End: