New upstream release.debian/8.0pl3+8.1beta-1

6 files changed, 21 insertions, 149 deletions

diff --git a/debian/changelog b/debian/changelog
index 09834e6a..4f8d7e96 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,14 @@
+coq (8.0pl3+8.1beta-1) experimental; urgency=low
+
+  * New upstream release.
+  * Added --fsets all option to configure to build the theory of finite sets. 
+  * Updated coqdoc_stdlib.dpatch, partly integrated upstream.
+  * Removed failing_tests.dpath, all the tests should succeed now.
+  * We don't need to remove rpaths anymore.
+  * Updated standards version to 3.7.2, no changes needed.
+
+ -- Samuel Mimram <smimram@debian.org>  Fri, 16 Jun 2006 12:59:07 +0000
+
 coq (8.0pl3+8.1alpha-2) experimental; urgency=low
 
   * Added makefile.dpatch in order for ocamlopt not to be called when
diff --git a/debian/control b/debian/control
index 7b0cd6a4..3f15619d 100644
--- a/debian/control
+++ b/debian/control
@@ -3,8 +3,8 @@ Section: math
 Priority: optional
 Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
 Uploaders: Ralf Treinen <treinen@debian.org>, Sven Luther <luther@debian.org>, Remi Vanicat <vanicat@debian.org>, Stefano Zacchiroli <zack@debian.org>, Samuel Mimram <smimram@debian.org>
-Standards-Version: 3.6.2
-Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox (>= 3.09.0), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0), chrpath
+Standards-Version: 3.7.2
+Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox (>= 3.09.0), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0), tetex-extra, hevea
 
 Package: coq
 Architecture: any
diff --git a/debian/patches/00list b/debian/patches/00list
index 55a135be..cafb071e 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1,4 +1,3 @@
 coqdoc_stdlib
-failing_tests
 browser
 makefile
diff --git a/debian/patches/coqdoc_stdlib.dpatch b/debian/patches/coqdoc_stdlib.dpatch
index a2530876..fb618f56 100755
--- a/debian/patches/coqdoc_stdlib.dpatch
+++ b/debian/patches/coqdoc_stdlib.dpatch
@@ -6,9 +6,9 @@
 ## DP: to be able to build the documentation before coqdoc is installed.
 
 @DPATCH@
