Use debhelper 7, simplify debian/rules

10 files changed, 93 insertions, 135 deletions

diff --git a/debian/control b/debian/control
index d84be0b3..a24e091e 100644
--- a/debian/control
+++ b/debian/control
@@ -2,7 +2,8 @@ Source: coq
 Section: math
 Priority: optional
 Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
-Uploaders: Ralf Treinen <treinen@debian.org>,
+Uploaders:
+ Ralf Treinen <treinen@debian.org>,
  Remi Vanicat <vanicat@debian.org>,
  Stefano Zacchiroli <zack@debian.org>,
  Samuel Mimram <smimram@debian.org>,
@@ -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 00000000..9a521ba8
--- /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 1166b157..00000000
--- 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 00000000..20f8dc0d
--- /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 06484408..00000000
--- 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 00000000..5bb62f26
--- /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 00000000..250c3210
--- /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 238c4fdd..dd6bf116 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 00000000..c73095fe
--- /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 640fceb8..19bd688d 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