Merge branch 'k11-release-prep' into release-masters

.gitignore

@@ -29,6 +29,7 @@
 *.tix
 *.hix
 *.fdb_latexmk
+*.synctex.gz
 
 #Generated Verilog from Iyoda/Gordon hw compilation
 *.vl
@@ -41,19 +42,6 @@ build-log
 svn-update
 developers/generateBuildSummary
 developers/comparelogs
-bin/Holmake
-bin/build
-bin/hol
-bin/hol.bare
-bin/hol.bare.noquote
-bin/hol.noquote
-bin/unquote
-bin/hol.builder
-bin/hol.builder0
-bin/heapname
-bin/buildheap
-bin/*.bat
-
 developers/docfiles/*.txt
 
 tools*/Holmake/Systeml.sml
@@ -133,11 +121,7 @@ examples/set-theory/hol_sets/ordinalML.*
 
 examples/theorem-prover/lisp-runtime/bin/*.s
 
-
 examples/computability/lambda/computability-heap
 
-examples/miniML/hol2miniml/*.txt
-examples/miniML/hol2miniml/miniml-heap
-
 local-hol-heap
 examples/l3-machine-code/**/*-heap

CONTRIBUTORS

@@ -0,0 +1,42 @@
+Vincent Aravantinos
+Bruno Barras
+Richard Boulton
+Jens Brandt
+Aaron Coble
+Hélène Collavizza
+Andrea Condoluci
+Jeremy Dawson
+Anthony Fox
+Ken Friis Larsen
+Thibault Gauthier
+Mike Gordon
+Elsa Gunter
+John Harrison
+Peter Homeier
+Juliano Iyoda
+Matt Kaufmann
+Narges Khakpour
+Ramana Kumar
+Joe Leslie-Hurd
+Guodong Li
+Tom Melham
+Tarek Mhamdi
+Robin Milner
+Lockwood Morris
+Magnus Myreen
+Malcolm Newey
+Michael Norrish
+Scott Owens
+Larry Paulson
+James Reynolds
+Tom Ridge
+Peter Sewell
+Thomas Sewell
+Konrad Slind
+Donald Syme
+Piotr Trojanek
+Thomas Tuerk
+Chris Wadsworth
+Keith Wansbrough
+Tjark Weber
+Chongkai Zhu

COPYRIGHT

@@ -1,9 +1,6 @@
 HOL COPYRIGHT NOTICE, LICENSE AND DISCLAIMER.
 
-Copyright 1998, 1999 by Konrad Slind.
-Copyright 2000--2014 by Michael Norrish and Konrad Slind.
-
-All rights reserved.
+Copyright 2015 by the HOL4 CONTRIBUTORS
 
 Redistribution and use in source and binary forms, with or without
 modification, are permitted provided that the following conditions are

INSTALL

@@ -65,15 +65,7 @@ A. [Moscow ML:] First, install Moscow ML. This is usually
 
        declare -x LD_LIBRARY_PATH=/usr/local/lib:$HOME/lib
 
-   If you are using PolyML 5.5.1 or later, you will have to configure
-   its build with the
-
-       --enabled-shared
-
-   option. In other words, the first thing to do when building PolyML
-   will be
-
-       ./configure --enable-shared
+   Do not use the --with-portable option.
 
 B. Unpack HOL with the commands
 
@@ -163,6 +155,11 @@ E. If bin/build completes (it takes a while!), successfully, you are
    On Windows the hol scripts additionally include a .bat extension,
    and Holmake has a .exe extension.
 
+   At this point, the system is build in <hol-dir> and cannot easily
+   be moved to other locations. In other words, you should unpack HOL
+   in the location/directory where you wish to access it for all your
+   future work.
+
 
 External tools
 --------------

Manual/.gitignore

@@ -0,0 +1 @@
+*.fls

Manual/Description/.gitignore

@@ -0,0 +1,6 @@
+drules.tex
+HolSat.tex
+libraries.tex
+tactics.tex
+theories.tex
+system.tex

Manual/Description/HolQbf.tex

@@ -65,6 +65,7 @@ \subsection{Interface}
 Finally, \ml{decide} does the same job as \ml{decide\_prenex} but accepts QBFs
 in a less restricted form. Restrictions on $\phi$ are described below.
 
+\begin{figure}
 \begin{session}
 \begin{verbatim}
 - load "HolQbfLib";
@@ -110,6 +111,8 @@ \subsection{Interface}
 - val it =  [] |- ?x. x: thm
 \end{verbatim}
 \end{session}
+\caption{\ml{HolQbfLib} in action.}
+\end{figure}
 
 \paragraph{Supported subset of higher-order logic}
 The argument given to \ml{decide} must be a Boolean term built using only conjunction, disjunction, implication, negation, universal/existential quantification, and variables. Free variables are considered universally quantified. Every quantified variable must occur.
@@ -174,7 +177,7 @@ \subsection{Interface}
 \subsection{Wishlist}
 
 The following features have not been implemented yet.
