[arch-commits] Commit in coq/trunk (2 files)

[Baptiste Jonglez]

    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 <Vincent.Laporte at gmail.com>
-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 <e+git at x80.org>
-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