diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-06 07:24:25 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-06 07:24:25 -0500 |
| commit | 4a85cdbc0796afd2e70a7daf30967dfa2fadbafd (patch) | |
| tree | 76432c8d8a20e646d231e9de12c4a196588cd886 /debian | |
| parent | 4bf1d996c98a37c312c5dddf418316d77086e9c2 (diff) | |
Update fix-bytecode-build.patch to latest version
The fix-bytecode-build.patch in previous commits works fine for
building and testing, but installation still fails on bytecode
platforms – the system tries to install .cmx files that don’t exist.
Update fix-bytecode-build.patch to the latest version from Gaëtan
Gilbert, which corrects the installation targets.
Diffstat (limited to 'debian')
| -rw-r--r-- | debian/patches/fix-bytecode-build.patch | 31 |
1 files changed, 30 insertions, 1 deletions
diff --git a/debian/patches/fix-bytecode-build.patch b/debian/patches/fix-bytecode-build.patch index e2cdaa7d..24fbe1ec 100644 --- a/debian/patches/fix-bytecode-build.patch +++ b/debian/patches/fix-bytecode-build.patch @@ -1,13 +1,14 @@ 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 +Origin: other, https://github.com/SkySkimmer/coq/commit/f29aa6720eba884533972530b4283bf19d8410aa 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 +- don't try to install .cmx and native-compute .o files Benjamin Barenblat modified this patch to apply cleanly on top of 8.9.0. --- a/Makefile.build @@ -89,6 +90,20 @@ Benjamin Barenblat modified this patch to apply cleanly on top of 8.9.0. install-byte: install-coqide-byte $(MKDIR) $(FULLBINDIR) +@@ -104,11 +104,11 @@ + $(MKDIR) $(FULLCOQLIB) + $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA) + $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) # Regular CMI files ++ $(INSTALLSH) $(FULLCOQLIB) $(TOOLS_HELPERS) ++ifeq ($(BEST),opt) + $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMX) # To avoid warning 58 "-opaque" + $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.cmx) # For static linking of plugins + $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.o) # For static linking of plugins +- $(INSTALLSH) $(FULLCOQLIB) $(TOOLS_HELPERS) +-ifeq ($(BEST),opt) + $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a) + endif + --- a/test-suite/misc/poly-capture-global-univs.sh +++ b/test-suite/misc/poly-capture-global-univs.sh @@ -11,7 +11,7 @@ @@ -100,3 +115,17 @@ Benjamin Barenblat modified this patch to apply cleanly on top of 8.9.0. if make; then >&2 echo 'Should have failed!' +--- a/Makefile.vofiles ++++ b/Makefile.vofiles +@@ -31,7 +31,10 @@ + + GLOBFILES:=$(ALLVO:.vo=.glob) + ifdef NATIVECOMPUTE +-NATIVEFILES := $(call vo_to_cm,$(ALLVO)) $(call vo_to_obj,$(ALLVO)) ++NATIVEFILES := $(call vo_to_cm,$(ALLVO)) ++ifeq ($(BEST),opt) ++NATIVEFILES += $(call vo_to_obj,$(ALLVO)) ++endif + else + NATIVEFILES := + endif |