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 0000000..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..0000000
--- 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 0000000..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..0000000
--- 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.sty usr/share/texmf/tex/latex/misc/
diff --git a/debian/coq.install.in b/debian/coq.install.in
new file mode 100644
index 0000000..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 0000000..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 0000000..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 /usr/share/emacs/site-lisp/coq --reals all --fsets all \
--browser "/usr/bin/x-www-browser %s &" \
- --with-doc no
+ --with-doc no --coqrunbyteflags "-dllib -lcoqrun"
+
+OCAMLINITSED := -e 's/@OCamlABI@/$(OCAMLABI)/g'
+
+ifeq ($(shell test -e /usr/bin/ocamlopt && echo yes),yes)
+ CONFIGUREOPTS += -opt
+ OCAMLINITSED += -e 's/^OPT: //'
+else
+ OCAMLINITSED += -e '/^OPT: /d'
+endif
+
+ocamlinit: ocamlinit-stamp
+ocamlinit-stamp:
+ for f in $(OFILES); do sed $(OCAMLINITSED) $$f.in > $$f; done
+ touch $@
configure: configure-stamp
-configure-stamp: patch-stamp
- dh_testdir
- # git doesn't handle empty directories, so we create them here
- -mkdir bin
- if [ -e /usr/bin/ocamlc.opt ]; \
- then \
- ./configure -opt $(CONFIGUREOPTS); \
- else \
- ./configure $(CONFIGUREOPTS); \
- fi
- touch configure-stamp
+configure-stamp: patch-stamp ocamlinit-stamp
+ dh build --before dh_auto_configure
+ ./configure $(CONFIGUREOPTS)
+ echo 'F:OCamlABI="$(OCAMLABI)"' > debian/substvars
+ touch $@
build: build-stamp
build-stamp: configure-stamp
dh_testdir
- if grep -q BEST=opt config/Makefile; \
- then \
- ($(MAKE) check \
- && touch opt-stamp) \
- || (echo WARNING: NATIVE CODE COMPILATION FAILED \
- && echo Trying to build coq in bytecode instead \
- && $(MAKE) archclean clean \
- && sed -i -e 's/best = "opt"/best = "byte"/'
config/coq_config.ml \
- && $(MAKE) BEST=byte HASCOQIDE=byte check \
- && echo NATIVE CODE COMPILATION FAILED \
- && echo Coq was built in bytecode instead); \
- else \
- $(MAKE) BEST=byte HASCOQIDE=byte check; \
- fi
- cp tools/coqdoc/coqdoc.sty doc/stdlib/
- $(MAKE) -f Makefile.stage3 doc/stdlib/html/index.html
COQDOC="bin/coqdoc --coqlib_path `pwd`"
- touch build-stamp
-
-clean: unpatch
- dh_testdir
- dh_testroot
- rm -f build-stamp configure-stamp opt-stamp install-stamp
-
- # Contains a directory ending in .d which breaks the clean rule
- # of upstream Makefile
- -rm -Rf debian/coq/etc
-
- [ ! -f config/Makefile ] || $(MAKE) clean
- [ ! -f config/Makefile ] || $(MAKE) archclean
- rm -f bin/*
- 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
- rm -f test-suite/modules/*.vo
- rm -f doc/stdlib/coqdoc.sty
-
- dh_clean
+ $(MAKE) STRIP=true check
+ if [ -f bin/coqtop.opt ]; then touch opt-stamp; fi
+ $(MAKE) COQDOC="bin/coqdoc --coqlib_path `pwd`" \
+ DOC_TARGETS=$(HTMLDOC) $(HTMLDOC)
+ dh build --after dh_auto_test
+ touch $@
install: install-stamp
install-stamp: build-stamp
- dh_testdir
- dh_testroot
- dh_clean -k
- dh_installdirs
-
- if [ -e opt-stamp ]; then \
- $(MAKE) $(ADDPREF) install; \
- else \
- $(MAKE) BEST=byte HASCOQIDE=byte $(ADDPREF) install; \
- fi
-
- -for i in $(COQPREF)/usr/bin/*.opt; do \
- echo "Stripping: $$i"; \
- strip -R .note -R .comment $$i; \
- done
- if [ -e opt-stamp ]; then \
- strip -R .note -R .comment $ $(COQPREF)/usr/bin/coqc; \
- strip -R .note -R .comment $(COQPREF)/usr/bin/coqmktop; \
- fi
- cp debian/coq.xpm debian/coq/usr/share/pixmaps/coq.xpm
+ dh install --before dh_auto_install
+ $(MAKE) $(ADDPREF) install
+ dh_install -XFAQ --list-missing
+ mv debian/coq-libs/usr/lib/coq/contrib/micromega/csdpcert
debian/coq/usr/lib/coq/contrib/micromega
+ cp debian/coq.xpm debian/coq/usr/share/pixmaps
cp debian/coq.xpm debian/coqide/usr/share/pixmaps/coqide.xpm
cp debian/coqide.desktop debian/coqide/usr/share/applications
-
- if [ -e opt-stamp ]; then \
- cp man/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 man/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.1
- cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.1
- cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.byte.1
-
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
+ dh install --after dh_install
+ touch $@
- # These are installed as docs
- rm -f $(COQPREF)/usr/lib/coq/ide/utf8.v $(COQPREF)/usr/lib/coq/ide/FAQ
+clean: unpatch
+ dh $@
+ rm -f debian/substvars $(OFILES)
- dh_install --sourcedir=$(COQPREF) --list-missing
- touch install-stamp
+binary-indep: install-stamp
+ dh $@
-binary-common:
- dh_testdir
- dh_testroot
- dh_installdocs
- dh_installmenu
- dh_installemacsen
- dh_installman
- dh_installchangelogs CHANGES
- dh_installtex
- dh_desktop
- dh_link
- dh_compress
- dh_fixperms
- dh_installdeb
- dh_shlibdeps
- dh_gencontrol -- -VF:OCamlABI="$(OCAMLABI)"
- dh_md5sums
- dh_builddeb
-
-binary-indep: build install
- $(MAKE) -f debian/rules DH_OPTIONS=-i binary-common
-
-binary-arch: build install
- $(MAKE) -f debian/rules DH_OPTIONS=-a binary-common
+binary-arch: install-stamp
+ dh $@
binary: binary-indep binary-arch
-.PHONY: build clean binary-indep binary-arch binary-common binary install
configure
+.PHONY: build clean binary-indep binary-arch binary install configure ocamlinit
--
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
