New upstream release: 8.0pl2.debian/8.0pl2-1

11 files changed, 67 insertions, 93 deletions

diff --git a/debian/README.Debian b/debian/README.Debian
index 5657bfca..685f6047 100644
--- a/debian/README.Debian
+++ b/debian/README.Debian
@@ -1,5 +1,28 @@
-Coq package for Debian
-----------------------
+--------------------------
++ Coq package for Debian +
+--------------------------
+
+Binary (in)compatibility
+------------------------
+The compiled libraries of Coq (the *.vo) are not expected to be backward or
+upward compatible between releases (including plX releases). In case of a new
+upstream release, your Coq files should be recompiled.
+
+
+Coq frontends
+-------------
+For interactive use of coqtop, we suggest
+- either the Debian cle package
+- or the Proof-General (x)emacs mode, which unfortunately can not be
+distributed by Debian for copyright reasons. However, a Debian package
+might become available at proof general home page in the future
+(http://zermelo.dcs.ed.ac.uk/~proofgen)
+
+However we recommand you to use the CoqIde gtk interface provided in coqide.
+
+
+Unstripped binaries
+-------------------
 
 Note that all bytecode files in this package need to be left
 'unstripped' after compiling. The reason is the following:
@@ -17,12 +40,3 @@ Note that all bytecode files in this package need to be left
 Moreover the bytecode version is installed even on platforms having a
 native version as the dynamic loading of tactics works only with the
 bytecode version.
-
-For interactive use of coqtop, we suggest
-- either the Debian cle package
-- or the Proof-General (x)emacs mode, which unfortunately can not be
-distributed by Debian for copyright reasons. However, a Debian package
-might become available at proof general home page in the future
-(http://zermelo.dcs.ed.ac.uk/~proofgen)
-
-However we recommand you to use the CoqIde gtk interface provided in coqide.
diff --git a/debian/TODO b/debian/TODO.Debian
index 783c4ca5..61d5189d 100644
--- a/debian/TODO
+++ b/debian/TODO.Debian
@@ -1,6 +1,3 @@
-* See if the -libs are arch-independant (I'm not sure but they should be). If
-  it's the case change them to Arch: all.
-
 * Move the coqide stuff from /usr/lib/coq/ide to /usr/share/coqide. The variable
   lib_ide should be changed to do that.
 
diff --git a/debian/changelog b/debian/changelog
index e3ee6a8b..dca117be 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,17 @@
+coq (8.0pl2-1) unstable; urgency=low
+
+  * New upstream release.
+  * Put the libraries in arch all since they are supposed to be
+    arch-independant.
+  * Updated the README.Debian to explain that .vo are not compatible between
+    different upstream releases.
+  * Renamed coq.desktop into coqide.desktop, updated it and put it in
+    /usr/share/applications/ to be compliant with the policy.
+  * Description synopsis now begin with lowercase letters.
+  * Updated Standards-Version to 3.6.1.1.
+
+ -- Samuel Mimram <smimram@debian.org>  Mon, 31 Jan 2005 13:25:06 +0100
+
 coq (8.0pl1-5) unstable; urgency=low
 
   * Reuploaded since powerpc .deb did not include native code executable
diff --git a/debian/control b/debian/control
index c1b8f444..25695824 100644
--- a/debian/control
+++ b/debian/control
@@ -2,16 +2,16 @@ Source: coq
 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>, Jerome Marant <jerome@debian.org>, Remi Vanicat <vanicat@debian.org>, Stefano Zacchiroli <zack@debian.org>, Samuel Mimram <samuel.mimram@ens-lyon.org>
-Standards-Version: 3.6.1
+Uploaders: Ralf Treinen <treinen@debian.org>, Sven Luther <luther@debian.org>, Jerome Marant <jerome@debian.org>, Remi Vanicat <vanicat@debian.org>, Stefano Zacchiroli <zack@debian.org>, Samuel Mimram <smimram@debian.org>
+Standards-Version: 3.6.1.1
 Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox-3.08, ocaml-nox (>= 3.08.2), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0)
 
 Package: coq
 Architecture: any
-Depends: ${shlibs:Depends}, ${ocaml:Runtime}, coq-libs
-Suggests: ocaml-3.08, proofgeneral-coq, ledit, cle
+Depends: ${shlibs:Depends}, ${ocaml:Runtime}, coq-libs (= ${Source-Version})
 Recommends: coq-doc, coqide | proofgeneral-coq
-Description: Proof assistant for higher-order logic (toplevel and compiler)
+Suggests: ocaml-3.08, proofgeneral-coq, ledit, cle
+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
  specification. It is developed using Objective Caml and Camlp4.
@@ -27,7 +27,7 @@ Description: Proof assistant for higher-order logic (toplevel and compiler)
 Package: coqide
 Architecture: any
 Depends: ${shlibs:Depends}, ${ocaml:Runtime}, coq (>= 8.0), liblablgtk2-ocaml (>= 2.4.0)
-Description: Proof assistant for higher-order logic (gtk interface)
+Description: proof assistant for higher-order logic (gtk interface)
  Coq is a proof assistant for higher-order logic, which allows the
  development of computer programs consistent with their formal
  specification. It is developed using Objective Caml and Camlp4.
@@ -37,10 +37,10 @@ Description: Proof assistant for higher-order logic (gtk interface)
  developing proofs.
 
 Package: coq-libs
-Architecture: any
+Architecture: all
 Recommends: coq (>= 8.0)
 Conflicts: coq (<< 8.0)
-Description: Proof assistant for higher-order logic (theories)
+Description: proof assistant for higher-order logic (theories)
  Coq is a proof assistant for higher-order logic, which allows the
  development of computer programs consistent with their formal
  specification. It is developed using Objective Caml and Camlp4.
@@ -50,9 +50,9 @@ Description: Proof assistant for higher-order logic (theories)
  based upon, including theories of arithmetic and Boolean values.
 
 Package: coq7-libs
-Architecture: any
+Architecture: all
 Recommends: coq (>= 8.0)
-Description: Proof assistant for higher-order logic (Coq 7 theories)
+Description: proof assistant for higher-order logic (Coq 7 theories)
  Coq is a proof assistant for higher-order logic, which allows the
  development of computer programs consistent with their formal
  specification. It is developed using Objective Caml and Camlp4.
diff --git a/debian/coq.desktop b/debian/coq.desktop
deleted file mode 100644
index af2698ec..00000000
--- a/debian/coq.desktop
+++ /dev/null
@@ -1,7 +0,0 @@
-[Desktop Entry]
-Name=Coq
-Comment=Proof Assistant
-Exec=/usr/bin/coqide
-Type=Application
-Terminal=0
-Icon=/usr/share/pixmaps/coq.xpm
diff --git a/debian/coq.dirs b/debian/coq.dirs
index 90431880..1166b157 100644
--- a/debian/coq.dirs
+++ b/debian/coq.dirs
@@ -1,4 +1,5 @@
 usr/bin
 usr/lib
 usr/lib/coq
+usr/share/man/man1
 usr/share/pixmaps
diff --git a/debian/coqide.desktop b/debian/coqide.desktop
new file mode 100644
index 00000000..1515c273
--- /dev/null
+++ b/debian/coqide.desktop
@@ -0,0 +1,9 @@
+[Desktop Entry]
+Encoding=UTF-8
+Name=CoqIde
+Comment=Graphical interface for the Coq proof assistant
+Exec=/usr/bin/coqide
+Type=Application
+Categories=GTK;Science;Math;
+Terminal=false
+Icon=/usr/share/pixmaps/coq.xpm
diff --git a/debian/coqide.dirs b/debian/coqide.dirs
index 1add6cd0..3afbe849 100644
--- a/debian/coqide.dirs
+++ b/debian/coqide.dirs
@@ -1,3 +1,4 @@
+usr/lib/coq/ide
 usr/share/doc/coqide
-usr/share/applnk/Development
+usr/share/applications
 usr/share/man/man1
diff --git a/debian/patches/00list b/debian/patches/00list
index 089b7a7b..e69de29b 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1 +0,0 @@
-ocaml_3.08.1
diff --git a/debian/patches/ocaml_3.08.1.dpatch b/debian/patches/ocaml_3.08.1.dpatch
deleted file mode 100755
index 8327a7ae..00000000
--- a/debian/patches/ocaml_3.08.1.dpatch
+++ /dev/null
@@ -1,55 +0,0 @@
-#! /bin/sh -e
-## ocaml_3.08.1.dpatch by Michel Mauny <Michel.Mauny@inria.fr>
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: Add parenthesis to arguments of fun since without parenthesis is not accepted anymore by ocaml.
-
-if [ $# -lt 1 ]; then
-    echo "`basename $0`: script expects -patch|-unpatch as argument" >&2
-    exit 1
-fi
-
-[ -f debian/patches/00patch-opts ] && . debian/patches/00patch-opts
-patch_opts="${patch_opts:--f --no-backup-if-mismatch} ${2:+-d $2}"
-
-case "$1" in
-    -patch) patch -p1 ${patch_opts} < $0;;
-    -unpatch) patch -R -p1 ${patch_opts} < $0;;
-    *)
-        echo "`basename $0`: script expects -patch|-unpatch as argument" >&2
-        exit 1;;
-esac
-
-exit 0
-
-@DPATCH@
-diff -urNad /home/smimram/work/gnu/pkg-ocaml-maint/coq/trunk/coq-8.0pl1/contrib/funind/tacinv.ml4 coq-8.0pl1/contrib/funind/tacinv.ml4
---- /home/smimram/work/gnu/pkg-ocaml-maint/coq/trunk/coq-8.0pl1/contrib/funind/tacinv.ml4	2004-02-10 17:22:14.000000000 +0100
-+++ coq-8.0pl1/contrib/funind/tacinv.ml4	2004-08-20 14:40:56.000000000 +0200
-@@ -495,7 +495,7 @@
-        let metav = mknewmeta() in
-        let substmeta t = popn 1 (substitterm 0 (mkRel 1) metav t) in
-        let newrec_call = substmeta rec_call in
--       let newlevar = List.map (fun ev,tev -> ev, substmeta tev) levar in
-+       let newlevar = List.map (fun (ev,tev) -> ev, substmeta tev) levar in
-        let newabsc = Array.map substmeta absc in
-        newrec_call,newlevar,lposeq,evararr,newabsc,((metav,nme, typ)::parms)
- 
-@@ -693,7 +693,7 @@
-  (* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *)
-  let gl_abstr' = add_lambdas (pf_concl gl) gl listargs' in
-  (* apply parameters immediately *)
-- let gl_abstr = applistc gl_abstr' (List.map (fun x,y,z -> x) (List.rev parms)) in
-+ let gl_abstr = applistc gl_abstr' (List.map (fun (x,y,z) -> x) (List.rev parms)) in
- 
-  (* we apply args of the fix now, the parameters will be applied later *)
-  let princ_proof_applied_args = 
-@@ -790,7 +790,7 @@
-  in
-  let rec princ_replace_params params t = 
-   List.fold_left (
--   fun acc ev,nam,typ -> 
-+   fun acc (ev,nam,typ) -> 
-     mkLambda (Name (id_of_name nam) , typ, 
-     substitterm 0 ev (mkRel 1) (lift 0 acc)))
-    t (List.rev params) in
diff --git a/debian/rules b/debian/rules
index d93631a9..dbc78be0 100755
--- a/debian/rules
+++ b/debian/rules
@@ -30,7 +30,6 @@ build-stamp:
 		|| (echo WARNING: NATIVE CODE COMPILATION FAILED \
 		   && echo Trying to build coq in bytecode instead \
 		   && $(MAKE) archclean clean \
-		   && touch test-suite/success/debian.v8 \
 		   && $(MAKE) BEST=byte HASCOQIDE=byte check \
 		   && echo NATIVE CODE COMPILATION FAILED \
 		   && echo Coq was built in bytecode instead); \
