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

.gitignore

@@ -89,15 +89,19 @@ help/theorygraph/theories.jpg
 help/theorygraph/theories.pdf
 
 src/bool/SharingTables.*
-src/emit/ML/*
-src/emit/Caml/*
+src/emit/ML/*.sml
+src/emit/ML/*.sig
+src/emit/Caml/*.ml
+src/emit/Caml/*.mli
 src/quotient/Manual/quotient.pdf
 src/quotient/src/*.html
 src/quotient/src/*.lst
 src/HolSat/sat_solvers/zc2hs/*.h
 src/HolSat/sat_solvers/zc2hs/zc2hs
 src/HolSat/sat_solvers/minisat/minisat
 src/HolSat/sat_solvers/minisat/depend.mak
+src/num/arith/Manual/arith.pdf
+src/num/arith/Manual/arith.ps
 src/num/termination/numheap
 src/num/termination/numheap.o
 src/pair/help
@@ -114,6 +118,7 @@ src/TeX/holindex-demo.ps
 Manual/*/*.pdf
 Manual/*/*.ps
 Manual/Reference/entries.tex
+Manual/Translations/*/*/*.pdf
 
 examples/dev/*.vl
 
@@ -135,3 +140,4 @@ examples/miniML/hol2miniml/*.txt
 examples/miniML/hol2miniml/miniml-heap
 
 local-hol-heap
+examples/l3-machine-code/**/*-heap

.travis.yml

@@ -3,6 +3,15 @@ compiler:
   - gcc
 before_script: developers/travis/before_install.sh
 script: poly < tools/smart-configure.sml && bin/build $BUILDOPTS -nograph
+notifications:
+  email:
+    recipients:
+      - [email protected]
+    on_success: always
+    on_failure: always
+  irc:
+    channels:
+      - "irc.freenode.net#hol"
 env:
   global:
     - PATH=$PATH:$HOME/bin LD_LIBRARY_PATH=$HOME/lib
@@ -14,3 +23,4 @@ env:
     - ROOTPOLY= BUILDOPTS="-expk -seq developers/travis/selftestseq -selftest"
     - ROOTPOLY= BUILDOPTS="-seq developers/travis/more_examples_seq -selftest"
     - ROOTPOLY= BUILDOPTS="-expk -seq developers/travis/more_examples_seq -selftest"
+    - ROOTPOLY= SVNPOLY=1 BUILDOPTS="-seq developers/travis/selftestseq"

COPYRIGHT

@@ -1,7 +1,7 @@
 HOL COPYRIGHT NOTICE, LICENSE AND DISCLAIMER.
 
 Copyright 1998, 1999 by Konrad Slind.
-Copyright 2000--2013 by Michael Norrish and Konrad Slind.
+Copyright 2000--2014 by Michael Norrish and Konrad Slind.
 
 All rights reserved.
 

Manual/Description/HolBdd.tex

@@ -1109,7 +1109,7 @@ \subsection{The structure \ml{PrintBdd}}\label{PrintBdd}\index{HolBddLib!termbdd
 the variables specified in the varmap part of $tb$. A file \t{ScratchBdd.ps}
 is created, and the BDD is labelled by default with a representation
 of the term part of $tb$. The default labels
-can be suppressed (i.e. set to be always the empty string) by assigning \t{false}
+can be suppressed (i.e.\ set to be always the empty string) by assigning \t{false}
 to the global reference \t{dotTermBddFlag}.
 \end{description}
 

Manual/Description/HolSat.tex

@@ -116,7 +116,7 @@ \subsection{{\tt tautLib}}\label{tautlib}
 
 For details, see the source file \t{src/taut/tautLib.sml} which contains comprehensive comments. Note however that the extra functionality in {{\tt tautLib}} was not engineered for very large problems and can become a performance bottleneck.
 
-\subsection{Support for other SAT solvers}\label{subsec:hs_zchaff}
+\subsection{Support for other SAT solvers}\label{subsec:hs-zchaff}
 
 The ZChaff SAT solver has a proof production mode and is supported by {\tt{HolSatLib}}. However, the ZChaff end user license is not compatible with the \HOL{} license, so we are unable to distribute it with \HOL{}. If you wish to use ZChaff, download and unpack it in the directory {\tt src/HolSat/sat\_solvers/} under the main \HOL{} directory, and compile it with proof production mode enabled (which is not the default). This should create a binary {\tt zchaff} in the directory {\tt src/HolSat/sat\_solvers/zchaff/}. ZChaff can now be used as the external proof engine instead of MiniSat, by using the HolSatLib functions described above, prefixed with a ``{\tt Z}'', e.g., {\tt ZSAT\_PROVE}.
 
@@ -134,10 +134,10 @@ \subsection{The general interface}
 The input term.
 \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.
+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}}
 
-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.
+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}}
 
 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.

Manual/Description/Makefile

@@ -8,16 +8,17 @@ MAKEINDEX=makeindex
 BIBTEX=bibtex
 
 CHAPTERS = conv.tex drules.tex HolQbf.tex HolSat.tex HolSmt.tex		\
-           libraries.tex misc.tex preface.tex \
-           tactics.tex theories.tex title.tex system.tex definitions.tex
+           libraries.tex misc.tex preface.tex QuantHeuristics.tex	\
+           tactics.tex theories.tex title.tex system.tex definitions.tex \
+           enumfset.tex
 OTHER = ../LaTeX/commands.tex ../LaTeX/layout.sty ../LaTeX/ack.tex
 
 default: pdf
 pdf: description.pdf HolBdd.pdf holCheck.pdf
 
 clean:
 	rm -f *.dvi *.aux *.toc *.log *.idx *.ilg *.ind description.pdf \
-            *.bbl *.blg HolBdd.pdf holCheck.pdf
+            *.bbl *.blg *.out HolBdd.pdf holCheck.pdf
 
 description.pdf: description.tex $(CHAPTERS) $(OTHER)
 	${PDFLATEX}  description