Last modifications before upload.debian/8.0pl3+8.1alpha-1

9 files changed, 114 insertions, 10 deletions

diff --git a/debian/changelog b/debian/changelog
index b60769ed..c73a4116 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,10 +1,11 @@
 coq (8.0pl3+8.1alpha-1) experimental; urgency=low
 
   * New upstream release.
-  * Disabling checks for now as they don't succeed.
-  * Removed coq-8.0pl3-ocaml-3.09.dpatch.
   * No longer providing the compatibility coq7-libs package.
   * coq-libs is now providing its documentation in html format.
+  * Added browser.dpatch to use the default Debian browser for help.
+  * Disabling checks which don't succeed for now: failing_tests.dpatch.
+  * Removed coq-8.0pl3-ocaml-3.09.dpatch.
 
  -- Samuel Mimram <smimram@debian.org>  Thu, 27 Apr 2006 13:43:16 +0000
 
diff --git a/debian/control b/debian/control
index bd35a5ba..07eaacb2 100644
--- a/debian/control
+++ b/debian/control
@@ -10,7 +10,7 @@ Package: coq
 Architecture: any
 Depends: ${shlibs:Depends}, coq-libs (= ${Source-Version})
 Recommends: coqide | proofgeneral-coq
-Suggests: ocaml-nox (>= 3.08), proofgeneral-coq, ledit, cle
+Suggests: ocaml-nox (>= 3.08), proofgeneral-coq, ledit, cle, coq-doc
 Description: proof assistant for higher-order logic (toplevel and compiler)
  Coq is a proof assistant for higher-order logic, which allows the
  development of computer programs consistent with their formal
diff --git a/debian/coqide.desktop b/debian/coqide.desktop
index 1515c273..eec6e22b 100644
--- a/debian/coqide.desktop
+++ b/debian/coqide.desktop
@@ -1,9 +1,9 @@
 [Desktop Entry]
 Encoding=UTF-8
-Name=CoqIde
+Name=CoqIDE
 Comment=Graphical interface for the Coq proof assistant
 Exec=/usr/bin/coqide
 Type=Application
-Categories=GTK;Science;Math;
+Categories=Application;Development;Science;Math;IDE;GTK;
 Terminal=false
-Icon=/usr/share/pixmaps/coq.xpm
+Icon=coq.xpm
diff --git a/debian/coqide.menu b/debian/coqide.menu
index 0fb1935a..2bf7d541 100644
--- a/debian/coqide.menu
+++ b/debian/coqide.menu
@@ -1,4 +1,4 @@
 ?package(coqide):command="/usr/bin/coqide" \
   icon="/usr/share/pixmaps/coqide.xpm" \
   needs="X11" \
-  section="Apps/Math" title="CoqIde"
+  section="Apps/Math" title="CoqIDE"
diff --git a/debian/patches/00list b/debian/patches/00list
index fa82f62e..1fbe17e1 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1 +1,3 @@
 coqdoc_stdlib
+failing_tests
+browser
diff --git a/debian/patches/browser.dpatch b/debian/patches/browser.dpatch
new file mode 100755
index 00000000..ba55f3de
--- /dev/null
+++ b/debian/patches/browser.dpatch
@@ -0,0 +1,19 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## browser.dpatch by Samuel Mimram <smimram@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Use the default Debian browser for help.
+
+@DPATCH@
+diff -urNad coq-8.0pl3+8.1alpha~/lib/options.ml coq-8.0pl3+8.1alpha/lib/options.ml
+--- coq-8.0pl3+8.1alpha~/lib/options.ml	2005-12-26 20:07:21.000000000 +0000
++++ coq-8.0pl3+8.1alpha/lib/options.ml	2006-04-29 16:06:20.000000000 +0000
+@@ -117,7 +117,4 @@
+            "\" must contain exactly one placeholder \"%s\".")
+    else pre,post
+  with
+-  Not_found ->
+-   if Sys.os_type = "Win32"
+-   then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
+-   else "netscape -remote \"OpenURL(", ")\""
++  Not_found -> "/usr/bin/x-www-browser ", ""
diff --git a/debian/patches/failing_tests.dpatch b/debian/patches/failing_tests.dpatch
new file mode 100755
index 00000000..cc8429c8
--- /dev/null
+++ b/debian/patches/failing_tests.dpatch
@@ -0,0 +1,83 @@
+#! /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 2971382b..f23efc82 100755
--- a/debian/rules
+++ b/debian/rules
@@ -29,8 +29,7 @@ configure-stamp:
 build: patch-stamp configure-stamp build-stamp
 build-stamp:
 	dh_testdir
-	$(MAKE) world
-#	if grep -q BEST=opt config/Makefile; \
+	if grep -q BEST=opt config/Makefile; \
 	then \
 		($(MAKE) check \
 		   && touch opt-stamp) \
diff --git a/debian/watch b/debian/watch
index 8867705d..45c97702 100644
--- a/debian/watch
+++ b/debian/watch
@@ -1,2 +1,2 @@
-version=2
+version=3
 ftp://ftp.inria.fr/INRIA/coq/current/coq-([0-9a-z\.]*)\.tar\.gz debian uupdate