[Pkg-ocaml-maint-commits] r5973 - /tags/packages/edos-debcheck/1.0-8/
Author: treinen Date: Sun Sep 7 15:14:11 2008 New Revision: 5973 URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/?sc=1rev=5973 Log: [svn-buildpackage] Tagging edos-debcheck (1.0-8) Added: tags/packages/edos-debcheck/1.0-8/ - copied from r5972, trunk/packages/edos-debcheck/trunk/ ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [SCM] coq packaging branch, master, updated. debian/8.2.beta4+dfsg-2-6-ge9ca8bf
The following commit has been merged in the master branch: commit cdce320e124a3fcba458fad3c638940ce8f993ce Author: Stephane Glondu [EMAIL PROTECTED] Date: Sun Sep 7 18:05:26 2008 +0200 Bump debhelper compatibility level to 7 diff --git a/debian/compat b/debian/compat index b8626c4..7f8f011 100644 --- a/debian/compat +++ b/debian/compat @@ -1 +1 @@ -4 +7 diff --git a/debian/control b/debian/control index 6df245e..d84be0b 100644 --- a/debian/control +++ b/debian/control @@ -9,7 +9,16 @@ Uploaders: Ralf Treinen [EMAIL PROTECTED], Stephane Glondu [EMAIL PROTECTED] DM-Upload-Allowed: yes Standards-Version: 3.8.0 -Build-Depends: debhelper (= 4.0.0), dpkg-dev (= 1.13.19), dpatch, ocaml-nox (= 3.10), ocaml-best-compilers, camlp5, liblablgtk2-ocaml-dev (= 2.4.0), texlive-latex-extra, hevea +Build-Depends: + debhelper (= 7), + dpkg-dev (= 1.13.19), + dpatch, + ocaml-nox (= 3.10), + ocaml-best-compilers, + camlp5, + liblablgtk2-ocaml-dev (= 2.4.0), + texlive-latex-extra, + hevea Homepage: http://coq.inria.fr/ Vcs-Browser: http://git.debian.org/?p=pkg-ocaml-maint/packages/coq.git Vcs-Git: git://git.debian.org/git/pkg-ocaml-maint/packages/coq.git -- coq packaging ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [SCM] coq packaging branch, master, updated. debian/8.2.beta4+dfsg-2-6-ge9ca8bf
The following commit has been merged in the master branch:
commit b6db9f4f71b806d89cd24db386a6bcdd3b469d31
Author: Stephane Glondu [EMAIL PROTECTED]
Date: Sun Sep 7 18:58:27 2008 +0200
Remove obsolete patches
diff --git a/debian/patches/00list b/debian/patches/00list
index fb3801f..e69de29 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1,4 +0,0 @@
-no-complexity-test
-check
-use-env-in-coq-config
-non-native-archs
diff --git a/debian/patches/check.dpatch b/debian/patches/check.dpatch
deleted file mode 100755
index d0cb390..000
--- a/debian/patches/check.dpatch
+++ /dev/null
@@ -1,19 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## check.dpatch by Samuel Mimram [EMAIL PROTECTED]
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: Suppress warnings from tests outputs.
-
[EMAIL PROTECTED]@
-diff -urNad coq~/test-suite/check coq/test-suite/check
coq~/test-suite/check 2008-07-25 15:36:31.0 +0200
-+++ coq/test-suite/check 2008-07-25 15:36:31.0 +0200
-@@ -52,7 +52,7 @@
- nbtests=`expr $nbtests + 1`
- printf $f...
- tmpoutput=`mktemp /tmp/coqcheck.XX`
-- $command $f 21 | grep -v Welcome to Coq | grep -v Skipping rcfile
loading $tmpoutput
-+ $command $f 21 | grep -v Welcome to Coq | grep -v Skipping rcfile
loading | grep -v some rule has been masked $tmpoutput
- foutput=`dirname $f`/`basename $f .v`.out
- diff $tmpoutput $foutput /dev/null
- if [ $? = 0 ]; then
diff --git a/debian/patches/no-complexity-test.dpatch
b/debian/patches/no-complexity-test.dpatch
deleted file mode 100755
index 5f9bff6..000
--- a/debian/patches/no-complexity-test.dpatch
+++ /dev/null
@@ -1,21 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## no-complexity-test.dpatch by Julien Cristau [EMAIL PROTECTED]
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: Don't run complexity tests, they are far too fragile.
-
[EMAIL PROTECTED]@
-diff -urNad coq~/test-suite/check coq/test-suite/check
coq~/test-suite/check 2008-07-25 15:13:00.0 +0200
-+++ coq/test-suite/check 2008-07-25 15:33:55.0 +0200
-@@ -250,8 +250,8 @@
- test_interactive interactive
- echo Micromega tests
- test_success micromega
--echo Complexity tests
--test_complexity complexity
-+echo Skipping complexity tests
-+#test_complexity complexity
- echo Module tests
- $coqtop -compile modules/Nat
- $coqtop -compile modules/plik
diff --git a/debian/patches/non-native-archs.dpatch
b/debian/patches/non-native-archs.dpatch
deleted file mode 100755
index cbb9f83..000
--- a/debian/patches/non-native-archs.dpatch
+++ /dev/null
@@ -1,32 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## non-native-archs.dpatch by Stephane Glondu [EMAIL PROTECTED]
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: Fix FTBFS on non-native architectures
-
[EMAIL PROTECTED]@
-diff --git a/Makefile.build b/Makefile.build
-index a5bae4e..c47b688 100644
a/Makefile.build
-+++ b/Makefile.build
-@@ -655,7 +655,10 @@ install-library:
- $(MKDIR) $(FULLCOQLIB)/states
- $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
- $(MKDIR) $(FULLCOQLIB)/user-contrib
-- $(INSTALLLIB) $(LINKCMO) $(LINKCMX) $(GRAMMARCMA) $(FULLCOQLIB)
-+ $(INSTALLLIB) $(LINKCMO) $(GRAMMARCMA) $(FULLCOQLIB)
-+ifeq ($(BEST),opt)
-+ $(INSTALLLIB) $(LINKCMX) $(FULLCOQLIB)
-+endif
- find . -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \;
-
- install-library-light:
-@@ -716,7 +719,7 @@ dev/printers.cma: $(PRINTERSCMO)
- parsing/grammar.cma: $(GRAMMARCMO)
- $(SHOW)'Testing $@'
- @touch test.ml4
-- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp $(CAMLP4O) $(CAMLP4EXTENDFLAGS)
$(GRAMMARCMO) -impl -impl test.ml4 -o test-grammar
-+ $(HIDE)$(OCAMLC) $(OPTFLAGS) -pp $(CAMLP4O) $(CAMLP4EXTENDFLAGS)
$(GRAMMARCMO) -impl -impl test.ml4 -o test-grammar
- @rm -f test-grammar test.*
- $(SHOW)'OCAMLC -a $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@
diff --git a/debian/patches/use-env-in-coq-config.dpatch
b/debian/patches/use-env-in-coq-config.dpatch
deleted file mode 100755
index 1f01315..000
--- a/debian/patches/use-env-in-coq-config.dpatch
+++ /dev/null
@@ -1,24 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## use-env-in-coq-config.dpatch by Stephane Glondu [EMAIL PROTECTED]
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: Use environment variables by default in coq_config.ml
-
[EMAIL PROTECTED]@
-diff --git a/configure b/configure
-index 2747ee2..a57b996 100755
a/configure
-+++ b/configure
-@@ -862,9 +862,9 @@ cat END_OF_COQ_CONFIG $mlconfig_file
- (* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
-
- let local = $local
--let bindir = $ESCBINDIR
--let coqlib = $ESCLIBDIR
--let coqtop = $ESCCOQTOP
-+let bindir = try Sys.getenv COQBIN with
[Pkg-ocaml-maint-commits] [SCM] coq packaging branch, master, updated. debian/8.2.beta4+dfsg-2-6-ge9ca8bf
The following commit has been merged in the master branch:
commit d8e408268a5d4c59770e5ce02d6c814f751caed3
Author: Stephane Glondu [EMAIL PROTECTED]
Date: Sun Sep 7 18:58:58 2008 +0200
Use debhelper 7, simplify debian/rules
diff --git a/debian/control b/debian/control
index d84be0b..a24e091 100644
--- a/debian/control
+++ b/debian/control
@@ -2,7 +2,8 @@ Source: coq
Section: math
Priority: optional
Maintainer: Debian OCaml Maintainers [EMAIL PROTECTED]
-Uploaders: Ralf Treinen [EMAIL PROTECTED],
+Uploaders:
+ Ralf Treinen [EMAIL PROTECTED],
Remi Vanicat [EMAIL PROTECTED],
Stefano Zacchiroli [EMAIL PROTECTED],
Samuel Mimram [EMAIL PROTECTED],
@@ -43,7 +44,11 @@ Description: proof assistant for higher-order logic
(toplevel and compiler)
Package: coqide
Architecture: any
-Depends: ${shlibs:Depends}, ${misc:Depends}, coq (= 8.0)
+Depends:
+ ${shlibs:Depends},
+ coq (= ${binary:Version}),
+ ocaml-base-nox-${F:OCamlABI},
+ ${misc:Depends}
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
diff --git a/debian/coq-libs.links b/debian/coq-libs.links
new file mode 100644
index 000..9a521ba
--- /dev/null
+++ b/debian/coq-libs.links
@@ -0,0 +1 @@
+/usr/share/doc/coq-libs/html /usr/share/doc/coq/stdlib-html
diff --git a/debian/coq.dirs b/debian/coq.dirs
deleted file mode 100644
index 1166b15..000
--- a/debian/coq.dirs
+++ /dev/null
@@ -1,5 +0,0 @@
-usr/bin
-usr/lib
-usr/lib/coq
-usr/share/man/man1
-usr/share/pixmaps
diff --git a/debian/coq.dirs.in b/debian/coq.dirs.in
new file mode 100644
index 000..20f8dc0
--- /dev/null
+++ b/debian/coq.dirs.in
@@ -0,0 +1,6 @@
+usr/bin
+usr/lib/coq/contrib/micromega
+usr/share/man/man1
+usr/share/pixmaps
+usr/share/texmf/tex/latex/misc
+usr/lib/ocaml/@OCamlABI@/stublibs
diff --git a/debian/coq.install b/debian/coq.install
deleted file mode 100644
index 0648440..000
--- a/debian/coq.install
+++ /dev/null
@@ -1,18 +0,0 @@
-usr/bin/coqc
-usr/bin/coqdep
-usr/bin/coqdoc
-usr/bin/coq-interface*
-usr/bin/coq_makefile
-usr/bin/coqmktop
-usr/bin/coq-tex
-usr/bin/coqtop*
-usr/bin/coqwc
-usr/bin/gallina
-usr/bin/csdpcert
-usr/lib/coq/*.cm*
-usr/lib/coq/tools/coqdoc/
-usr/share/emacs/site-lisp/coq/*
-usr/share/man/man1/c*
-usr/share/man/man1/gallina.1
-usr/share/texmf/tex/latex/misc/*
-usr/share/emacs/site-lisp/coqdoc.styusr/share/texmf/tex/latex/misc/
diff --git a/debian/coq.install.in b/debian/coq.install.in
new file mode 100644
index 000..5bb62f2
--- /dev/null
+++ b/debian/coq.install.in
@@ -0,0 +1,28 @@
+usr/bin/coqc*
+usr/bin/coqdep*
+usr/bin/coqdoc*
+usr/bin/coq_makefile*
+usr/bin/coqmktop*
+usr/bin/coq-interface*
+usr/bin/coq-parser*
+usr/bin/coq-tex*
+usr/bin/coqtop*
+usr/bin/coqwc*
+usr/bin/gallina*
+usr/lib/coq/contrib/micromega/csdpcert*
+usr/lib/coq/*.cm*
+usr/lib/coq/tools/coqdoc/
+usr/share/emacs/site-lisp/coq/
+usr/share/man/man1/coqc*
+usr/share/man/man1/coqdep*
+usr/share/man/man1/coqdoc*
+usr/share/man/man1/coq_makefile*
+usr/share/man/man1/coqmktop*
+usr/share/man/man1/coq-interface*
+usr/share/man/man1/coq-parser*
+usr/share/man/man1/coq-tex*
+usr/share/man/man1/coqtop*
+usr/share/man/man1/coqwc*
+usr/share/man/man1/gallina*
+usr/lib/coq/dllcoqrun.so usr/lib/ocaml/@OCamlABI@/stublibs
+usr/share/emacs/site-lisp/coqdoc.sty usr/share/texmf/tex/latex/misc/
diff --git a/debian/coq.links.in b/debian/coq.links.in
new file mode 100644
index 000..250c321
--- /dev/null
+++ b/debian/coq.links.in
@@ -0,0 +1,2 @@
+OPT: /usr/share/man/man1/coq-interface.1
/usr/share/man/man1/coq-interface.opt.1
+OPT: /usr/share/man/man1/coq-parser.1 /usr/share/man/man1/coq-parser.opt.1
diff --git a/debian/coqide.install b/debian/coqide.install
index 238c4fd..dd6bf11 100644
--- a/debian/coqide.install
+++ b/debian/coqide.install
@@ -1,3 +1,4 @@
usr/bin/coqide*
usr/lib/coq/ide/coq.png
usr/lib/coq/ide/.coqide-gtk2rc
+usr/share/man/man1/coqide*
diff --git a/debian/coqide.links.in b/debian/coqide.links.in
new file mode 100644
index 000..c73095f
--- /dev/null
+++ b/debian/coqide.links.in
@@ -0,0 +1,2 @@
+/usr/share/man/man1/coqide.1 /usr/share/man/man1/coqide.byte.1
+OPT: /usr/share/man/man1/coqide.1 /usr/share/man/man1/coqide.opt.1
diff --git a/debian/rules b/debian/rules
index 640fceb..19bd688 100755
--- a/debian/rules
+++ b/debian/rules
@@ -5,142 +5,78 @@
#export DH_VERBOSE=1
# This has to be exported to make some magic below work.
-export DH_OPTIONS
+export COQTEST_SKIPCOMPLEXITY = true
+export CAML_LD_LIBRARY_PATH = $(shell pwd)/kernel/byterun
# We want to use dpatch
include /usr/share/dpatch/dpatch.make
+HTMLDOC := doc/stdlib/html/index.html
+
COQPREF := $(CURDIR)/debian/tmp
ADDPREF := COQINSTALLPREFIX=$(COQPREF)
+OFILES := $(patsubst %.in,%,$(wildcard debian/*.in))
OCAMLABI := $(shell ocamlc -version)
CONFIGUREOPTS := --arch Linux --prefix /usr --mandir /usr/share/man \
--emacslib
[Pkg-ocaml-maint-commits] [SCM] coq packaging branch, pristine-tar, updated. 7a4f7aac5a2b62098a484c3d996bf47db4c11ed0
The following commit has been merged in the pristine-tar branch: commit 7a4f7aac5a2b62098a484c3d996bf47db4c11ed0 Author: Stephane Glondu [EMAIL PROTECTED] Date: Mon Sep 8 00:21:18 2008 +0200 pristine-tar data for coq_8.2~beta4.svn20080907+dfsg.orig.tar.gz diff --git a/coq_8.2~beta4.svn20080907+dfsg.orig.tar.gz.delta b/coq_8.2~beta4.svn20080907+dfsg.orig.tar.gz.delta new file mode 100644 index 000..031a99e Binary files /dev/null and b/coq_8.2~beta4.svn20080907+dfsg.orig.tar.gz.delta differ diff --git a/coq_8.2~beta4.svn20080907+dfsg.orig.tar.gz.id b/coq_8.2~beta4.svn20080907+dfsg.orig.tar.gz.id new file mode 100644 index 000..dad0021 --- /dev/null +++ b/coq_8.2~beta4.svn20080907+dfsg.orig.tar.gz.id @@ -0,0 +1 @@ +113b703a695acbe31ac6dd6a8c4aa94f6fda7545 -- coq packaging ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/mailman/listinfo/pkg-ocaml-maint-commits
[Pkg-ocaml-maint-commits] [SCM] coq packaging annotated tag, upstream/8.2.beta4.svn20080907+dfsg, created. upstream/8.2.beta4.svn20080907+dfsg
The annotated tag, upstream/8.2.beta4.svn20080907+dfsg has been created at b5e6a28e8b7d1a69e5ee94a3f88878852b74c7ec (tag) tagging 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (commit) replaces upstream/8.2.beta4+dfsg tagged by Stephane Glondu on Mon Sep 8 00:15:04 2008 +0200 - Shortlog Upstream version 8.2~beta4.svn20080907+dfsg Stephane Glondu (1): Imported Upstream version 8.2~beta4.svn20080907+dfsg --- -- coq packaging ___ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/mailman/listinfo/pkg-ocaml-maint-commits
