Fix build on platforms without ocamlopt

This includes disabling all unit tests, which require ocamlopt and
“don’t test much yet” anyway.

3 files changed, 122 insertions, 0 deletions

diff --git a/debian/patches/fix-bytecode-build.patch b/debian/patches/fix-bytecode-build.patch
new file mode 100644
index 00000000..e2cdaa7d
--- /dev/null
+++ b/debian/patches/fix-bytecode-build.patch
@@ -0,0 +1,102 @@
+From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
+Subject: Makefiles: Fixes for byte compilation
+Bug: https://github.com/coq/coq/issues/9464
+Origin: other, https://github.com/SkySkimmer/coq/commit/4308dd8cd6deff4db946faf11822c80d16ee77ea
+Reviewed-by: Benjamin Barenblat <bbaren@debian.org>
+
+- default targets don't depend on ocamlopt when it's unavailable
+- coqc.byte is built by byte target and coqc by coqbinaries target
+- unit tests use best ocaml
+- poly-capture-global-univs tests ml compilation with ocamlc
+
+Benjamin Barenblat modified this patch to apply cleanly on top of 8.9.0.
+--- a/Makefile.build
++++ b/Makefile.build
+@@ -237,6 +237,10 @@
+ BESTOBJ:=.cmo
+ BESTLIB:=.cma
+ BESTDYN:=.cma
++
++# needed while booting if non -local
++CAML_LD_LIBRARY_PATH := $(PWD)/kernel/byterun:$(CAML_LD_LIBRARY_PATH)
++export CAML_LD_LIBRARY_PATH
+ endif
+ 
+ define bestobj
+@@ -408,12 +412,12 @@
+ 
+ .PHONY: coqbinaries coqbyte
+ 
+-coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
+-coqbyte: $(TOPBYTE) $(CHICKENBYTE)
++coqbinaries: $(TOPBIN) $(COQC) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
++coqbyte: $(TOPBYTE) $(COQCBYTE) $(CHICKENBYTE)
+ 
+ # Special rule for coqtop, we imitate `ocamlopt` can delete the target
+ # to avoid #7666
+-$(COQTOPEXE): $(TOPBINOPT:.opt=.$(BEST))
++$(COQTOPEXE): $(TOPBIN)
+ 	rm -f $@ && cp $< $@
+ 
+ bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
+@@ -435,12 +439,12 @@
+ 
+ # Special rule for coqtop.byte
+ # VMBYTEFLAGS will either contain -custom of the right -dllpath for the VM
+-$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(COQTOP_BYTE)
++$(COQTOPBYTE): $(COQTOP_BYTE) $(LINKCMO) $(LIBCOQRUN)
+ 	$(SHOW)'COQMKTOP -o $@'
+ 	$(HIDE)$(OCAMLC) -linkall -linkpkg -I lib -I vernac -I toplevel \
+ 	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
+ 			 $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \
+-			 $(LINKCMO) $(BYTEFLAGS) $(COQTOP_BYTE) -o $@
++			 $(LINKCMO) $(BYTEFLAGS) $< -o $@
+ 
+ # For coqc
+ COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo
+@@ -567,7 +571,7 @@
+ 
+ FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo tools/fake_ide.cmo
+ 
+-$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP)
++$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPEXE)
+ 	$(SHOW)'OCAMLBEST -o $@'
+ 	$(HIDE)$(call bestocaml, -I ide -I ide/protocol -package str -package dynlink)
+ 
+--- a/Makefile.common
++++ b/Makefile.common
+@@ -74,10 +74,12 @@
+ # for Declare ML Module files.
+ 
+ ifeq ($(BEST),opt)
++TOPBIN:=$(TOPBINOPT)
+ COQTOPBEST:=$(COQTOPEXE)
+ DYNOBJ:=.cmxs
+ DYNLIB:=.cmxs
+ else
++TOPBIN:=$(TOPBYTE)
+ COQTOPBEST:=$(COQTOPBYTE)
+ DYNOBJ:=.cmo
+ DYNLIB:=.cma
+--- a/Makefile.install
++++ b/Makefile.install
+@@ -68,7 +68,7 @@
+ 
+ install-binaries: install-tools
+ 	$(MKDIR) $(FULLBINDIR)
+-	$(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBINOPT) $(FULLBINDIR)
++	$(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBIN) $(FULLBINDIR)
+ 
+ install-byte: install-coqide-byte
+ 	$(MKDIR) $(FULLBINDIR)
+--- a/test-suite/misc/poly-capture-global-univs.sh
++++ b/test-suite/misc/poly-capture-global-univs.sh
+@@ -11,7 +11,7 @@
+ 
+ make clean
+ 
+-make src/evil_plugin.cmxs
++make src/evil_plugin.cma
+ 
+ if make; then
+     >&2 echo 'Should have failed!'
diff --git a/debian/patches/remove-bytecode-failing-tests.patch b/debian/patches/remove-bytecode-failing-tests.patch
new file mode 100644
index 00000000..49fe7fc3
--- /dev/null
+++ b/debian/patches/remove-bytecode-failing-tests.patch
@@ -0,0 +1,18 @@
+From: Benjamin Barenblat <bbaren@debian.org>
+Subject: Disable tests which require ocamlopt
+Forwarded: not-needed
+
+Disable unit tests. They require ocamlopt, which isn't available on all
+Debian architectures, and Gaëtan Gilbert says that "they don't test much
+yet" anyway.
+--- a/test-suite/Makefile
++++ b/test-suite/Makefile
+@@ -102,7 +102,7 @@
+   coqdoc
+ 
+ # All subsystems
+-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools unit-tests
++SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools
+ 
+ PREREQUISITELOG = prerequisite/admit.v.log			\
+   prerequisite/make_local.v.log prerequisite/make_notation.v.log \
diff --git a/debian/patches/series b/debian/patches/series
index df422d2d..393f2c14 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -7,3 +7,5 @@ skip-dot-pc.patch
 remove-ssrmatching.patch
 spelling.patch
 verbose-build.patch
+fix-bytecode-build.patch
+remove-bytecode-failing-tests.patch