[Pkg-ocaml-maint-commits] r2644 - in /trunk/packages/coq/branches: ./ 8.0pl3+8.1alpha/ 8.0pl3+8.1alpha/debian/ 8.0pl3+8.1alpha/debian/patches/ upstream/

smimram at users.alioth.debian.org smimram at users.alioth.debian.org
Fri Apr 28 14:59:22 UTC 2006 

Author: smimram
Date: Fri Apr 28 14:59:16 2006
New Revision: 2644

URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/?sc=1&rev=2644
Log:
Started to package the upcoming 8.1 release.

Added:
    trunk/packages/coq/branches/
    trunk/packages/coq/branches/8.0pl3+8.1alpha/
      - copied from r2643, trunk/packages/coq/trunk/
    trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq-libs.dirs
    trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq-libs.doc-base
    trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/patches/coqdoc_stdlib.dpatch   (with props)
    trunk/packages/coq/branches/upstream/
    trunk/packages/coq/branches/upstream/coq_8.0pl3+8.1alpha.orig.tar.gz   (with props)
Removed:
    trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq7-libs.install
    trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch
Modified:
    trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/changelog
    trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/control
    trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq-libs.install
    trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq.install
    trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coqide.install
    trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/patches/00list
    trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/rules

Modified: trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/changelog
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/branches/8.0pl3%2B8.1alpha/debian/changelog?rev=2644&op=diff
==============================================================================
--- trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/changelog (original)
+++ trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/changelog Fri Apr 28 14:59:16 2006
@@ -1,3 +1,13 @@
+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.
+
+ -- Samuel Mimram <smimram at debian.org>  Thu, 27 Apr 2006 13:43:16 +0000
+
 coq (8.0pl3-2) unstable; urgency=low
 
   * Added coq-8.0pl3-ocaml-3.09.dpatch in order to prevent intuition from

Modified: trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/control
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/branches/8.0pl3%2B8.1alpha/debian/control?rev=2644&op=diff
==============================================================================
--- trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/control (original)
+++ trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/control Fri Apr 28 14:59:16 2006
@@ -4,7 +4,7 @@
 Maintainer: Debian OCaml Maintainers <debian-ocaml-maint at lists.debian.org>
 Uploaders: Ralf Treinen <treinen at debian.org>, Sven Luther <luther at debian.org>, Remi Vanicat <vanicat at debian.org>, Stefano Zacchiroli <zack at debian.org>, Samuel Mimram <smimram at 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
+Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox (>= 3.09.0), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0), chrpath, tetex-bin
 
 Package: coq
 Architecture: any
@@ -39,7 +39,7 @@
 Package: coq-libs
 Architecture: all
 Recommends: coq (>= 8.0)
-Conflicts: coq (<< 8.0)
+Conflicts: coq (<< 8.0), coq-doc (<= 8.0pl1.0-2)
 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
@@ -48,18 +48,3 @@
  .
  This package provides existing theories that new proofs can be
  based upon, including theories of arithmetic and Boolean values.
-
-Package: coq7-libs
-Architecture: all
-Recommends: coq (>= 8.0)
-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.
- For more information, see <http://coq.inria.fr/>.
- .
- This package provides existing theories from Coq 7 in Coq 8, and
- allows proofs that were developed in Coq 7 to be used in Coq 8.
- It is also required to translate theories in Coq 7 syntax into
- the new syntax introduced in Coq 8. However, this package does
- not need to be installed to use Coq 7.

Added: trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq-libs.dirs
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/branches/8.0pl3%2B8.1alpha/debian/coq-libs.dirs?rev=2644&op=file
==============================================================================
--- trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq-libs.dirs (added)
+++ trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq-libs.dirs Fri Apr 28 14:59:16 2006
@@ -1,0 +1,2 @@
+usr/share/doc/coq-libs
+usr/share/doc/coq

