[Pkg-ocaml-maint-commits] r949 - in packages/coq/trunk: . debian debian/patches

Samuel Mimram smimram-guest@costa.debian.org
Mon, 31 Jan 2005 15:35:26 +0100 

Author: smimram-guest
Date: 2005-01-31 15:34:14 +0100 (Mon, 31 Jan 2005)
New Revision: 949

Added:
   packages/coq/trunk/coq_8.0pl2.orig.tar.gz
   packages/coq/trunk/debian/TODO.Debian
   packages/coq/trunk/debian/coqide.desktop
Removed:
   packages/coq/trunk/coq_8.0pl1.orig.tar.gz
   packages/coq/trunk/debian/TODO
   packages/coq/trunk/debian/coq.desktop
   packages/coq/trunk/debian/patches/ocaml_3.08.1.dpatch
Modified:
   packages/coq/trunk/debian/README.Debian
   packages/coq/trunk/debian/changelog
   packages/coq/trunk/debian/control
   packages/coq/trunk/debian/coq.dirs
   packages/coq/trunk/debian/coqide.dirs
   packages/coq/trunk/debian/patches/00list
   packages/coq/trunk/debian/rules
Log:
New upstream release: 8.0pl2.

Deleted: packages/coq/trunk/coq_8.0pl1.orig.tar.gz
===================================================================
(Binary files differ)

Added: packages/coq/trunk/coq_8.0pl2.orig.tar.gz
===================================================================
(Binary files differ)


Property changes on: packages/coq/trunk/coq_8.0pl2.orig.tar.gz
___________________________________________________________________
Name: svn:mime-type
   + application/octet-stream

Modified: packages/coq/trunk/debian/README.Debian
===================================================================
--- packages/coq/trunk/debian/README.Debian	2005-01-31 08:42:25 UTC (rev 948)
+++ packages/coq/trunk/debian/README.Debian	2005-01-31 14:34:14 UTC (rev 949)
@@ -1,6 +1,29 @@
-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 @@
 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.

Deleted: packages/coq/trunk/debian/TODO
===================================================================
--- packages/coq/trunk/debian/TODO	2005-01-31 08:42:25 UTC (rev 948)
+++ packages/coq/trunk/debian/TODO	2005-01-31 14:34:14 UTC (rev 949)
@@ -1,6 +0,0 @@
-* 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.
-

Copied: packages/coq/trunk/debian/TODO.Debian (from rev 870, packages/coq/trunk/debian/TODO)
===================================================================
--- packages/coq/trunk/debian/TODO	2004-12-13 15:43:13 UTC (rev 870)
+++ packages/coq/trunk/debian/TODO.Debian	2005-01-31 14:34:14 UTC (rev 949)
@@ -0,0 +1,3 @@
+* Move the coqide stuff from /usr/lib/coq/ide to /usr/share/coqide. The variable
+  lib_ide should be changed to do that.
+

Modified: packages/coq/trunk/debian/changelog
===================================================================
--- packages/coq/trunk/debian/changelog	2005-01-31 08:42:25 UTC (rev 948)
+++ packages/coq/trunk/debian/changelog	2005-01-31 14:34:14 UTC (rev 949)
@@ -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

Modified: packages/coq/trunk/debian/control
===================================================================
--- packages/coq/trunk/debian/control	2005-01-31 08:42:25 UTC (rev 948)
+++ packages/coq/trunk/debian/control	2005-01-31 14:34:14 UTC (rev 949)
@@ -2,16 +2,16 @@
 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
+Depends: ${shlibs:Depends}, ${ocaml:Runtime}, coq-libs (= ${Source-Version})
+Recommends: coq-doc, coqide | proofgeneral-coq
 Suggests: ocaml-3.08, proofgeneral-coq, ledit, cle
-Recommends: coq-doc, coqide | proofgeneral-coq
-Description: Proof assistant for higher-order logic (toplevel and compiler)
+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 @@
 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 @@
  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 @@
  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.

Deleted: packages/coq/trunk/debian/coq.desktop
===================================================================
--- packages/coq/trunk/debian/coq.desktop	2005-01-31 08:42:25 UTC (rev 948)
+++ packages/coq/trunk/debian/coq.desktop	2005-01-31 14:34:14 UTC (rev 949)
@@ -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

Modified: packages/coq/trunk/debian/coq.dirs
===================================================================
--- packages/coq/trunk/debian/coq.dirs	2005-01-31 08:42:25 UTC (rev 948)
+++ packages/coq/trunk/debian/coq.dirs	2005-01-31 14:34:14 UTC (rev 949)
@@ -1,4 +1,5 @@
 usr/bin
 usr/lib
 usr/lib/coq
+usr/share/man/man1
 usr/share/pixmaps

Copied: packages/coq/trunk/debian/coqide.desktop (from rev 870, packages/coq/trunk/debian/coq.desktop)
===================================================================
--- packages/coq/trunk/debian/coq.desktop	2004-12-13 15:43:13 UTC (rev 870)
+++ packages/coq/trunk/debian/coqide.desktop	2005-01-31 14:34:14 UTC (rev 949)
@@ -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

Modified: packages/coq/trunk/debian/coqide.dirs
===================================================================
--- packages/coq/trunk/debian/coqide.dirs	2005-01-31 08:42:25 UTC (rev 948)
+++ packages/coq/trunk/debian/coqide.dirs	2005-01-31 14:34:14 UTC (rev 949)
@@ -1,3 +1,4 @@
+usr/lib/coq/ide
 usr/share/doc/coqide
-usr/share/applnk/Development
+usr/share/applications
 usr/share/man/man1

Modified: packages/coq/trunk/debian/patches/00list
===================================================================
--- packages/coq/trunk/debian/patches/00list	2005-01-31 08:42:25 UTC (rev 948)
+++ packages/coq/trunk/debian/patches/00list	2005-01-31 14:34:14 UTC (rev 949)
@@ -1 +0,0 @@
-ocaml_3.08.1

Deleted: packages/coq/trunk/debian/patches/ocaml_3.08.1.dpatch
===================================================================
--- packages/coq/trunk/debian/patches/ocaml_3.08.1.dpatch	2005-01-31 08:42:25 UTC (rev 948)
+++ packages/coq/trunk/debian/patches/ocaml_3.08.1.dpatch	2005-01-31 14:34:14 UTC (rev 949)
@@ -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

Modified: packages/coq/trunk/debian/rules
===================================================================
--- packages/coq/trunk/debian/rules	2005-01-31 08:42:25 UTC (rev 948)
+++ packages/coq/trunk/debian/rules	2005-01-31 14:34:14 UTC (rev 949)
@@ -30,7 +30,6 @@
 		|| (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 @@
 		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
+	cp debian/coqide.desktop debian/coqide/usr/share/applications
 
-	dh_install --sourcedir=$(COQPREF)
-
 	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 @@
 	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 @@
 	dh_installdocs
 	dh_installemacsen
 	dh_installchangelogs CHANGES
+	dh_install --sourcedir=$(COQPREF) --list-missing
 	dh_link
 	dh_compress
 	dh_fixperms