|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
#######
#
# E-scripts on HOL.
#
# 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/hol.e>
# or at <http://angg.twu.net/e/hol.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/>.
#
#######
# «.mailing-lists» (to "mailing-lists")
# «.ckpt» (to "ckpt")
# «.checkpointing» (to "checkpointing")
# «.dmtcp» (to "dmtcp")
# «.hol-light» (to "hol-light")
# «.hol-mode» (to "hol-mode")
# «.hol-zero» (to "hol-zero")
# «.hol88-doc» (to "hol88-doc")
# «.hol-omega» (to "hol-omega")
# «.mizar» (to "mizar")
# «.zol» (to "zol")
http://www.ams.org/notices/200811/tx081101408p.pdf
http://www.cl.cam.ac.uk/~jrh13/hol-light/
http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html
http://www.cl.cam.ac.uk/~jrh13/hol-light/summary.txt
http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf
https://lists.sourceforge.net/lists/listinfo/hol-info
http://en.wikipedia.org/wiki/Hol_light
http://www.cl.cam.ac.uk/~jrh13/hol-light/hol_light_220.tar.gz
http://www.cl.cam.ac.uk/~jrh13/hol-light/hol_light_090731.tgz
#####
#
# Mailing lists
# 2012nov16
#
#####
# «mailing-lists» (to ".mailing-lists")
# http://sourceforge.net/mailarchive/forum.php?forum_name=hol-info
#####
#
# ckpt
# 2009oct28
#
#####
# «ckpt» (to ".ckpt")
# http://www.cl.cam.ac.uk/~jrh13/hol-light/hol_light_090731.tgz
# http://www.cs.wisc.edu/~zandy/ckpt/
# http://www.cs.wisc.edu/~zandy/ckpt/ckpt-latest.tar.gz
# (code-c-d "ckpt" "~/usrc/ckpt/")
# (find-ckptfile "")
# (find-ckptfile "README")
# (find-ckptfile "README" "-a SIGNAL")
# (find-ckptfile "README" "-n NAME")
# (find-hollightfile "Makefile" "ckpt -a SIGUSR1 -n hol.snapshot ocaml")
# (find-ckptfile "Makefile")
# (find-ckptfile "om")
# (find-ckptfile "sys.h" "#include <asm/page.h>")
#*
rm -Rv ~/usrc/ckpt/
mkdir ~/usrc/ckpt/
tar -C ~/usrc/ -xvzf \
$S/http/www.cs.wisc.edu/~zandy/ckpt/ckpt-latest.tar.gz
cd ~/usrc/ckpt/
#*
#####
#
# ckpt: garbage-ish notes
# 2009oct28
#
#####
#*
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-ckptfile "sys.h" "#include <asm/page.h>")
cd ~/usrc/ckpt/
make |& tee om
# (find-sh "locate include/asm")
# (find-sh "locate asm-i486/page.h")
# (find-fline "/sda1/usr/include/asm/page.h")
# (find-fline "/sda1/usr/include/asm-i486/page.h")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
R
chroot /sda1/
installeddebs | sort | grep linux
dmissing asm/page.h
linux-headers-2.6.18-4-486_2.6.18.dfsg.1-12.deb
linux-headers-2.6.18-4_2.6.18.dfsg.1-12.deb
linux-headers-2.6.18_2.6.18-10.00.Custom.deb
linux-image-2.6-486_2.6.18+6etch1.deb
linux-image-2.6.18-4-486_2.6.18.dfsg.1-12.deb
linux-image-2.6.18-5-486_2.6.18.dfsg.1-13.deb
linux-image-2.6.18_2.6.18-10.00.Custom.deb
linux-kbuild-2.6.18_2.6.18-1.deb
linux-kernel-headers_2.6.18-7.deb
linux-patch-debian-2.6.18_2.6.18.dfsg.1-12.deb
linux-sound-base_1.0.13-5etch1.deb
linux-source-2.6.18_2.6.18.dfsg.1-12.deb
linux-tree-2.6.18_2.6.18.dfsg.1-12.deb
# (find-zsh "installeddebs | sort | grep linux")
# (find-zsh "dmissing include | grep asm | grep page.h")
# (find-sh "locate usr/include | grep page.h")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
apti linux-headers
uname -r
apti linux-headers-$(uname -r)
uname -a
# (find-status "linux-headers-2.6.26-1-686")
# (find-vldifile "linux-headers-2.6.26-1-686.list")
# (find-vldifile "linux-headers-2.6.26-1-686.list")
# (find-vldifile "linux-headers-2.6.26-1-686.list" "asm-x86/page.h")
# (find-udfile "linux-headers-2.6.26-1-686/")
apti linux-kernel-headers
apti linux-libc-dev
apti linux-source-2.6.26
# (find-status "linux-libc-dev")
# (find-vldifile "linux-libc-dev.list")
# (find-udfile "linux-libc-dev/")
#*
# (find-zsh "installeddebs | sort | grep linux-headers")
# (find-status "linux-headers-2.6.26-1-686")
# (find-vldifile "linux-headers-2.6.26-1-686.list")
# (find-vldifile "linux-headers-2.6.26-1-686.list" "asm-generic/page.h")
# (find-vldifile "linux-headers-2.6.26-1-686.list" "asm-x86/page.h")
# (find-udfile "linux-headers-2.6.26-1-686/")
# (find-status "linux-headers-2.6.26-1-common")
# (find-vldifile "linux-headers-2.6.26-1-common.list")
# (find-vldifile "linux-headers-2.6.26-1-common.list" "asm-generic/page.h")
# (find-vldifile "linux-headers-2.6.26-1-common.list" "asm-x86/page.h")
# (find-udfile "linux-headers-2.6.26-1-common/")
#####
#
# Checkpointing
# 2009oct28
#
#####
# «checkpointing» (to ".checkpointing")
# «dmtcp» (to ".dmtcp")
# (find-es "gdb" "urdb")
# http://www.checkpointing.org/
# http://dmtcp.sourceforge.net/
# http://sourceforge.net/projects/dmtcp/files/
# http://weyl.math.pitt.edu/hanoi2009/Tech/DMTCP
#*
rm -Rv ~/usrc/dmtcp*
mkdir ~/usrc/dmtcp/
tar -C ~/usrc/dmtcp/ -xvzf \
$S/http/ufpr.dl.sourceforge.net/sourceforge/dmtcp/dmtcp/1.06-r354/dmtcp_1.06-r354.tar.gz
cd ~/usrc/dmtcp/dmtcp_1.06-r354/
dpkg-buildpackage -us -uc -b -rfakeroot |& tee odb
#*
# (find-fline "~/usrc/dmtcp/")
* (eepitch-shell)
cd ~/usrc/dmtcp/
sudo dpkg -i *.deb
#*
# (code-c-d "dmtcp" "~/usrc/dmtcp/dmtcp_1.06-r354/")
# (find-dmtcpfile "")
# (find-status "dmtcp")
# (find-vldifile "dmtcp.list")
# (find-udfile "dmtcp/")
# (find-man "1 dmtcp")
# (find-man "1 dmtcp_command")
# (find-man "1 dmtcp_checkpoint")
# (find-man "1 dmtcp_restart")
# (find-man "1 dmtcp_coordinator")
#####
#
# HOL Light
# 2012may06
#
#####
# «hol-light» (to ".hol-light")
# http://www.cl.cam.ac.uk/~jrh13/hol-light/
# http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf
# http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.pdf
# http://www.cl.cam.ac.uk/~jrh13/hol-light/hol_light_100110.tgz
# http://code.google.com/p/hol-light/
# svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light
(code-xpdf "hollighttut" "$S/http/www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf")
(code-pdftotext "hollighttut" "$S/http/www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf" 0)
;; (find-hollighttutpage 1 "Contents")
;; (find-hollighttutpage (+ 1 1) "Index")
;; (find-hollighttuttext "")
# Old:
# http://www.cl.cam.ac.uk/~jrh13/hol-light/
#*
rm -Rv ~/usrc/hol_light/
tar -C ~/usrc/ -xvzf \
$S/http/www.cl.cam.ac.uk/~jrh13/hol-light/hol_light_090731.tgz
cd ~/usrc/hol_light/
make |& tee om
make hol |& tee omh
#*
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/usrc/hol_light/
ocaml
use "hol.ml";;
# (code-c-d "hollight" "~/usrc/hol_light/")
# (find-hollightfile "")
# (find-hollightfile "README")
# (find-hollightfile "Tutorial/")
# (find-hollightfile "100/")
# (find-hollightfile "Makefile" "hol:")
# (find-hollightfile "Makefile" "ckpt -a")
# (find-hollightfile "Makefile" "ckpt -a SIGUSR1 -n hol.snapshot ocaml")
#####
#
# hol-mode for Emacs
# 2010jun28
#
#####
# «hol-mode» (to ".hol-mode")
from Michael Norrish
to xiaoyu xu
cc hol-info <hol-info@lists.sourceforge.net>
date Tue, Jun 22, 2010 at 1:28 AM
subject Re: [Hol-info] how to use hol4
mailing list hol-info.lists.sourceforge.net Filter messages from this mailing list
mailed-by lists.sourceforge.net
unsubscribe Unsubscribe from this mailing-list
hide details Jun 22 (6 days ago)
On 18/06/10 15:57, xiaoyu xu wrote:
> I have installed ML and HOL4 in windows. How can I prove theorems? I am
> a new user of HOL4.
> I have also installed ML HOL4 proofgeneral GNU emacs in Linux system
> Fedora. I can't find "proofgeneral"in menu.
HOL4 doesn't work with Proof General. If you have emacs installed, I
recommend using the emacs-mode, which has a little documentation at
http://hol.sourceforge.net/hol-mode.html
#####
#
# HOL-zero
# 2010nov15
#
#####
# «hol-zero» (to ".hol-zero")
# http://proof-technologies.com/holzero.html
# http://proof-technologies.com/holzero-0.4.1.tgz
# http://proof-technologies.com/holzero-0.5.4.tgz
#*
rm -Rv ~/usrc/holzero-0.5.4/
tar -C ~/usrc/ -xvzf \
$S/http/proof-technologies.com/holzero-0.5.4.tgz
cd ~/usrc/holzero-0.5.4/
#*
# (code-c-d "holzero" "~/usrc/holzero-0.5.4/")
# (find-holzerofile "")
# (find-holzerofile "INSTALL")
# (find-holzerofile "INSTALL" "6. INSTALLING XPP\n\n")
# (find-holzerofile "README")
# (find-holzerofile "README" "4. STARTING HOL ZERO\n\n")
# (find-holzerofile "README" "5. GETTING STARTED WITH INTERACTIVE PROOF\n\n")
# (find-holzerofile "README" "hzhelp")
# (find-holzerosh "cd src/ && ./hzhelp disch_rule")
# (find-holzerofile "src/")
# (find-holzerofile "doc/")
# (find-holzerofile "doc/Glossary.txt")
# (find-holzerofile "doc/User_Manual/")
# (find-holzerofile "doc/User_Manual/3_HOL_Language.txt")
# (find-holzerofile "doc/User_Manual/3_HOL_Language.txt" "type_of")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/usrc/holzero-0.5.4/src/
# ocaml
withgodi ocaml
#use "holzero.ml";;
`! A B . A /\ B ==> B`;;
`? x . (x:'1#'2) = y`;;
disch_rule `q:bool` (assume_rule `p:bool`);;
new_type ("People", 0);;
new_const ("Socrates", `: People`);;
new_const ("Man", `: People -> bool`);;
new_const ("Mortal", `: People -> bool`);;
new_axiom ("Mortality", `! p . Man p ==> Mortal p`);;
new_axiom ("Manhood", `Man Socrates`);;
mp_rule (spec_rule `Socrates` (get_axiom "Mortality"))
(get_axiom "Manhood");;
help "disch_rule";;
type_of `(2, true, x:'a)`;;
#####
#
# hol88-doc
# 2012sep03
#
#####
# «hol88-doc» (to ".hol88-doc")
# (find-status "hol88-doc")
# (find-vldifile "hol88-doc.list")
# (find-udfile "hol88-doc/")
#####
#
# HOL omega
# 2013feb09
#
#####
# «hol-omega» (to ".hol-omega")
# http://www.trustworthytools.com/holw/tutorial.pdf
# http://www.trustworthytools.com/id17.html
#####
#
# Mizar
# 2013may01
#
#####
# «mizar» (to ".mizar")
# http://centria.di.fct.unl.pt/~alama/
# http://markun.cs.shinshu-u.ac.jp/mizar/mma.dir/2005/mma2005(2).pdf
# http://jfr.unibo.it/article/view/1980/1356 mizar in a nutshell
#####
#
# Vincent Aravantinos's tutorial on HOL internals
# 2013jul25
#
#####
# «zol» (to ".zol")
Hi list,
I recently gave a tutorial about HOL internals here in Concordia and I
though it might be useful to share with the community, in case anyone
is interested.
Objective of the tutorial: provide a deeper idea of how HOL works.
Intended audience: people having some experience of HOL as users and
wanting to know more about how HOL works "from inside", but who do not
necessarilly have much background in logic nor functionnal
programming.
To do so we develop a simplistic theorem prover for *propositional*
logic: it is of course useless to do actual mathematics but enables to
understand the fact that terms are Ocaml/SML values, how we use
abstract datatypes to represent theorems and how the tactic system
works.
The prover is called "ZOL" for Zero-Order Logic. The sources are less
than 200 lines and are available both in Ocaml and SML.
Slides: http://users.encs.concordia.ca/~vincent/Teaching_files/zol.pdf
Ocaml source: http://users.encs.concordia.ca/~vincent/Teaching_files/zol.ml
SML source: http://users.encs.concordia.ca/~vincent/Teaching_files/zol.sml
Main page: http://users.encs.concordia.ca/~vincent/Teaching.html
http://sourceforge.net/mailarchive/forum.php?thread_name=4AECC387.3030605%40earthdetails.com&forum_name=hol-info
John Harrison wrote (1995) that reflection hasn't proven very useful in
practice and it has workarounds in higher order logic:
http://www.cl.cam.ac.uk/~jrh13/papers/reflect.ps.gz
But in 2005 he said that "[...] Still some more impressive applications
of reflection are starting to appear":
http://www.cl.cam.ac.uk/~jrh13/slides/wg23-07jun05/slides.pdf
What are these more impressive applications?
Thanks a lot.
Reza.
http://perso.ens-lyon.fr/chantal.keller/Documents-recherche/Stage09/itp10.pdf
http://perso.ens-lyon.fr/chantal.keller/recherche-br.html
http://www.proof-technologies.com/Glossary
;; John Harrison: "Theorem Proving With Real Numbers" (PhD Thesis)
;; http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-408.ps.gz
;; See: "A Question About the Reciprocal of Real_0" (thread)
;; on Hol-info, 2010nov12
;; http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf
(code-xpdf "hollighttut" "$S/http/www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf")
;; (find-hollighttutpage 1 "Contents")
;; (find-hollighttutpage (+ 1 1) "Index")
;; (find-hollighttuttext)
;; John Harrison: "HOL Done Right"
;; http://www.cl.cam.ac.uk/~jrh13/papers/holright.html
# https://bitbucket.org/akrauss/hol-light-workbench/
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd /tmp/
hg clone https://bitbucket.org/akrauss/hol-light-workbench
# (find-fline "/tmp/hol-light-workbench/setup")
http://www.cl.cam.ac.uk/~jrh13/slides/principia-27nov10/slides.pdf
2012may10:
I just read Harrison's talk and the first thing that comes to my
mind is to get started on algebraic topology in a systematic way.
Let's forget proving just the big theorems and build the whole
thing.
http://www.proof-technologies.com/tactician/index.html
http://www.trustworthytools.com/holw/teaser.pdf
http://nevidal.org/download/forthel.pdf
http://people.ds.cam.ac.uk/mg262/CSLI%20talk.pdf
http://people.ds.cam.ac.uk/mg262/
http://www.math.northwestern.edu/~richter/TarskiAxiomGeometry.ml
http://www.michaelbeeson.com/research/FormalTarski/index.php
http://packages.debian.org/stable/hol-light
https://launchpad.net/ubuntu/+source/hol-light
/usr/share/doc/hol-light/README.Debian
http://askra.de/software/prooftree/
is close before the first
public announcement without making any progress. Many things work
already, it just needs a Hol Light + Emacs user to fix the
remaining issues.
Set comprehensions:
http://sourceforge.net/mailarchive/forum.php?thread_name=4FA05981-DD18-472B-B4CB-B7012C6FA85B%40lemma-one.com&forum_name=hol-info
http://sourceforge.net/mailarchive/forum.php?thread_name=78AD4FFA-0A80-40AB-B4E7-0BA283B1B306%40lemma-one.com&forum_name=hol-info
http://article.gmane.org/gmane.comp.mathematics.hol/2118
http://article.gmane.org/gmane.comp.mathematics.hol/2933
http://article.gmane.org/gmane.comp.mathematics.hol/2892
term_grammar.get_precedence (Parse.term_grammar())
https://sourceforge.net/p/hol/mailman/message/36654754/ Ken Kubota on dependent types in HOL
https://www.owlofminerva.net/files/fom.pdf#page=10
# Local Variables:
# coding: utf-8-unix
# End: