From 4e783ae1e73875e34026baff95afc46351746098 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Tue, 5 Feb 2019 15:09:24 -0500 Subject: Fix build on platforms without ocamlopt MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This includes disabling all unit tests, which require ocamlopt and “don’t test much yet” anyway. --- debian/patches/fix-bytecode-build.patch | 102 +++++++++++++++++++++ debian/patches/remove-bytecode-failing-tests.patch | 18 ++++ debian/patches/series | 2 + 3 files changed, 122 insertions(+) create mode 100644 debian/patches/fix-bytecode-build.patch create mode 100644 debian/patches/remove-bytecode-failing-tests.patch 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 +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 + +- 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 +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 -- cgit v1.2.3