Use debhelper 7, simplify debian/rules

1 files changed, 46 insertions, 110 deletions

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