-Please submit additional feature requests (or code contributions) via \url{http://github.com/mn200/HOL}.
+Please submit additional feature requests (or code contributions) via \url{http://github.com/HOL-Theorem-Prover/HOL}.
 
 \paragraph{Support for other QBF solvers}
 

Manual/Description/HolSat.tex → Manual/Description/HolSat.stex

@@ -55,27 +55,18 @@
 The following example illustrates the use of {\tt{HolSatLib}} for proving propositional tautologies:
 
 \begin{session}
-\begin{verbatim}
-- load "HolSatLib"; open HolSatLib;
-(* output omitted *)
-> val it = () : unit
+\begin{alltt}
+>>_ load "HolSatLib"; open HolSatLib;
 
-- show_tags := true;
-> val it = () : unit
+>> show_tags := true;
 
-- SAT_PROVE ``(a ==> b) /\ (b ==> a) = (a=b)``;
-> val it = [oracles: DISK_THM] [axioms: ] []
-           |- (a ==> b) /\ (b ==> a) = (a = b) : thm
+>> SAT_PROVE ``(a ==> b) /\ (b ==> a) = (a=b)``;
 
-- SAT_PROVE ``(a ==> b) ==> (a=b)``
+>> SAT_PROVE ``(a ==> b) ==> (a=b)``
    handle HolSatLib.SAT_cex th => th;
-> val it = [oracles: DISK_THM] [axioms: ] []
-           |- ~a /\ b ==> ~((a ==> b) ==> (a = b)) : thm
 
-- SAT_ORACLE ``(a ==> b) /\ (b ==> a) = (a=b)``;
-> val it = [oracles: DISK_THM, HolSatLib] [axioms: ] []
-           |- (a ==> b) /\ (b ==> a) = (a = b) : thm
-\end{verbatim}
+>> SAT_ORACLE ``(a ==> b) /\ (b ==> a) = (a=b)``;
+\end{alltt}
 \end{session}
 
 Setting \t{show\_tags} to \t{true} makes the \HOL{} top-level print theorem tags. The \t{DISK\_THM} oracle tag has nothing to do with \t{HolSatLib}. It just indicates the use of theorems from \HOL{} libraries read in from permanent storage.
@@ -85,16 +76,12 @@
 The next example illustrates using {\tt{HolSatLib}} for satisfiability testing. The idea is to negate the target term before passing it to {\tt{HolSatLib}}.
 
 \begin{session}
-\begin{verbatim}
-- SAT_PROVE ``~((a ==> b) ==> (a=b))``
-   handle HolSatLib.SAT_cex => th;
-> val it = [oracles: DISK_THM ] [axioms: ] []
-           |- a /\ ~b ==> ~~((a ==> b) ==> (a = b)) : thm
-
-- SAT_PROVE ``~(a /\ ~a)``;
-> val it = [oracles: DISK_THM ] [axioms: ] []
-           |- ~(a /\ ~a) : thm
-\end{verbatim}
+\begin{alltt}
+>> SAT_PROVE ``~((a ==> b) ==> (a=b))``
+   handle HolSatLib.SAT_cex th => th;
+
+>> SAT_PROVE ``~(a /\ ~a)``;
+\end{alltt}
 \end{session}
 
 As expected, if the target term is unsatisfiable we get a theorem saying as much.
@@ -122,51 +109,45 @@ \subsection{Support for other SAT solvers}\label{subsec:hs-zchaff}
 
 A file \texttt{resolve\_trace} may be created in the current working directory, when working with ZChaff. This is the proof trace file produced by ZChaff, and is hardwired.
 
-Other SAT solvers are currently not supported. If you would like such support to be added for your favourite solver, please send a feature request via \url{http://github.com/mn200/HOL}.
+Other SAT solvers are currently not supported. If you would like such support to be added for your favourite solver, please send a feature request via \url{http://github.com/HOL-Theorem-Prover/HOL}.
 
 \subsection{The general interface}
 
 The functions described above are wrappers for the function \texttt{GEN\_SAT}, which is the single entry point for {\tt{HolSatLib}}. \texttt{GEN\_SAT} can be used directly if more flexibility is required. \texttt{GEN\_SAT} takes a single argument, of type \texttt{sat\_config}, defined in \texttt{satConfig.sml}. This is an opaque record type, currently containing the following fields:
 
 \begin{enumerate}
-\item{\texttt{term : Term.term}}
+\item{\texttt{term~:~Term.term}}
 
 The input term.
-\item{\texttt{solver : SatSolvers.sat\_solver}}
+\item{\texttt{solver~:~SatSolvers.sat\_solver}}
 
 The external SAT solver to use. The default is \texttt{SatSolvers.minisatp}. If ZChaff is installed (see \S\ref{subsec:hs-zchaff}), then \texttt{SatSolvers.zchaff} may also be used.
-\item{\texttt{infile : string option}}
+\item{\texttt{infile~:~string option}}
 
 The name of a file in DIMACS format.\footnote{\url{http://www.satlib.org/Benchmarks/SAT/satformat.ps}} Overrides \texttt{term} if set. The input term is instead read from the file.
-\item{\texttt{proof : string option}}
+\item{\texttt{proof~:~string option}}
 
 The name of a proof trace file. Overrides \texttt{solver} if set. The file must be in the native format of {\tt{HolSatLib}}, and must correspond to a proof for \texttt{infile}, which must also be set. The included version of MiniSat has been modified to produce proofs in the native format, and ZChaff proofs are translated to this format using the included proof translator \texttt{src/HolSat/sat\_solvers/zc2hs} (type \texttt{zc2hs -h} for usage help). \texttt{zc2hs} is used internally by \texttt{ZSAT\_PROVE} etc.
-\item{\texttt{is\_cnf : bool}}
+\item{\texttt{is\_cnf~:~bool}}
 
 If true then the input term is expected to be a negated CNF term. This is set automatically if \texttt{infile} is set. Typically a user will never need to modify this field directly.
-\item{\texttt{is\_proved : bool}}
+\item{\texttt{is\_proved~:~bool}}
 
 If true then \HOL{} will prove the SAT solver's results.
 \end{enumerate}
 
-A special value \texttt{base\_config~:~sat\_config} is provided for which the term is \texttt{T}, the solver is MiniSat, the options are unset, the CNF flag is false and the proof flag is true. This value can be inspected and modified using getter and setter functions provided in \texttt{src/HolSat/satConfig.sig}. For example, to invoke ZChaff (assuming it is installed), on a file \texttt{unsat.cnf} containing an unsatisfiable problem, we do:
+A special value \texttt{base\_config~:~sat\_config} is provided for which the term is \texttt{T}, the solver is MiniSat, the options are unset, the CNF flag is false and the proof flag is true. This value can be inspected and modified using getter and setter functions provided in \texttt{src/HolSat/satConfig.sig}. For example, to invoke ZChaff (assuming it is installed), on a file \texttt{zchaff.cnf} containing a DIMACS-formatted  problem, we do:
 
 \begin{session}
-\begin{verbatim}
-- open satConfig;
-(* output omitted *)
+\begin{alltt}
+>>_ open satConfig;
 
-- val c = (set_infile "unsat.cnf" o set_solver SatSolvers.zchaff) base_config;
-> val c = <sat_config> : sat_config
+>> val c = base_config |> set_infile "zchaff.cnf"
+                       |> set_solver SatSolvers.zchaff;
 
-- GEN_SAT c;
-> val it = [oracles: DISK_THM ] [axioms: ] []
-           |- ~<unsat.cnf term here> : thm
-\end{verbatim}
+>>+ GEN_SAT c;
+\end{alltt}
 \end{session}
-
-If the problem were satisfiable, the model can be captured via exception, as shown earlier.
-
 Normally, {\tt{HolSatLib}} will delete the files generated by the SAT solver, such as the output proof, counter-model, and result status. However, if \texttt{infile} is set, the files are not deleted, in case they are required elsewhere.
 
 \subsection{Notes}

Manual/Description/HolSmt.tex

@@ -221,7 +221,7 @@ \subsection{Wishlist}
 
 The following features have not been implemented yet.  Please submit
 additional feature requests (or code contributions) via
-\url{http://github.com/mn200/HOL}.
+\url{http://github.com/HOL-Theorem-Prover/HOL}.
 
 \paragraph{Counterexamples}
 

Manual/Description/Holmakefile

@@ -0,0 +1,36 @@
+INCLUDES = ../Tools
+
+TEX_CORES = description title preface system drules tactics theories definitions libraries misc HolSat
+
+TEX_SOURCES = ../LaTeX/ack.tex ../LaTeX/commands.tex $(patsubst %,%.tex,$(TEX_CORES))
+
+PS_STUFF = ../Tools/polyscripter ../Tools/umap
+PS_COMMAND = $(PS_STUFF) < $< > $@
+
+description.pdf: $(TEX_SOURCES)
+	latexmk -pdf description
+
+drules.tex: drules.stex $(PS_STUFF)
+	$(PS_COMMAND)
+
+tactics.tex: tactics.stex $(PS_STUFF)
+	$(PS_COMMAND)
+
+theories.tex: theories.stex $(PS_STUFF)
+	$(PS_COMMAND)
+
+libraries.tex: libraries.stex $(PS_STUFF)
+	$(PS_COMMAND)
+
+system.tex: system.stex $(PS_STUFF)
+	$(PS_COMMAND)
+
+HolSat.tex: HolSat.stex $(PS_STUFF) zchaff.cnf
+	$(PS_COMMAND)
+
+EXTRA_CLEANS = drules.tex tactics.tex theories.tex libraries.tex HolSat.tex \
+               system.tex\
+               description.pdf \
+               $(patsubst %,%.aux,$(TEX_CORES)) description.log description.out \
+               description.toc description.fls description.idx description.ilg \
+               description.ind description.blg description.bbl description.fdb_latexmk