diff options
Diffstat (limited to 'debian/patches/fix-bytecode-build.patch')
-rw-r--r-- | debian/patches/fix-bytecode-build.patch | 102 |
1 files changed, 102 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!' |