-diff -urNad coq-8.0pl3+8.1alpha~/doc/Makefile coq-8.0pl3+8.1alpha/doc/Makefile
---- coq-8.0pl3+8.1alpha~/doc/Makefile	2006-04-07 15:08:12.000000000 +0000
-+++ coq-8.0pl3+8.1alpha/doc/Makefile	2006-04-28 13:43:28.000000000 +0000
+diff -urNad coq-8.0pl3+8.1beta~/doc/Makefile coq-8.0pl3+8.1beta/doc/Makefile
+--- coq-8.0pl3+8.1beta~/doc/Makefile	2006-06-16 13:02:33.000000000 +0000
++++ coq-8.0pl3+8.1beta/doc/Makefile	2006-06-16 13:19:11.000000000 +0000
 @@ -216,6 +216,7 @@
  	mkdir stdlib/html
  	(cd stdlib/html;\
@@ -17,57 +17,3 @@ diff -urNad coq-8.0pl3+8.1alpha~/doc/Makefile coq-8.0pl3+8.1alpha/doc/Makefile
  	  -R $(COQTOP)/theories Coq $(COQTOP)/theories/*/*.v)
  	mv stdlib/html/index.html stdlib/index-body.html
  
-@@ -232,6 +233,7 @@
- stdlib/Library.coqdoc.tex: 
- 	(for dir in $(LIBDIRS) ; do \
- 	  $(COQDOC) -q --gallina --body-only --latex --stdout \
-+	    --coqlib_path $(COQTOP) \
-             -R $(COQTOP)/theories Coq "$(COQTOP)/theories/$$dir/"*.v >> $@ ; done)
- 
- stdlib/Library.dvi: $(COMMON) stdlib/Library.coqdoc.tex stdlib/Library.tex
-diff -urNad coq-8.0pl3+8.1alpha~/tools/coqdoc/cdglobals.ml coq-8.0pl3+8.1alpha/tools/coqdoc/cdglobals.ml
---- coq-8.0pl3+8.1alpha~/tools/coqdoc/cdglobals.ml	2006-03-08 10:47:12.000000000 +0000
-+++ coq-8.0pl3+8.1alpha/tools/coqdoc/cdglobals.ml	2006-04-28 13:41:09.000000000 +0000
-@@ -44,6 +44,7 @@
- let title = ref ""
- let externals = ref true
- let coqlib = ref "http://coq.inria.fr/library/"
-+let coqlib_path = ref Coq_config.coqlib
- let raw_comments = ref false
- 
- let charset = ref "iso-8859-1"
-diff -urNad coq-8.0pl3+8.1alpha~/tools/coqdoc/main.ml coq-8.0pl3+8.1alpha/tools/coqdoc/main.ml
---- coq-8.0pl3+8.1alpha~/tools/coqdoc/main.ml	2006-03-28 17:34:15.000000000 +0000
-+++ coq-8.0pl3+8.1alpha/tools/coqdoc/main.ml	2006-04-28 13:41:09.000000000 +0000
-@@ -54,6 +54,8 @@
-   prerr_endline "  --no-externals      no links to Coq standard library";
-   prerr_endline "  --coqlib <url>      set URL for Coq standard library";
-   prerr_endline "                      (default is http://coq.inria.fr/library/)";
-+  prerr_endline "  --coqlib_path <dir> path of the coqlibrary";
-+  prerr_endline ("                      (default is " ^ !Cdglobals.coqlib_path ^ ")");
-   prerr_endline "  -R <dir> <coqdir>   map physical dir to Coq dir";
-   prerr_endline "  --latin1            set ISO-8859-1 input language";
-   prerr_endline "  --utf8              set UTF-8 input language";
-@@ -315,6 +317,8 @@
- 	Cdglobals.externals := false; parse_rec rem
-     | ("--coqlib" | "-coqlib") :: u :: rem ->
- 	Cdglobals.coqlib := u; parse_rec rem
-+    | ("--coqlib_path" | "-coqlib_path") :: u :: rem ->
-+        Cdglobals.coqlib_path := u; parse_rec rem
-     | ("--coqlib" | "-coqlib") :: [] ->
- 	usage ()
-     | f :: rem -> 
-@@ -420,11 +424,11 @@
- let produce_document l =
-   List.iter index_module l;
-   (if !target_language=HTML then
--    let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.css") in
-+    let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in
-     let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in
-       copy src dst);
-   (if !target_language=LaTeX then
--    let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.sty") in
-+    let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
-     let dst = if !output_dir <> "" then 
-       Filename.concat !output_dir "coqdoc.sty" 
-     else "coqdoc.sty" in
diff --git a/debian/patches/failing_tests.dpatch b/debian/patches/failing_tests.dpatch
deleted file mode 100755
index cc8429c8..00000000
--- a/debian/patches/failing_tests.dpatch
+++ /dev/null
@@ -1,83 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## failing_tests.dpatch by Samuel Mimram <smimram@debian.org>
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: Remove tests which don't succeed!
-
-@DPATCH@
-diff -urNad coq-8.0pl3+8.1alpha~/test-suite/modules/mod_decl.v coq-8.0pl3+8.1alpha/test-suite/modules/mod_decl.v
---- coq-8.0pl3+8.1alpha~/test-suite/modules/mod_decl.v	2005-12-21 23:50:17.000000000 +0000
-+++ coq-8.0pl3+8.1alpha/test-suite/modules/mod_decl.v	1970-01-01 00:00:00.000000000 +0000
-@@ -1,49 +0,0 @@
--Module Type SIG.
--  Axiom A : Set.
--End SIG.
--
--Module M0.
--  Definition A : Set.
--  exact nat.
--  Qed.
--End M0.
--
--Module M1 : SIG.
--  Definition A := nat.
--End M1.
--
--Module M2 <: SIG.
--  Definition A := nat.
--End M2.
--
--Module M3 := M0.
--
--Module M4 : SIG := M0.
--
--Module M5 <: SIG := M0.
--
--
--Module F (X: SIG) := X.
--
--
--Module Type T.
--
--  Module M0.
--    Axiom A : Set.
--  End M0.
--  
--  Declare Module M1: SIG.
--  
--  Declare Module M2 <: SIG.
--    Definition A := nat.
--  End M2.
--  
--  Module M3 := M0.
--  
--  Module M4 : SIG := M0.
--  
--  Module M5 <: SIG := M0.
--
--  Module M6 := F M0.
--
--End T.
-diff -urNad coq-8.0pl3+8.1alpha~/test-suite/output/Cases.out coq-8.0pl3+8.1alpha/test-suite/output/Cases.out
---- coq-8.0pl3+8.1alpha~/test-suite/output/Cases.out	2005-12-21 23:50:17.000000000 +0000
-+++ coq-8.0pl3+8.1alpha/test-suite/output/Cases.out	1970-01-01 00:00:00.000000000 +0000
-@@ -1,9 +0,0 @@
--t_rect = 
--fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
--fix F (t : t) : P t :=
--  match t as t0 return (P t0) with
--  | k x x0 => f x0 (F x0)
--  end
--     : forall P : t -> Type,
--       (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
--
-diff -urNad coq-8.0pl3+8.1alpha~/test-suite/output/Cases.v coq-8.0pl3+8.1alpha/test-suite/output/Cases.v
---- coq-8.0pl3+8.1alpha~/test-suite/output/Cases.v	2005-12-21 23:50:17.000000000 +0000
-+++ coq-8.0pl3+8.1alpha/test-suite/output/Cases.v	1970-01-01 00:00:00.000000000 +0000
-@@ -1,6 +0,0 @@
--(* Cases with let-in in constructors types *)
--
--Inductive t : Set :=
--    k : let x := t in x -> x.
--
--Print t_rect.
diff --git a/debian/rules b/debian/rules
index 550349dd..57444fb7 100755
--- a/debian/rules
+++ b/debian/rules
@@ -13,7 +13,7 @@ include /usr/share/dpatch/dpatch.make
 COQPREF := $(CURDIR)/debian/tmp
 ADDPREF := COQINSTALLPREFIX=$(COQPREF)
 
-CONFIGUREOPTS := --prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq --reals all
+CONFIGUREOPTS := --prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq --reals all --fsets all
 
 configure: configure-stamp
 configure-stamp:
@@ -78,11 +78,10 @@ install: build
 		echo "Stripping: $$i"; \
 		strip -R .note -R .comment $$i; \
 	done
-	-for i in $(COQPREF)/usr/bin/coqide.*; do \
-		echo "Rpath for `chrpath $$i`"; \
-		echo "Removing rpath: $$i"; \
-		chrpath -d $$i; \
-	done
+	if [ -e opt-stamp ]; then \
+		strip -R .note -R .comment $ $(COQPREF)/usr/bin/coqc; \
+		strip -R .note -R .comment $(COQPREF)/usr/bin/coqmktop; \
+	fi
 	cp debian/coq.xpm debian/coq/usr/share/pixmaps/coq.xpm
 	cp debian/coq.xpm debian/coqide/usr/share/pixmaps/coqide.xpm
 	cp debian/coqide.desktop debian/coqide/usr/share/applications