The following commit has been merged in the master branch:
commit 06491d805f34c353f5b5d03d415b8df64e3deb0e
Author: Hendrik Tews <hend...@askra.de>
Date:   Sun Jun 10 21:54:04 2012 +0200

    unapply debian patches, remove holtest-dependency-hint patch

diff --git a/.pc/.quilt_patches b/.pc/.quilt_patches
deleted file mode 100644
index 6857a8d..0000000
--- a/.pc/.quilt_patches
+++ /dev/null
@@ -1 +0,0 @@
-debian/patches
diff --git a/.pc/.quilt_series b/.pc/.quilt_series
deleted file mode 100644
index c206706..0000000
--- a/.pc/.quilt_series
+++ /dev/null
@@ -1 +0,0 @@
-series
diff --git a/.pc/.version b/.pc/.version
deleted file mode 100644
index 0cfbf08..0000000
--- a/.pc/.version
+++ /dev/null
@@ -1 +0,0 @@
-2
diff --git a/.pc/applied-patches b/.pc/applied-patches
deleted file mode 100644
index c4fb8a5..0000000
--- a/.pc/applied-patches
+++ /dev/null
@@ -1,3 +0,0 @@
-default-hollight-dir
-holtest-no-proof-recording.patch
-holtest-dependency-hint.patch
diff --git a/.pc/default-hollight-dir/.timestamp 
b/.pc/default-hollight-dir/.timestamp
deleted file mode 100644
index e69de29..0000000
diff --git a/.pc/default-hollight-dir/hol.ml b/.pc/default-hollight-dir/hol.ml
deleted file mode 100644
index 843b11f..0000000
--- a/.pc/default-hollight-dir/hol.ml
+++ /dev/null
@@ -1,159 +0,0 @@
-(* ========================================================================= *)
-(*                               HOL LIGHT                                   *)
-(*                                                                           *)
-(*              Modern OCaml version of the HOL theorem prover               *)
-(*                                                                           *)
-(*                            John Harrison                                  *)
-(*                                                                           *)
-(*            (c) Copyright, University of Cambridge 1998                    *)
-(*              (c) Copyright, John Harrison 1998-2007                       *)
-(* ========================================================================= *)
-
-let hol_version = "2.20++";;
-
-let hol_dir = ref
-  (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;
-
-(* ------------------------------------------------------------------------- *)
-(* Should eventually change to "ref(Filename.temp_dir_name)".                *)
-(* However that's not available in 3.08, which is still the default          *)
-(* in Cygwin, and I don't want to force people to upgrade Ocaml.             *)
-(* ------------------------------------------------------------------------- *)
-
-let temp_path = ref "/tmp";;
-
-(* ------------------------------------------------------------------------- *)
-(* Load in parsing extensions.                                               *)
-(* For Ocaml < 3.10, use the built-in camlp4                                 *)
-(* and for Ocaml >= 3.10, use camlp5 instead.                                *)
-(* ------------------------------------------------------------------------- *)
-
-if let v = String.sub Sys.ocaml_version 0 4 in v >= "3.10"
-then (Topdirs.dir_directory "+camlp5";
-      Topdirs.dir_load Format.std_formatter "camlp5o.cma")
-else (Topdirs.dir_load Format.std_formatter "camlp4o.cma");;
-
-Topdirs.dir_load Format.std_formatter (Filename.concat (!hol_dir) "pa_j.cmo");;
-
-(* ------------------------------------------------------------------------- *)
-(* Load files from system and/or user-settable directories.                  *)
-(* Paths map initial "$/" to !hol_dir dynamically; use $$ to get the actual  *)
-(* $ character at the start of a directory.                                  *)
-(* ------------------------------------------------------------------------- *)
-
-let use_file s =
-  if Toploop.use_file Format.std_formatter s then ()
-  else (Format.print_string("Error in included file "^s);
-        Format.print_newline());;
-
-let hol_expand_directory s =
-  if s = "$" or s = "$/" then !hol_dir
-  else if s = "$$" then "$"
-  else if String.length s <= 2 then s
-  else if String.sub s 0 2 = "$$" then (String.sub s 1 (String.length s - 1))
-  else if String.sub s 0 2 = "$/"
-  then Filename.concat (!hol_dir) (String.sub s 2 (String.length s - 2))
-  else s;;
-
-let load_path = ref ["."; "$"];;
-
-let loaded_files = ref [];;
-
-let file_on_path p s =
-  if not (Filename.is_relative s) then s else
-  let p' = List.map hol_expand_directory p in
-  let d = List.find (fun d -> Sys.file_exists(Filename.concat d s)) p' in
-  Filename.concat (if d = "." then Sys.getcwd() else d) s;;
-
-let load_on_path p s =
-  let s' = file_on_path p s in
-  let fileid = (Filename.basename s',Digest.file s') in
-  (use_file s'; loaded_files := fileid::(!loaded_files));;
-
-let loads s = load_on_path ["$"] s;;
-
-let loadt s = load_on_path (!load_path) s;;
-
-let needs s =
-  let s' = file_on_path (!load_path) s in
-  let fileid = (Filename.basename s',Digest.file s') in
-  if List.mem fileid (!loaded_files)
-  then Format.print_string("File \""^s^"\" already loaded\n") else loadt s;;
-
-(* ------------------------------------------------------------------------- *)
-(* Various tweaks to OCaml and general library functions.                    *)
-(* ------------------------------------------------------------------------- *)
-
-loads "system.ml";;     (* Set up proper parsing and load bignums            *)
-loads "lib.ml";;        (* Various useful general library functions          *)
-
-(* ------------------------------------------------------------------------- *)
-(* The logical core.                                                         *)
-(* ------------------------------------------------------------------------- *)
-
-loads "fusion.ml";;
-
-(* ------------------------------------------------------------------------- *)
-(* Some extra support stuff needed outside the core.                         *)
-(* ------------------------------------------------------------------------- *)
-
-loads "basics.ml";;     (* Additional syntax operations and other utilities  *)
-loads "nets.ml";;       (* Term nets for fast matchability-based lookup      *)
-
-(* ------------------------------------------------------------------------- *)
-(* The interface.                                                            *)
-(* ------------------------------------------------------------------------- *)
-
-loads "preterm.ml";;    (* Preterms and their interconversion with terms     *)
-loads "parser.ml";;     (* Lexer and parser                                  *)
-loads "printer.ml";;    (* Crude prettyprinter                               *)
-
-(* ------------------------------------------------------------------------- *)
-(* Higher level deductive system.                                            *)
-(* ------------------------------------------------------------------------- *)
-
-loads "equal.ml";;      (* Basic equality reasoning and conversionals        *)
-loads "bool.ml";;       (* Boolean theory and basic derived rules            *)
-loads "drule.ml";;      (* Additional derived rules                          *)
-loads "tactics.ml";;    (* Tactics, tacticals and goal stack                 *)
-loads "itab.ml";;       (* Toy prover for intuitionistic logic               *)
-loads "simp.ml";;       (* Basic rewriting and simplification tools.         *)
-loads "theorems.ml";;   (* Additional theorems (mainly for quantifiers) etc. *)
-loads "ind_defs.ml";;   (* Derived rules for inductive definitions           *)
-loads "class.ml";;      (* Classical reasoning: Choice and Extensionality    *)
-loads "trivia.ml";;     (* Some very basic theories, e.g. type ":1"          *)
-loads "canon.ml";;      (* Tools for putting terms in canonical forms        *)
-loads "meson.ml";;      (* First order automation: MESON (model elimination) *)
-loads "quot.ml";;       (* Derived rules for defining quotient types         *)
-
-(* ------------------------------------------------------------------------- *)
-(* Mathematical theories and additional proof tools.                         *)
-(* ------------------------------------------------------------------------- *)
-
-loads "pair.ml";;       (* Theory of pairs                                   *)
-loads "nums.ml";;       (* Axiom of Infinity, definition of natural numbers  *)
-loads "recursion.ml";;  (* Tools for primitive recursion on inductive types  *)
-loads "arith.ml";;      (* Natural number arithmetic                         *)
-loads "wf.ml";;         (* Theory of wellfounded relations                   *)
-loads "calc_num.ml";;   (* Calculation with natural numbers                  *)
-loads "normalizer.ml";; (* Polynomial normalizer for rings and semirings     *)
-loads "grobner.ml";;    (* Groebner basis procedure for most semirings.      *)
-loads "ind_types.ml";;  (* Tools for defining inductive types                *)
-loads "lists.ml";;      (* Theory of lists                                   *)
-loads "realax.ml";;     (* Definition of real numbers                        *)
-loads "calc_int.ml";;   (* Calculation with integer-valued reals             *)
-loads "realarith.ml";;  (* Universal linear real decision procedure          *)
-loads "real.ml";;       (* Derived properties of reals                       *)
-loads "calc_rat.ml";;   (* Calculation with rational-valued reals            *)
-loads "int.ml";;        (* Definition of integers                            *)
-loads "sets.ml";;       (* Basic set theory.                                 *)
-loads "iterate.ml";;    (* Iterated operations                               *)
-loads "cart.ml";;       (* Finite Cartesian products                         *)
-loads "define.ml";;     (* Support for general recursive definitions         *)
-
-(* ------------------------------------------------------------------------- *)
-(* The help system.                                                          *)
-(* ------------------------------------------------------------------------- *)
-
-loads "help.ml";;       (* Online help using the entries in Help directory   *)
-loads "database.ml";;   (* List of name-theorem pairs for search system      *)
diff --git a/.pc/holtest-dependency-hint.patch/.timestamp 
b/.pc/holtest-dependency-hint.patch/.timestamp
deleted file mode 100644
index e69de29..0000000
diff --git a/.pc/holtest-dependency-hint.patch/holtest 
b/.pc/holtest-dependency-hint.patch/holtest
deleted file mode 100755
index de3d4ff..0000000
--- a/.pc/holtest-dependency-hint.patch/holtest
+++ /dev/null
@@ -1,167 +0,0 @@
-#!/bin/bash
-#######################################################################
-# Load in a bunch of examples to test HOL Light is working properly
-# Try examining the output using something like
-#
-#     egrep -i '###|error|not.found' nohup.out
-#
-# to see progress and whether anything has gone wrong.
-#
-# You might first want to install the necessary external tools,
-# for instance with
-#
-#   aptitude install prover9 coinor-csdp pari-gp
-#
-#######################################################################
-
-set -e
-
-if which hol-light > /dev/null ; then
-    hollight=hol-light
-else
-    # Make sure we have an up-to-date hol, and Mizar Light extensions
-    make hol
-    (cd Mizarlight; make clean; make)
-    hollight=./hol
-fi
-
-# Standalone examples
-
-echo '### Loading Library/agm.ml'; echo 'loadt "Library/agm.ml";;' | (time 
$hollight)
-echo '### Loading Library/binary.ml'; echo 'loadt "Library/binary.ml";;' | 
(time $hollight)
-echo '### Loading Library/binomial.ml'; echo 'loadt "Library/binomial.ml";;' | 
(time $hollight)
-echo '### Loading Examples/borsuk.ml'; echo 'loadt "Examples/borsuk.ml";;' | 
(time $hollight)
-echo '### Loading Examples/brunn_minkowski.ml'; echo 'loadt 
"Examples/brunn_minkowski.ml";;' | (time $hollight)
-echo '### Loading Library/card.ml'; echo 'loadt "Library/card.ml";;' | (time 
$hollight)
-echo '### Loading Examples/combin.ml'; echo 'loadt "Examples/combin.ml";;' | 
(time $hollight)
-echo '### Loading Examples/cong.ml'; echo 'loadt "Examples/cong.ml";;' | (time 
$hollight)
-echo '### Loading Examples/cooper.ml'; echo 'loadt "Examples/cooper.ml";;' | 
(time $hollight)
-echo '### Loading Examples/dlo.ml'; echo 'loadt "Examples/dlo.ml";;' | (time 
$hollight)
-echo '### Loading Library/floor.ml'; echo 'loadt "Library/floor.ml";;' | (time 
$hollight)
-echo '### Loading Examples/forster.ml'; echo 'loadt "Examples/forster.ml";;' | 
(time $hollight)
-echo '### Loading Examples/hol88.ml'; echo 'loadt "Examples/hol88.ml";;' | 
(time $hollight)
-echo '### Loading Examples/holby.ml'; echo 'loadt "Examples/holby.ml";;' | 
(time $hollight)
-echo '### Loading Library/integer.ml'; echo 'loadt "Library/integer.ml";;' | 
(time $hollight)
-echo '### Loading Library/isum.ml'; echo 'loadt "Library/isum.ml";;' | (time 
$hollight)
-echo '### Loading Examples/kb.ml'; echo 'loadt "Examples/kb.ml";;' | (time 
$hollight)
-echo '### Loading Examples/lagrange_lemma.ml'; echo 'loadt 
"Examples/lagrange_lemma.ml";;' | (time $hollight)
-echo '### Loading Examples/mangoldt.ml'; echo 'loadt "Examples/mangoldt.ml";;' 
| (time $hollight)
-echo '### Loading Examples/mccarthy.ml'; echo 'loadt "Examples/mccarthy.ml";;' 
| (time $hollight)
-echo '### Loading Examples/mizar.ml'; echo 'loadt "Examples/mizar.ml";;' | 
(time $hollight)
-echo '### Loading Library/multiplicative.ml'; echo 'loadt 
"Library/multiplicative.ml";;' | (time $hollight)
-echo '### Loading Examples/multiwf.ml'; echo 'loadt "Examples/multiwf.ml";;' | 
(time $hollight)
-echo '### Loading Examples/pell.ml'; echo 'loadt "Examples/pell.ml";;' | (time 
$hollight)
-echo '### Loading Library/permutations.ml'; echo 'loadt 
"Library/permutations.ml";;' | (time $hollight)
-echo '### Loading Library/primitive.ml'; echo 'loadt "Library/primitive.ml";;' 
| (time $hollight)
-echo '### Loading Library/products.ml'; echo 'loadt "Library/products.ml";;' | 
(time $hollight)
-echo '### Loading Examples/prog.ml'; echo 'loadt "Examples/prog.ml";;' | (time 
$hollight)
-echo '### Loading Examples/prover9.ml'; echo 'loadt "Examples/prover9.ml";;' | 
(time $hollight)
-echo '### Loading Examples/rectypes.ml'; echo 'loadt "Examples/rectypes.ml";;' 
| (time $hollight)
-echo '### Loading Examples/schnirelmann.ml'; echo 'loadt 
"Examples/schnirelmann.ml";;' | (time $hollight)
-echo '### Loading Examples/solovay.ml'; echo 'loadt "Examples/solovay.ml";;' | 
(time $hollight)
-echo '### Loading Examples/sos.ml'; echo 'loadt "Examples/sos.ml";;' | (time 
$hollight)
-echo '### Loading Examples/ste.ml'; echo 'loadt "Examples/ste.ml";;' | (time 
$hollight)
-echo '### Loading Library/wo.ml'; echo 'loadt "Library/wo.ml";;' | (time 
$hollight)
-echo '### Loading 
Library/analysis.ml,/transc.ml,calc_real.ml,machin.ml,polylog.ml,poly.ml';
-(echo 'loadt "Library/analysis.ml";;'; echo 'loadt "Library/transc.ml";;';
- echo 'loadt "Library/calc_real.ml";;'; echo 'loadt "Examples/machin.ml";;';
- echo 'loadt "Examples/polylog.ml";;'; echo 'loadt "Library/poly.ml";;') | 
(time $hollight)
-echo '### Loading Library/prime.ml,pratt.ml';
-(echo 'loadt "Library/prime.ml";;'; echo 'loadt "Library/pratt.ml";;') | (time 
$hollight)
-echo '### Loading Library/prime.ml,pocklington.ml';
-(echo 'loadt "Library/prime.ml";;'; echo 'loadt "Library/pocklington.ml";;') | 
(time $hollight)
-echo '### Loading Library/rstc.ml,reduct.ml';
-(echo 'loadt "Library/rstc.ml";;'; echo 'loadt "Examples/reduct.ml";;') | 
(time $hollight)
-
-# Extended examples
-
-echo '### Loading Arithmetic/make.ml'; echo 'loadt "Arithmetic/make.ml";;' | 
(time $hollight)
-echo '### Loading Boyer_Moore/make.ml'; echo 'loadt "Boyer_Moore/make.ml";;' | 
(time $hollight)
-echo '### Loading Complex/make.ml'; echo 'loadt "Complex/make.ml";;' | (time 
$hollight)
-echo '### Loading IsabelleLight/make.ml'; echo 'loadt 
"IsabelleLight/make.ml";;' | (time $hollight)
-echo '### Loading Jordan/make.ml'; echo 'loadt "Jordan/make.ml";;' | (time 
$hollight)
-echo '### Loading Mizarlight/make.ml'; echo 'loadt "Mizarlight/make.ml";;' | 
(time $hollight)
-echo '### Loading miz3/make.ml, miz3/test.ml (twice)'; (echo 'loadt 
"miz3/make.ml";;'; echo 'loadt "miz3/test.ml";;'; echo 'loadt 
"miz3/test.ml";;') | (time $hollight)
-if which zchaff > /dev/null ; then
-    echo '### Loading Minisat/make.ml,Minisat/taut.ml';
-    (echo 'loadt "Minisat/make.ml";;'; echo 'loadt "Minisat/taut.ml";;') | 
(time $hollight)
-else
-    echo '### Error: skip Minisat/make.ml, Minisat/taut.ml because zchaff is 
not available'
-fi
-echo '### Loading Model/make.ml'; echo 'loadt "Model/make.ml";;' | (time 
$hollight)
-echo '### Loading Multivariate/make.ml'; echo 'loadt "Multivariate/make.ml";;' 
| (time $hollight)
-echo '### Loading Multivariate/make_complex.ml'; echo 'loadt 
"Multivariate/make_complex.ml";;' | (time $hollight)
-echo '### Loading Ntrie/ntrie.ml'; echo 'loadt "Ntrie/ntrie.ml";;' | (time 
$hollight)
-echo '### Loading Permutation/make.ml'; echo 'loadt "Permutation/make.ml";;' | 
(time $hollight)
-echo '### Loading QBF/make.ml'; echo 'loadt "QBF/make.ml";;' | (time $hollight)
-echo '### Loading Rqe/make.ml'; echo 'loadt "Rqe/make.ml";;' | (time $hollight)
-echo '### Loading Unity/make.ml'; echo 'loadt "Unity/make.ml";;' | (time 
$hollight)
-echo '### Loading Multivariate/geom.ml'; echo 'loadt "Multivariate/geom.ml";;' 
| (time $hollight)
-echo '### Loading Multivariate/cross.ml'; echo 'loadt 
"Multivariate/cross.ml";;' | (time $hollight)
-echo '### Loading Multivariate/flyspeck.ml'; echo 'loadt 
"Multivariate/flyspeck.ml";;' | (time $hollight)
-
-# Some of the "Great 100 theorems"
-
-echo '### Loading 100/arithmetic_geometric_mean.ml'; echo 'loadt 
"100/arithmetic_geometric_mean.ml";;' | (time $hollight)
-echo '### Loading 100/arithmetic.ml'; echo 'loadt "100/arithmetic.ml";;' | 
(time $hollight)
-echo '### Loading 100/ballot.ml'; echo 'loadt "100/ballot.ml";;' | (time 
$hollight)
-echo '### Loading 100/bernoulli.ml'; echo 'loadt "100/bernoulli.ml";;' | (time 
$hollight)
-echo '### Loading 100/bertrand.ml,100/primerecip.ml';
-(echo 'loadt "100/bertrand.ml";;'; echo 'loadt "100/primerecip.ml";;') | (time 
$hollight)
-echo '### Loading 100/birthday.ml'; echo 'loadt "100/birthday.ml";;' | (time 
$hollight)
-echo '### Loading 100/cantor.ml'; echo 'loadt "100/cantor.ml";;' | (time 
$hollight)
-echo '### Loading 100/ceva.ml'; echo 'loadt "100/ceva.ml";;' | (time $hollight)
-echo '### Loading 100/circle.ml'; echo 'loadt "100/circle.ml";;' | (time 
$hollight)
-echo '### Loading 100/chords.ml'; echo 'loadt "100/chords.ml";;' | (time 
$hollight)
-echo '### Loading 100/combinations.ml'; echo 'loadt "100/combinations.ml";;' | 
(time $hollight)
-echo '### Loading 100/constructible.ml'; echo 'loadt "100/constructible.ml";;' 
| (time $hollight)
-echo '### Loading 100/cosine.ml'; echo 'loadt "100/cosine.ml";;' | (time 
$hollight)
-echo '### Loading 100/cubic.ml'; echo 'loadt "100/cubic.ml";;' | (time 
$hollight)
-echo '### Loading 100/derangements.ml'; echo 'loadt "100/derangements.ml";;' | 
(time $hollight)
-echo '### Loading 100/desargues.ml'; echo 'loadt "100/desargues.ml";;' | (time 
$hollight)
-echo '### Loading 100/dirichlet.ml'; echo 'loadt "100/dirichlet.ml";;' | (time 
$hollight)
-echo '### Loading 100/div3.ml'; echo 'loadt "100/div3.ml";;' | (time $hollight)
-echo '### Loading 100/divharmonic.ml'; echo 'loadt "100/divharmonic.ml";;' | 
(time $hollight)
-echo '### Loading 100/e_is_transcendental.ml'; echo 'loadt 
"100/e_is_transcendental.ml";;' | (time $hollight)
-echo '### Loading 100/euler.ml'; echo 'loadt "100/euler.ml";;' | (time 
$hollight)
-echo '### Loading 100/fourier.ml'; echo 'loadt "100/fourier.ml";;' | (time 
$hollight)
-echo '### Loading 100/four_squares.ml'; echo 'loadt "100/four_squares.ml";;' | 
(time $hollight)
-echo '### Loading 100/friendship.ml'; echo 'loadt "100/friendship.ml";;' | 
(time $hollight)
-echo '### Loading 100/fta.ml'; echo 'loadt "100/fta.ml";;' | (time $hollight)
-echo '### Loading 100/gcd.ml'; echo 'loadt "100/gcd.ml";;' | (time $hollight)
-echo '### Loading 100/heron.ml'; echo 'loadt "100/heron.ml";;' | (time 
$hollight)
-echo '### Loading 100/inclusion_exclusion.ml'; echo 'loadt 
"100/inclusion_exclusion.ml";;' | (time $hollight)
-echo '### Loading 100/isosceles.ml'; echo 'loadt "100/isosceles.ml";;' | (time 
$hollight)
-echo '### Loading 100/konigsberg.ml'; echo 'loadt "100/konigsberg.ml";;' | 
(time $hollight)
-echo '### Loading 100/lagrange.ml'; echo 'loadt "100/lagrange.ml";;' | (time 
$hollight)
-echo '### Loading 100/leibniz.ml'; echo 'loadt "100/leibniz.ml";;' | (time 
$hollight)
-echo '### Loading 100/lhopital.ml'; echo 'loadt "100/lhopital.ml";;' | (time 
$hollight)
-echo '### Loading 100/liouville.ml'; echo 'loadt "100/liouville.ml";;' | (time 
$hollight)
-echo '### Loading 100/minkowski.ml'; echo 'loadt "100/minkowski.ml";;' | (time 
$hollight)
-echo '### Loading 100/morley.ml'; echo 'loadt "100/morley.ml";;' | (time 
$hollight)
-echo '### Loading 100/pascal.ml'; echo 'loadt "100/pascal.ml";;' | (time 
$hollight)
-echo '### Loading 100/perfect.ml'; echo 'loadt "100/perfect.ml";;' | (time 
$hollight)
-echo '### Loading 100/pick.ml'; echo 'loadt "100/pick.ml";;' | (time $hollight)
-echo '### Loading 100/piseries.ml'; echo 'loadt "100/piseries.ml";;' | (time 
$hollight)
-echo '### Loading 100/platonic.ml'; echo 'loadt "100/platonic.ml";;' | (time 
$hollight)
-echo '### Loading 100/pnt.ml'; echo 'loadt "100/pnt.ml";;' | (time $hollight)
-echo '### Loading 100/polyhedron.ml'; echo 'loadt "100/polyhedron.ml";;' | 
(time $hollight)
-echo '### Loading 100/ptolemy.ml'; echo 'loadt "100/ptolemy.ml";;' | (time 
$hollight)
-echo '### Loading 100/pythagoras.ml'; echo 'loadt "100/pythagoras.ml";;' | 
(time $hollight)
-echo '### Loading 100/quartic.ml'; echo 'loadt "100/quartic.ml";;' | (time 
$hollight)
-echo '### Loading 100/ramsey.ml'; echo 'loadt "100/ramsey.ml";;' | (time 
$hollight)
-echo '### Loading 100/ratcountable.ml'; echo 'loadt "100/ratcountable.ml";;' | 
(time $hollight)
-echo '### Loading 100/realsuncountable.ml'; echo 'loadt 
"100/realsuncountable.ml";;' | (time $hollight)
-echo '### Loading 100/reciprocity.ml'; echo 'loadt "100/reciprocity.ml";;' | 
(time $hollight)
-echo '### Loading 100/stirling.ml'; echo 'loadt "100/stirling.ml";;' | (time 
$hollight)
-echo '### Loading 100/subsequence.ml'; echo 'loadt "100/subsequence.ml";;' | 
(time $hollight)
-echo '### Loading 100/thales.ml'; echo 'loadt "100/thales.ml";;' | (time 
$hollight)
-echo '### Loading 100/triangular.ml'; echo 'loadt "100/triangular.ml";;' | 
(time $hollight)
-echo '### Loading 100/two_squares.ml'; echo 'loadt "100/two_squares.ml";;' | 
(time $hollight)
-echo '### Loading 100/wilson.ml'; echo 'loadt "100/wilson.ml";;' | (time 
$hollight)
-
-# Build the proof-recording version of HOL
-# ... not on Debian
-# echo '### Building proof-recording version';
-# cd Proofrecording/hol_light
-# make clean; make hol
diff --git a/.pc/holtest-no-proof-recording.patch/.timestamp 
b/.pc/holtest-no-proof-recording.patch/.timestamp
deleted file mode 100644
index e69de29..0000000
diff --git a/.pc/holtest-no-proof-recording.patch/holtest 
b/.pc/holtest-no-proof-recording.patch/holtest
deleted file mode 100755
index d992148..0000000
--- a/.pc/holtest-no-proof-recording.patch/holtest
+++ /dev/null
@@ -1,167 +0,0 @@
-#!/bin/bash
-#######################################################################
-# Load in a bunch of examples to test HOL Light is working properly
-# Try examining the output using something like
-#
-#     egrep -i '###|error|not.found' nohup.out
-#
-# to see progress and whether anything has gone wrong.
-#
-# You might first want to install the necessary external tools,
-# for instance with
-#
-#   aptitude install prover9 coinor-csdp pari-gp
-#
-#######################################################################
-
-set -e
-
-if which hol-light > /dev/null ; then
-    hollight=hol-light
-else
-    # Make sure we have an up-to-date hol, and Mizar Light extensions
-    make hol
-    (cd Mizarlight; make clean; make)
-    hollight=./hol
-fi
-
-# Standalone examples
-
-echo '### Loading Library/agm.ml'; echo 'loadt "Library/agm.ml";;' | (time 
$hollight)
-echo '### Loading Library/binary.ml'; echo 'loadt "Library/binary.ml";;' | 
(time $hollight)
-echo '### Loading Library/binomial.ml'; echo 'loadt "Library/binomial.ml";;' | 
(time $hollight)
-echo '### Loading Examples/borsuk.ml'; echo 'loadt "Examples/borsuk.ml";;' | 
(time $hollight)
-echo '### Loading Examples/brunn_minkowski.ml'; echo 'loadt 
"Examples/brunn_minkowski.ml";;' | (time $hollight)
-echo '### Loading Library/card.ml'; echo 'loadt "Library/card.ml";;' | (time 
$hollight)
-echo '### Loading Examples/combin.ml'; echo 'loadt "Examples/combin.ml";;' | 
(time $hollight)
-echo '### Loading Examples/cong.ml'; echo 'loadt "Examples/cong.ml";;' | (time 
$hollight)
-echo '### Loading Examples/cooper.ml'; echo 'loadt "Examples/cooper.ml";;' | 
(time $hollight)
-echo '### Loading Examples/dlo.ml'; echo 'loadt "Examples/dlo.ml";;' | (time 
$hollight)
-echo '### Loading Library/floor.ml'; echo 'loadt "Library/floor.ml";;' | (time 
$hollight)
-echo '### Loading Examples/forster.ml'; echo 'loadt "Examples/forster.ml";;' | 
(time $hollight)
-echo '### Loading Examples/hol88.ml'; echo 'loadt "Examples/hol88.ml";;' | 
(time $hollight)
-echo '### Loading Examples/holby.ml'; echo 'loadt "Examples/holby.ml";;' | 
(time $hollight)
-echo '### Loading Library/integer.ml'; echo 'loadt "Library/integer.ml";;' | 
(time $hollight)
-echo '### Loading Library/isum.ml'; echo 'loadt "Library/isum.ml";;' | (time 
$hollight)
-echo '### Loading Examples/kb.ml'; echo 'loadt "Examples/kb.ml";;' | (time 
$hollight)
-echo '### Loading Examples/lagrange_lemma.ml'; echo 'loadt 
"Examples/lagrange_lemma.ml";;' | (time $hollight)
-echo '### Loading Examples/mangoldt.ml'; echo 'loadt "Examples/mangoldt.ml";;' 
| (time $hollight)
-echo '### Loading Examples/mccarthy.ml'; echo 'loadt "Examples/mccarthy.ml";;' 
| (time $hollight)
-echo '### Loading Examples/mizar.ml'; echo 'loadt "Examples/mizar.ml";;' | 
(time $hollight)
-echo '### Loading Library/multiplicative.ml'; echo 'loadt 
"Library/multiplicative.ml";;' | (time $hollight)
-echo '### Loading Examples/multiwf.ml'; echo 'loadt "Examples/multiwf.ml";;' | 
(time $hollight)
-echo '### Loading Examples/pell.ml'; echo 'loadt "Examples/pell.ml";;' | (time 
$hollight)
-echo '### Loading Library/permutations.ml'; echo 'loadt 
"Library/permutations.ml";;' | (time $hollight)
-echo '### Loading Library/primitive.ml'; echo 'loadt "Library/primitive.ml";;' 
| (time $hollight)
-echo '### Loading Library/products.ml'; echo 'loadt "Library/products.ml";;' | 
(time $hollight)
-echo '### Loading Examples/prog.ml'; echo 'loadt "Examples/prog.ml";;' | (time 
$hollight)
-echo '### Loading Examples/prover9.ml'; echo 'loadt "Examples/prover9.ml";;' | 
(time $hollight)
-echo '### Loading Examples/rectypes.ml'; echo 'loadt "Examples/rectypes.ml";;' 
| (time $hollight)
-echo '### Loading Examples/schnirelmann.ml'; echo 'loadt 
"Examples/schnirelmann.ml";;' | (time $hollight)
-echo '### Loading Examples/solovay.ml'; echo 'loadt "Examples/solovay.ml";;' | 
(time $hollight)
-echo '### Loading Examples/sos.ml'; echo 'loadt "Examples/sos.ml";;' | (time 
$hollight)
-echo '### Loading Examples/ste.ml'; echo 'loadt "Examples/ste.ml";;' | (time 
$hollight)
-echo '### Loading Library/wo.ml'; echo 'loadt "Library/wo.ml";;' | (time 
$hollight)
-echo '### Loading 
Library/analysis.ml,/transc.ml,calc_real.ml,machin.ml,polylog.ml,poly.ml';
-(echo 'loadt "Library/analysis.ml";;'; echo 'loadt "Library/transc.ml";;';
- echo 'loadt "Library/calc_real.ml";;'; echo 'loadt "Examples/machin.ml";;';
- echo 'loadt "Examples/polylog.ml";;'; echo 'loadt "Library/poly.ml";;') | 
(time $hollight)
-echo '### Loading Library/prime.ml,pratt.ml';
-(echo 'loadt "Library/prime.ml";;'; echo 'loadt "Library/pratt.ml";;') | (time 
$hollight)
-echo '### Loading Library/prime.ml,pocklington.ml';
-(echo 'loadt "Library/prime.ml";;'; echo 'loadt "Library/pocklington.ml";;') | 
(time $hollight)
-echo '### Loading Library/rstc.ml,reduct.ml';
-(echo 'loadt "Library/rstc.ml";;'; echo 'loadt "Examples/reduct.ml";;') | 
(time $hollight)
-
-# Extended examples
-
-echo '### Loading Arithmetic/make.ml'; echo 'loadt "Arithmetic/make.ml";;' | 
(time $hollight)
-echo '### Loading Boyer_Moore/make.ml'; echo 'loadt "Boyer_Moore/make.ml";;' | 
(time $hollight)
-echo '### Loading Complex/make.ml'; echo 'loadt "Complex/make.ml";;' | (time 
$hollight)
-echo '### Loading IsabelleLight/make.ml'; echo 'loadt 
"IsabelleLight/make.ml";;' | (time $hollight)
-echo '### Loading Jordan/make.ml'; echo 'loadt "Jordan/make.ml";;' | (time 
$hollight)
-echo '### Loading Mizarlight/make.ml'; echo 'loadt "Mizarlight/make.ml";;' | 
(time $hollight)
-echo '### Loading miz3/make.ml, miz3/test.ml (twice)'; (echo 'loadt 
"miz3/make.ml";;'; echo 'loadt "miz3/test.ml";;'; echo 'loadt 
"miz3/test.ml";;') | (time $hollight)
-if which zchaff > /dev/null ; then
-    echo '### Loading Minisat/make.ml,Minisat/taut.ml';
-    (echo 'loadt "Minisat/make.ml";;'; echo 'loadt "Minisat/taut.ml";;') | 
(time $hollight)
-else
-    echo '### Error: skip Minisat/make.ml, Minisat/taut.ml because zchaff is 
not available'
-fi
-echo '### Loading Model/make.ml'; echo 'loadt "Model/make.ml";;' | (time 
$hollight)
-echo '### Loading Multivariate/make.ml'; echo 'loadt "Multivariate/make.ml";;' 
| (time $hollight)
-echo '### Loading Multivariate/make_complex.ml'; echo 'loadt 
"Multivariate/make_complex.ml";;' | (time $hollight)
-echo '### Loading Ntrie/ntrie.ml'; echo 'loadt "Ntrie/ntrie.ml";;' | (time 
$hollight)
-echo '### Loading Permutation/make.ml'; echo 'loadt "Permutation/make.ml";;' | 
(time $hollight)
-echo '### Loading QBF/make.ml'; echo 'loadt "QBF/make.ml";;' | (time $hollight)
-echo '### Loading Rqe/make.ml'; echo 'loadt "Rqe/make.ml";;' | (time $hollight)
-echo '### Loading Unity/make.ml'; echo 'loadt "Unity/make.ml";;' | (time 
$hollight)
-echo '### Loading Multivariate/geom.ml'; echo 'loadt "Multivariate/geom.ml";;' 
| (time $hollight)
-echo '### Loading Multivariate/cross.ml'; echo 'loadt 
"Multivariate/cross.ml";;' | (time $hollight)
-echo '### Loading Multivariate/flyspeck.ml'; echo 'loadt 
"Multivariate/flyspeck.ml";;' | (time $hollight)
-
-# Some of the "Great 100 theorems"
-
-echo '### Loading 100/arithmetic_geometric_mean.ml'; echo 'loadt 
"100/arithmetic_geometric_mean.ml";;' | (time $hollight)
-echo '### Loading 100/arithmetic.ml'; echo 'loadt "100/arithmetic.ml";;' | 
(time $hollight)
-echo '### Loading 100/ballot.ml'; echo 'loadt "100/ballot.ml";;' | (time 
$hollight)
-echo '### Loading 100/bernoulli.ml'; echo 'loadt "100/bernoulli.ml";;' | (time 
$hollight)
-echo '### Loading 100/bertrand.ml,100/primerecip.ml';
-(echo 'loadt "100/bertrand.ml";;'; echo 'loadt "100/primerecip.ml";;') | (time 
$hollight)
-echo '### Loading 100/birthday.ml'; echo 'loadt "100/birthday.ml";;' | (time 
$hollight)
-echo '### Loading 100/cantor.ml'; echo 'loadt "100/cantor.ml";;' | (time 
$hollight)
-echo '### Loading 100/ceva.ml'; echo 'loadt "100/ceva.ml";;' | (time $hollight)
-echo '### Loading 100/circle.ml'; echo 'loadt "100/circle.ml";;' | (time 
$hollight)
-echo '### Loading 100/chords.ml'; echo 'loadt "100/chords.ml";;' | (time 
$hollight)
-echo '### Loading 100/combinations.ml'; echo 'loadt "100/combinations.ml";;' | 
(time $hollight)
-echo '### Loading 100/constructible.ml'; echo 'loadt "100/constructible.ml";;' 
| (time $hollight)
-echo '### Loading 100/cosine.ml'; echo 'loadt "100/cosine.ml";;' | (time 
$hollight)
-echo '### Loading 100/cubic.ml'; echo 'loadt "100/cubic.ml";;' | (time 
$hollight)
-echo '### Loading 100/derangements.ml'; echo 'loadt "100/derangements.ml";;' | 
(time $hollight)
-echo '### Loading 100/desargues.ml'; echo 'loadt "100/desargues.ml";;' | (time 
$hollight)
-echo '### Loading 100/dirichlet.ml'; echo 'loadt "100/dirichlet.ml";;' | (time 
$hollight)
-echo '### Loading 100/div3.ml'; echo 'loadt "100/div3.ml";;' | (time $hollight)
-echo '### Loading 100/divharmonic.ml'; echo 'loadt "100/divharmonic.ml";;' | 
(time $hollight)
-echo '### Loading 100/e_is_transcendental.ml'; echo 'loadt 
"100/e_is_transcendental.ml";;' | (time $hollight)
-echo '### Loading 100/euler.ml'; echo 'loadt "100/euler.ml";;' | (time 
$hollight)
-echo '### Loading 100/fourier.ml'; echo 'loadt "100/fourier.ml";;' | (time 
$hollight)
-echo '### Loading 100/four_squares.ml'; echo 'loadt "100/four_squares.ml";;' | 
(time $hollight)
-echo '### Loading 100/friendship.ml'; echo 'loadt "100/friendship.ml";;' | 
(time $hollight)
-echo '### Loading 100/fta.ml'; echo 'loadt "100/fta.ml";;' | (time $hollight)
-echo '### Loading 100/gcd.ml'; echo 'loadt "100/gcd.ml";;' | (time $hollight)
-echo '### Loading 100/heron.ml'; echo 'loadt "100/heron.ml";;' | (time 
$hollight)
-echo '### Loading 100/inclusion_exclusion.ml'; echo 'loadt 
"100/inclusion_exclusion.ml";;' | (time $hollight)
-echo '### Loading 100/isosceles.ml'; echo 'loadt "100/isosceles.ml";;' | (time 
$hollight)
-echo '### Loading 100/konigsberg.ml'; echo 'loadt "100/konigsberg.ml";;' | 
(time $hollight)
-echo '### Loading 100/lagrange.ml'; echo 'loadt "100/lagrange.ml";;' | (time 
$hollight)
-echo '### Loading 100/leibniz.ml'; echo 'loadt "100/leibniz.ml";;' | (time 
$hollight)
-echo '### Loading 100/lhopital.ml'; echo 'loadt "100/lhopital.ml";;' | (time 
$hollight)
-echo '### Loading 100/liouville.ml'; echo 'loadt "100/liouville.ml";;' | (time 
$hollight)
-echo '### Loading 100/minkowski.ml'; echo 'loadt "100/minkowski.ml";;' | (time 
$hollight)
-echo '### Loading 100/morley.ml'; echo 'loadt "100/morley.ml";;' | (time 
$hollight)
-echo '### Loading 100/pascal.ml'; echo 'loadt "100/pascal.ml";;' | (time 
$hollight)
-echo '### Loading 100/perfect.ml'; echo 'loadt "100/perfect.ml";;' | (time 
$hollight)
-echo '### Loading 100/pick.ml'; echo 'loadt "100/pick.ml";;' | (time $hollight)
-echo '### Loading 100/piseries.ml'; echo 'loadt "100/piseries.ml";;' | (time 
$hollight)
-echo '### Loading 100/platonic.ml'; echo 'loadt "100/platonic.ml";;' | (time 
$hollight)
-echo '### Loading 100/pnt.ml'; echo 'loadt "100/pnt.ml";;' | (time $hollight)
-echo '### Loading 100/polyhedron.ml'; echo 'loadt "100/polyhedron.ml";;' | 
(time $hollight)
-echo '### Loading 100/ptolemy.ml'; echo 'loadt "100/ptolemy.ml";;' | (time 
$hollight)
-echo '### Loading 100/pythagoras.ml'; echo 'loadt "100/pythagoras.ml";;' | 
(time $hollight)
-echo '### Loading 100/quartic.ml'; echo 'loadt "100/quartic.ml";;' | (time 
$hollight)
-echo '### Loading 100/ramsey.ml'; echo 'loadt "100/ramsey.ml";;' | (time 
$hollight)
-echo '### Loading 100/ratcountable.ml'; echo 'loadt "100/ratcountable.ml";;' | 
(time $hollight)
-echo '### Loading 100/realsuncountable.ml'; echo 'loadt 
"100/realsuncountable.ml";;' | (time $hollight)
-echo '### Loading 100/reciprocity.ml'; echo 'loadt "100/reciprocity.ml";;' | 
(time $hollight)
-echo '### Loading 100/stirling.ml'; echo 'loadt "100/stirling.ml";;' | (time 
$hollight)
-echo '### Loading 100/subsequence.ml'; echo 'loadt "100/subsequence.ml";;' | 
(time $hollight)
-echo '### Loading 100/thales.ml'; echo 'loadt "100/thales.ml";;' | (time 
$hollight)
-echo '### Loading 100/triangular.ml'; echo 'loadt "100/triangular.ml";;' | 
(time $hollight)
-echo '### Loading 100/two_squares.ml'; echo 'loadt "100/two_squares.ml";;' | 
(time $hollight)
-echo '### Loading 100/wilson.ml'; echo 'loadt "100/wilson.ml";;' | (time 
$hollight)
-
-# Build the proof-recording version of HOL
-
-echo '### Building proof-recording version';
-cd Proofrecording/hol_light
-make clean; make hol
diff --git a/debian/patches/holtest-dependency-hint.patch 
b/debian/patches/holtest-dependency-hint.patch
deleted file mode 100644
index 7a97bac..0000000
--- a/debian/patches/holtest-dependency-hint.patch
+++ /dev/null
@@ -1,13 +0,0 @@
-Description: add ocamlgraph dependency comment in holtest for QBF
-Author: Hendrik Tews <hend...@askra.de>
---- a/holtest
-+++ b/holtest
-@@ -10,7 +10,7 @@
- # You might first want to install the necessary external tools,
- # for instance with
- #
--#   aptitude install prover9 coinor-csdp pari-gp
-+#   aptitude install prover9 coinor-csdp pari-gp libocamlgraph-ocaml-dev
- #
- #######################################################################
- 
diff --git a/debian/patches/series b/debian/patches/series
index c4fb8a5..0c7a73b 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,3 +1,2 @@
 default-hollight-dir
 holtest-no-proof-recording.patch
-holtest-dependency-hint.patch
diff --git a/hol.ml b/hol.ml
index c19c860..843b11f 100644
--- a/hol.ml
+++ b/hol.ml
@@ -11,16 +11,8 @@
 
 let hol_version = "2.20++";;
 
-let debian_hol_light_dir = "/usr/share/hol-light"
-
 let hol_dir = ref
-  (try Sys.getenv "HOLLIGHT_DIR"
-   with Not_found ->
-     try
-       if Sys.is_directory debian_hol_light_dir
-       then debian_hol_light_dir
-       else raise (Sys_error "")
-     with Sys_error _ -> Sys.getcwd());;
+  (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;
 
 (* ------------------------------------------------------------------------- *)
 (* Should eventually change to "ref(Filename.temp_dir_name)".                *)
diff --git a/holtest b/holtest
index 671113e..d992148 100755
--- a/holtest
+++ b/holtest
@@ -10,7 +10,7 @@
 # You might first want to install the necessary external tools,
 # for instance with
 #
-#   aptitude install prover9 coinor-csdp pari-gp libocamlgraph-ocaml-dev
+#   aptitude install prover9 coinor-csdp pari-gp
 #
 #######################################################################
 
@@ -161,7 +161,7 @@ echo '### Loading 100/two_squares.ml'; echo 'loadt 
"100/two_squares.ml";;' | (ti
 echo '### Loading 100/wilson.ml'; echo 'loadt "100/wilson.ml";;' | (time 
$hollight)
 
 # Build the proof-recording version of HOL
-# ... not on Debian
-# echo '### Building proof-recording version';
-# cd Proofrecording/hol_light
-# make clean; make hol
+
+echo '### Building proof-recording version';
+cd Proofrecording/hol_light
+make clean; make hol

-- 
hol-light packaging

_______________________________________________
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits

Reply via email to