Package coq_makefile’s new Python dependency

6 files changed, 67 insertions, 2 deletions

diff --git a/debian/control b/debian/control
index 0421b4c0..29f85268 100644
--- a/debian/control
+++ b/debian/control
@@ -11,13 +11,16 @@ Uploaders:
 Standards-Version: 4.3.0
 Build-Depends:
  debhelper (>= 10),
+ dh-exec,
  dh-ocaml (>= 0.9.5~),
+ dh-python,
  ocaml-nox (>= 4),
  ocaml-best-compilers,
  ocaml-findlib (>= 1.4),
  camlp5 (>= 5.12-2~),
  liblablgtk2-ocaml-dev (>= 2.14),
  liblablgtksourceview2-ocaml-dev,
+ python3,
  rsync,
  texlive-latex-extra,
  hevea (>= 1.10-7)
@@ -31,6 +34,7 @@ Depends:
  coq-theories (= ${binary:Version}),
  emacsen-common,
  ${ocaml:Depends},
+ ${python3:Depends},
  ${shlibs:Depends},
  ${misc:Depends}, 
  ocaml-best-compilers,
diff --git a/debian/coq.install.in b/debian/coq.install.in
index f8556a60..f2f5339f 100644
--- a/debian/coq.install.in
+++ b/debian/coq.install.in
@@ -1,3 +1,4 @@
+#!/usr/bin/dh-exec
 usr/bin/coqc*
 usr/bin/coqdep*
 usr/bin/coqdoc*
@@ -8,8 +9,13 @@ usr/bin/coqwc*
 usr/bin/gallina*
 usr/bin/coqworkmgr*
 usr/lib/coq/plugins/micromega/csdpcert
+usr/lib/coq/tools/CoqMakefile.in
+usr/lib/coq/tools/TimeFileMaker.py
 usr/lib/coq/tools/coqdoc/coqdoc.css
 usr/lib/coq/tools/coqdoc/coqdoc.sty
+usr/lib/coq/tools/make-both-single-timing-files.py => usr/lib/coq/tools/make-both-single-timing-files
+usr/lib/coq/tools/make-both-time-files.py => usr/lib/coq/tools/make-both-time-files
+usr/lib/coq/tools/make-one-time-file.py => usr/lib/coq/tools/make-one-time-file
 usr/share/emacs/site-lisp/coq/
 usr/share/man/man1/coqc*
 usr/share/man/man1/coqdep*
diff --git a/debian/patches/0008-avoid-usr-bin-env.patch b/debian/patches/0008-avoid-usr-bin-env.patch
new file mode 100644
index 00000000..132ed7aa
--- /dev/null
+++ b/debian/patches/0008-avoid-usr-bin-env.patch
@@ -0,0 +1,32 @@
+From: Benjamin Barenblat <bbaren@debian.org>
+Subject: Avoid invoking /usr/bin/env
+Forwarded: not-needed
+
+Per Debian Python policy [1], use `/usr/bin/python3` rather than
+`/usr/bin/env python` to refer to the system Python (3) interpreter.
+
+[1] https://www.debian.org/doc/packaging-manuals/python-policy/python.html#interpreter_loc
+--- a/tools/make-both-single-timing-files.py
++++ b/tools/make-both-single-timing-files.py
+@@ -1,4 +1,4 @@
+-#!/usr/bin/env python
++#!/usr/bin/python3
+ import sys
+ from TimeFileMaker import *
+ 
+--- a/tools/make-both-time-files.py
++++ b/tools/make-both-time-files.py
+@@ -1,4 +1,4 @@
+-#!/usr/bin/env python
++#!/usr/bin/python3
+ import sys
+ from TimeFileMaker import *
+ 
+--- a/tools/make-one-time-file.py
++++ b/tools/make-one-time-file.py
+@@ -1,4 +1,4 @@
+-#!/usr/bin/env python
++#!/usr/bin/python3
+ import sys
+ from TimeFileMaker import *
+ 
diff --git a/debian/patches/0009-python-scripts-libraries.patch b/debian/patches/0009-python-scripts-libraries.patch
new file mode 100644
index 00000000..66a4a9e9
--- /dev/null
+++ b/debian/patches/0009-python-scripts-libraries.patch
@@ -0,0 +1,20 @@
+From: Benjamin Barenblat <bbaren@debian.org>
+Subject: Differentiate between Python scripts and libraries
+Forwarded: not-needed
+
+Eliminate the .py extension from executable Python scripts.
+--- a/tools/CoqMakefile.in
++++ b/tools/CoqMakefile.in
+@@ -91,9 +91,9 @@
+ COQMKFILE ?= "$(COQBIN)coq_makefile"
+ 
+ # Timing scripts
+-COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py"
+-COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py"
+-COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py"
++COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file"
++COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files"
++COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files"
+ BEFORE ?=
+ AFTER ?=
+ 
diff --git a/debian/patches/series b/debian/patches/series
index b098f303..16ae3a4d 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -5,3 +5,5 @@
 0005-remove-ssrmatching.patch
 0006-remove-tests-that-need-coqlib.patch
 0007-spelling.patch
+0008-avoid-usr-bin-env.patch
+0009-python-scripts-libraries.patch
diff --git a/debian/rules b/debian/rules
index 55cd0491..7c820e03 100755
--- a/debian/rules
+++ b/debian/rules
@@ -45,13 +45,13 @@ export OCAMLINIT_SED += \
   -e 's%@CoqABI@%$(COQ_ABI)%'
 
 %:
-	+dh $@ --with ocaml
+	+dh $@ --with ocaml,python3
 
 # There is already a file named "build" in upstream sources, so the
 # above rule is never called. We make it explicitly a phony rule here.
 .PHONY: build
 build:
-	+dh $@ --with ocaml
+	+dh $@ --with ocaml,python3
 
 .PHONY: override_dh_auto_configure
 override_dh_auto_configure:
@@ -106,6 +106,7 @@ override_dh_auto_install:
 .PHONY: override_dh_install
 override_dh_install:
 	chmod a-x debian/tmp/usr/lib/coq/toploop/*cma
+	chmod +x debian/coq.install
 	dh_install --fail-missing
 
 .PHONY: override_dh_ocaml