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

[Baptiste Jonglez]

    Date: Tuesday, January 23, 2018 @ 11:45:55
  Author: zorun
Revision: 285533

coq: Initial work for building against ocaml 4.06

Added:
  coq/trunk/Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch
Modified:
  coq/trunk/PKGBUILD

------------------------------------------------------------+
 Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch |   58 +++++++++++
 PKGBUILD                                                   |   13 +-
 2 files changed, 67 insertions(+), 4 deletions(-)

Added: Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch
===================================================================
--- Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch	                        (rev 0)
+++ Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch	2018-01-23 11:45:55 UTC (rev 285533)
@@ -0,0 +1,58 @@
+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
+

Modified: PKGBUILD
===================================================================
--- PKGBUILD	2018-01-23 10:54:13 UTC (rev 285532)
+++ PKGBUILD	2018-01-23 11:45:55 UTC (rev 285533)
@@ -7,7 +7,7 @@
 
 pkgname=('coq' 'coqide' 'coq-doc')
 pkgver=8.7.1
-pkgrel=1
+pkgrel=2
 pkgdesc='Formal proof management system'
 arch=('x86_64')
 url='https://coq.inria.fr/'
@@ -14,14 +14,16 @@
 license=('GPL')
 groups=('coq')
 options=('!emptydirs')
-depends=('ocaml' 'camlp5' 'gtk2' 'gtksourceview2')
+depends=('ocaml' 'camlp5' 'ocaml-num' 'gtk2' 'gtksourceview2')
 makedepends=('ocaml-findlib'
              'lablgtk2' 'gendesk' # coqide
              'texlive-bin' 'texlive-latexextra' 'texlive-pictures' # coq-doc
              'texlive-fontsextra' 'texlive-science'
              'fig2dev' 'imagemagick' 'hevea' 'ghostscript')
-source=("coq-${pkgver}.tar.gz::https://github.com/coq/coq/archive/V${pkgver}.tar.gz")
-sha512sums=('43ef086de93bf99f94d74b9827dd16c79f4d24f5dd4332ee53bbd4588941cb602a64672638a3b3a56bfb612e4dbf7b2a3b5fd4921182dabbbe96e4fef07455b5')
+source=("coq-${pkgver}.tar.gz::https://github.com/coq/coq/archive/V${pkgver}.tar.gz"
+        "Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch")
+sha512sums=('43ef086de93bf99f94d74b9827dd16c79f4d24f5dd4332ee53bbd4588941cb602a64672638a3b3a56bfb612e4dbf7b2a3b5fd4921182dabbbe96e4fef07455b5'
+            'e974c2bbe15e177341a71518c0e02051ae82fc33c669c91c2d49562feb9dcb9fc1c4f59512bcbe3388b05ca486d066356390a4cef0799122c96422d1656383fb')
 
 prepare() {
   gendesk -f -n --pkgname "coqide" \
@@ -28,6 +30,9 @@
     --name "CoqIDE Proof Assistant" \
     --pkgdesc "Graphical interface for the Coq proof assistant" \
     --categories "Development;Science;Math;IDE;GTK"
+  cd "$srcdir/coq-$pkgver"
+  # Necessary since OCaml 4.06: Num is now a separate library.
+  patch -p1 < "$srcdir/Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch"
 }
 
 build() {