Date: Friday, February 16, 2018 @ 09:01:42 Author: zorun Revision: 294970
upgpkg: coq 8.7.2-1 Deleted: coq/trunk/Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch coq/trunk/fix-num-build.patch ------------------------------------------------------------+ Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch | 58 ----------- fix-num-build.patch | 47 -------- 2 files changed, 105 deletions(-) Deleted: Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch =================================================================== --- Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch 2018-02-16 09:00:00 UTC (rev 294969) +++ Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch 2018-02-16 09:01:42 UTC (rev 294970) @@ -1,58 +0,0 @@ -From 8e7b876b6d9f3d4131e3b7e969f8e1943154df4c Mon Sep 17 00:00:00 2001 -From: Vincent Laporte <[email protected]> -Date: Thu, 28 Dec 2017 13:24:12 +0000 -Subject: [PATCH] [Makefile] plugins micromega and nsatz depend on unix and num - ---- - Makefile.build | 24 ++++++++++++++++++++++++ - 1 file changed, 24 insertions(+) - -diff --git a/Makefile.build b/Makefile.build -index 33ab72e68..5c454a145 100644 ---- a/Makefile.build -+++ b/Makefile.build -@@ -606,10 +606,26 @@ COND_BYTEFLAGS= \ - COND_OPTFLAGS= \ - $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(OPTFLAGS) - -+plugins/micromega/%.cmi: plugins/micromega/%.mli -+ $(SHOW)'OCAMLC $<' -+ $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< -+ -+plugins/nsatz/%.cmi: plugins/nsatz/%.mli -+ $(SHOW)'OCAMLC $<' -+ $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< -+ - %.cmi: %.mli - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< - -+plugins/micromega/%.cmo: plugins/micromega/%.ml -+ $(SHOW)'OCAMLC $<' -+ $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< -+ -+plugins/nsatz/%.cmo: plugins/nsatz/%.ml -+ $(SHOW)'OCAMLC $<' -+ $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< -+ - %.cmo: %.ml - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< -@@ -643,6 +659,14 @@ plugins/micromega/sos_FORPACK:= - plugins/micromega/sos_print_FORPACK:= - plugins/micromega/csdpcert_FORPACK:= - -+plugins/micromega/%.cmx: plugins/micromega/%.ml -+ $(SHOW)'OCAMLOPT $<' -+ $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $< -+ -+plugins/nsatz/%.cmx: plugins/nsatz/%.ml -+ $(SHOW)'OCAMLOPT $<' -+ $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $< -+ - plugins/%.cmx: plugins/%.ml - $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $< --- -2.16.1 - Deleted: fix-num-build.patch =================================================================== --- fix-num-build.patch 2018-02-16 09:00:00 UTC (rev 294969) +++ fix-num-build.patch 2018-02-16 09:01:42 UTC (rev 294970) @@ -1,47 +0,0 @@ -From 330564fff5946c0cd11b6744443bae95cf54019b Mon Sep 17 00:00:00 2001 -From: Emilio Jesus Gallego Arias <[email protected]> -Date: Tue, 30 Jan 2018 21:10:58 +0100 -Subject: [PATCH] [make] Fix build in split `num` configuration. - -It seems that recent fixes using ocamlbuild to locate num missed to -switch in some binaries. This is needed to solve problems like the -one in this issue: https://github.com/ocaml/opam-repository/issues/11316 ---- - Makefile.build | 2 +- - tools/coqmktop.ml | 3 ++- - 2 files changed, 3 insertions(+), 2 deletions(-) - -diff --git a/Makefile.build b/Makefile.build -index b0e7546113d..312ce53dd88 100644 ---- a/Makefile.build -+++ b/Makefile.build -@@ -530,7 +530,7 @@ CSDPCERTCMO:=lib/clib.cma $(addprefix plugins/micromega/, \ - - $(CSDPCERT): $(call bestobj, $(CSDPCERTCMO)) - $(SHOW)'OCAMLBEST -o $@' -- $(HIDE)$(call bestocaml,,nums unix) -+ $(HIDE)$(call bestocaml,-linkpkg -package num -package unix,) - - ########################################################################### - # tests -diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml -index 950ed53ccf7..c387c879824 100644 ---- a/tools/coqmktop.ml -+++ b/tools/coqmktop.ml -@@ -108,7 +108,7 @@ let incl_all_subdirs dir opts = - - (** OCaml + CamlpX libraries *) - --let ocaml_libs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"] -+let ocaml_libs = ["str.cma";"dynlink.cma"] - let camlp4_libs = ["gramlib.cma"] - let libobjs = ocaml_libs @ camlp4_libs - -@@ -289,6 +289,7 @@ let main () = - List.filter ((<>) "") (split_on_char ' ' Coq_config.caml_flags) in - let args = - coq_camlflags @ "-linkall" :: "-w" :: "-31" :: flags @ copts @ options @ -+ ["-linkpkg"; "-package"; "num"] @ - (std_includes basedir) @ tolink @ [ main_file ] @ topstart - in - if !echo then begin