@@ -69,13 +68,11 @@ install: build
 		strip -R .note -R .comment $$i; \
 	done
 	cp debian/coq.xpm debian/coq/usr/share/pixmaps/coq.xpm
-	cp debian/coq.desktop debian/coqide/usr/share/applnk/Development
-
-	dh_install --sourcedir=$(COQPREF)
+	cp debian/coqide.desktop debian/coqide/usr/share/applications
 
 	cp ide/index_urls.txt debian/coqide/usr/lib/coq/ide/index_urls.txt
 	if [ -e opt-stamp ]; then \
-		cp debian/coq/usr/share/man/man1/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.opt.1; \
+		cp debian/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.opt.1; \
 		cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.opt.1; \
 	fi
 	cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.1
@@ -86,6 +83,9 @@ install: build
 	cp debian/coqmktop.1 debian/coq/usr/share/man/man1/coqmktop.1
 	cp debian/coqtop.1 debian/coq/usr/share/man/man1/coqtop.1
 
+	# These are installed as docs
+	rm -f $(COQPREF)/usr/lib/coq/ide/utf8.v $(COQPREF)/usr/lib/coq/ide/FAQ
+
 binary-indep: build install
 
 binary-arch: build install
@@ -94,6 +94,7 @@ binary-arch: build install
 	dh_installdocs
 	dh_installemacsen
 	dh_installchangelogs CHANGES
+	dh_install --sourcedir=$(COQPREF) --list-missing
 	dh_link
 	dh_compress
 	dh_fixperms