Added: trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq-libs.doc-base
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/branches/8.0pl3%2B8.1alpha/debian/coq-libs.doc-base?rev=2644&op=file
==============================================================================
--- trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq-libs.doc-base (added)
+++ trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq-libs.doc-base Fri Apr 28 14:59:16 2006
@@ -1,0 +1,9 @@
+Document: coq-library
+Title: The Coq Standard Library
+Author: The Coq Development Team
+Abstract: Standard Library documentation of version 8.0 of the Coq proof assistant which is a system designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specification.
+Section: Apps/Math
+
+Format: HTML
+Index: /usr/share/doc/coq-libs/html/index.html
+Files: /usr/share/doc/coq-libs/html/*.html

Modified: trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq-libs.install
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/branches/8.0pl3%2B8.1alpha/debian/coq-libs.install?rev=2644&op=diff
==============================================================================
--- trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq-libs.install (original)
+++ trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq-libs.install Fri Apr 28 14:59:16 2006
@@ -1,4 +1,4 @@
 usr/lib/coq/contrib
 usr/lib/coq/states
 usr/lib/coq/theories
-usr/lib/coq/ide/utf8.vo usr/lib/coq
+usr/lib/coq/ide/utf8.vo	usr/lib/coq

Modified: trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq.install
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/branches/8.0pl3%2B8.1alpha/debian/coq.install?rev=2644&op=diff
==============================================================================
--- trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq.install (original)
+++ trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coq.install Fri Apr 28 14:59:16 2006
@@ -9,7 +9,6 @@
 usr/bin/coqwc
 usr/bin/gallina
 usr/share/emacs/site-lisp/coq
-usr/share/emacs/site-lisp/coqdoc.sty
 usr/share/man/man1/c*
 usr/share/man/man1/gallina.1
 usr/share/texmf/tex/latex/misc/*

Modified: trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coqide.install
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/branches/8.0pl3%2B8.1alpha/debian/coqide.install?rev=2644&op=diff
==============================================================================
--- trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coqide.install (original)
+++ trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/coqide.install Fri Apr 28 14:59:16 2006
@@ -1,5 +1,4 @@
 usr/bin/coqide*
-usr/lib/coq/ide/coq.ico
-usr/lib/coq/ide/coq2.ico
+usr/lib/coq/ide/coq.png
 usr/lib/coq/ide/utf8.vo
 usr/lib/coq/ide/.coqide-gtk2rc

Modified: trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/patches/00list
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/branches/8.0pl3%2B8.1alpha/debian/patches/00list?rev=2644&op=diff
==============================================================================
--- trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/patches/00list (original)
+++ trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/patches/00list Fri Apr 28 14:59:16 2006
@@ -1,1 +1,1 @@
-coq-8.0pl3-ocaml-3.09
+coqdoc_stdlib

Added: trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/patches/coqdoc_stdlib.dpatch
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/branches/8.0pl3%2B8.1alpha/debian/patches/coqdoc_stdlib.dpatch?rev=2644&op=file
==============================================================================
--- trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/patches/coqdoc_stdlib.dpatch (added)
+++ trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/patches/coqdoc_stdlib.dpatch Fri Apr 28 14:59:16 2006
@@ -1,0 +1,72 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## coqdoc_stdlib.dpatch by Samuel Mimram <smimram at debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: No description.
+
+ at 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
+@@ -216,6 +216,7 @@
+ 	mkdir stdlib/html
+ 	(cd stdlib/html;\
+ 	 $(COQDOC) -q --multi-index --html --glob-from $(GLOBDUMP)\
++	  --coqlib_path $(COQTOP) \
+ 	  -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

Propchange: trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/patches/coqdoc_stdlib.dpatch
------------------------------------------------------------------------------
    svn:executable = *

Modified: trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/rules
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/branches/8.0pl3%2B8.1alpha/debian/rules?rev=2644&op=diff
==============================================================================
--- trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/rules (original)
+++ trunk/packages/coq/branches/8.0pl3+8.1alpha/debian/rules Fri Apr 28 14:59:16 2006
@@ -10,11 +10,10 @@
 # We want to use dpatch
 include /usr/share/dpatch/dpatch.make
 
-COQPREF=$(CURDIR)/debian/tmp
-ADDPREF=COQINSTALLPREFIX=$(COQPREF)
+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
 
 configure: configure-stamp
 configure-stamp:
@@ -30,7 +29,8 @@
 build: patch-stamp configure-stamp build-stamp
 build-stamp:
 	dh_testdir
-	if grep -q BEST=opt config/Makefile; \
+	$(MAKE) world
+#	if grep -q BEST=opt config/Makefile; \
 	then \
 		($(MAKE) check \
 		   && touch opt-stamp) \
@@ -43,6 +43,9 @@
 	else \
 		$(MAKE) BEST=byte HASCOQIDE=byte check; \
 	fi
+	$(MAKE) glob.dump
+	cp tools/coqdoc/coqdoc.sty doc/stdlib/
+	$(MAKE) -C doc stdlib
 	touch build-stamp
 
 clean: unpatch
@@ -55,6 +58,8 @@
 	rm -f bin/parser.opt
 	rm -f tools/coqdoc/*.cm[oi]
 	rm -f config/coq_config.ml config/Makefile test-suite/check.log
+	rm -f dev/ocamldebug-v7
+	rm -f ide/undo.mli glob.dump
 
 	dh_clean
 
@@ -96,7 +101,8 @@
 	cp debian/coqmktop.1 debian/coq/usr/share/man/man1/coqmktop.1
 	cp debian/coqtop.1 debian/coq/usr/share/man/man1/coqtop.1
 
-	chmod -x debian/tmp/usr/lib/coq/ide/coq2.ico
+	cp -r doc/stdlib/html debian/coq-libs/usr/share/doc/coq-libs/
+	cd debian/coq-libs/usr/share/doc/coq; ln -s ../coq-libs/html stdlib
 
 	# These are installed as docs
 	rm -f $(COQPREF)/usr/lib/coq/ide/utf8.v $(COQPREF)/usr/lib/coq/ide/FAQ

Added: trunk/packages/coq/branches/upstream/coq_8.0pl3+8.1alpha.orig.tar.gz
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/branches/upstream/coq_8.0pl3%2B8.1alpha.orig.tar.gz?rev=2644&op=file
==============================================================================
Binary file - no diff available.

Propchange: trunk/packages/coq/branches/upstream/coq_8.0pl3+8.1alpha.orig.tar.gz
------------------------------------------------------------------------------
    svn:mime-type = application/octet-stream

More information about the Pkg-ocaml-maint-commits mailing list