[arch-commits] Commit in coq/repos/community-x86_64 (4 files)
Baptiste Jonglez
zorun at archlinux.org
Fri Feb 16 09:01:57 UTC 2018
Date: Friday, February 16, 2018 @ 09:01:56
Author: zorun
Revision: 294971
archrelease: copy trunk to community-x86_64
Added:
coq/repos/community-x86_64/PKGBUILD
(from rev 294970, coq/trunk/PKGBUILD)
Deleted:
coq/repos/community-x86_64/Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch
coq/repos/community-x86_64/PKGBUILD
coq/repos/community-x86_64/fix-num-build.patch
------------------------------------------------------------+
Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch | 58 ---
PKGBUILD | 185 +++++------
fix-num-build.patch | 47 --
3 files changed, 89 insertions(+), 201 deletions(-)
Deleted: Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch
===================================================================
--- Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch 2018-02-16 09:01:42 UTC (rev 294970)
+++ Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch 2018-02-16 09:01:56 UTC (rev 294971)
@@ -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: PKGBUILD
===================================================================
--- PKGBUILD 2018-02-16 09:01:42 UTC (rev 294970)
+++ PKGBUILD 2018-02-16 09:01:56 UTC (rev 294971)
@@ -1,96 +0,0 @@
-# Maintainer: Baptiste Jonglez <baptiste--aur at jonglez dot org>
-# Contributor: acieroid
-# Contributor: spider-mario <spidermario at free.fr>
-# Contributor: Thomas Dziedzic < gostrc at gmail >
-# Contributor: George Giorgidze <giorgidze at gmail.com>
-# Contributor: William J. Bowman <bluephoenix47 at gmail.com>
-
-pkgname=('coq' 'coqide' 'coq-doc')
-pkgver=8.7.1
-pkgrel=3
-pkgdesc='Formal proof management system'
-arch=('x86_64')
-url='https://coq.inria.fr/'
-license=('GPL')
-groups=('coq')
-options=('!emptydirs')
-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"
- "Makefile-plugins-micromega-and-nsatz-depend-on-unix-.patch"
- "fix-num-build.patch")
-sha512sums=('43ef086de93bf99f94d74b9827dd16c79f4d24f5dd4332ee53bbd4588941cb602a64672638a3b3a56bfb612e4dbf7b2a3b5fd4921182dabbbe96e4fef07455b5'
- 'e974c2bbe15e177341a71518c0e02051ae82fc33c669c91c2d49562feb9dcb9fc1c4f59512bcbe3388b05ca486d066356390a4cef0799122c96422d1656383fb'
- '328723f14f5f07c93f0eff6e7468baf6034ce0ef4ae7c2a5d59ca0a774cab0eeddd444e2f511fbf2abc1e5c71560efedb46c75ec45cf070e42b2a22ae18fd4c6')
-
-prepare() {
- gendesk -f -n --pkgname "coqide" \
- --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"
- patch -p1 < "$srcdir/fix-num-build.patch"
-}
-
-build() {
- cd "$srcdir/coq-$pkgver"
-
- ./configure \
- -prefix '/usr' \
- -mandir '/usr/share/man' \
- -configdir '/etc/xdg/coq/' \
- -coqide opt \
- -with-doc yes
-
- make world
-}
-
-package_coq() {
- depends=('ocaml' 'camlp5')
- optdepends=('coqide: graphical Coq IDE'
- 'coq-doc: offline documentation')
- # coq-nox was the old name for coq without coqide
- replaces=('coq-nox')
- conflicts=('coq-nox')
-
- cd "$srcdir/coq-$pkgver"
-
- # The second target is needed to install coqidetop.cmxs (needed for some
- # frontend other than coqide, for instance coquille)
- make COQINSTALLPREFIX="$pkgdir" install-coq install-ide-toploop
- rm -f "${pkgdir}/usr/share/man/man1/coqide.1"
-}
-
-package_coqide() {
- pkgdesc="GTK-based graphical interface for the Coq proof assistant"
- depends=('coq' 'ocaml' 'camlp5' 'gtk2' 'gtksourceview2')
-
- cd "$srcdir/coq-$pkgver"
-
- make COQINSTALLPREFIX="$pkgdir" install-coqide
- install -D -m 644 -t "${pkgdir}/usr/share/man/man1/" man/coqide.1
-
- # Remove toploop files installed by "install-ide-toploop" in the main package
- rm -f "${pkgdir}/usr/lib/coq/toploop"/coqidetop.{cma,cmxs}
- # In coq 8.7 this file is installed both by install-coq and install-coqide, remove the duplicate.
- rm -f "${pkgdir}/usr/lib/coq/vernac/topfmt.cmi"
-
- # Desktop file generated by gendesk
- install -D -m 644 "${srcdir}/${pkgname}.desktop" "${pkgdir}/usr/share/applications/${pkgname}.desktop"
- install -D -m 644 ide/coq.png "${pkgdir}/usr/share/pixmaps/${pkgname}.png"
-}
-
-package_coq-doc() {
- pkgdesc="HTML and PDF documentation for the Coq proof assistant"
- depends=()
-
- cd "$srcdir/coq-$pkgver"
-
- make COQINSTALLPREFIX="$pkgdir" install-doc
-}
Copied: coq/repos/community-x86_64/PKGBUILD (from rev 294970, coq/trunk/PKGBUILD)
===================================================================
--- PKGBUILD (rev 0)
+++ PKGBUILD 2018-02-16 09:01:56 UTC (rev 294971)
@@ -0,0 +1,89 @@
+# Maintainer: Baptiste Jonglez <baptiste--aur at jonglez dot org>
+# Contributor: acieroid
+# Contributor: spider-mario <spidermario at free.fr>
+# Contributor: Thomas Dziedzic < gostrc at gmail >
+# Contributor: George Giorgidze <giorgidze at gmail.com>
+# Contributor: William J. Bowman <bluephoenix47 at gmail.com>
+
+pkgname=('coq' 'coqide' 'coq-doc')
+pkgver=8.7.2
+pkgrel=1
+pkgdesc='Formal proof management system'
+arch=('x86_64')
+url='https://coq.inria.fr/'
+license=('GPL')
+groups=('coq')
+options=('!emptydirs')
+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=('6117ef243c62805996a21952016acaaf21db6d1b539fc813c19c897e100f45cde2bee7c9fb045b269a241b79306c656969ca8051e3212ea2090f6d7c1afad5a8')
+
+prepare() {
+ gendesk -f -n --pkgname "coqide" \
+ --name "CoqIDE Proof Assistant" \
+ --pkgdesc "Graphical interface for the Coq proof assistant" \
+ --categories "Development;Science;Math;IDE;GTK"
+ cd "$srcdir/coq-$pkgver"
+}
+
+build() {
+ cd "$srcdir/coq-$pkgver"
+
+ ./configure \
+ -prefix '/usr' \
+ -mandir '/usr/share/man' \
+ -configdir '/etc/xdg/coq/' \
+ -coqide opt \
+ -with-doc yes
+
+ make world
+}
+
+package_coq() {
+ depends=('ocaml' 'camlp5')
+ optdepends=('coqide: graphical Coq IDE'
+ 'coq-doc: offline documentation')
+ # coq-nox was the old name for coq without coqide
+ replaces=('coq-nox')
+ conflicts=('coq-nox')
+
+ cd "$srcdir/coq-$pkgver"
+
+ # The second target is needed to install coqidetop.cmxs (needed for some
+ # frontend other than coqide, for instance coquille)
+ make COQINSTALLPREFIX="$pkgdir" install-coq install-ide-toploop
+ rm -f "${pkgdir}/usr/share/man/man1/coqide.1"
+}
+
+package_coqide() {
+ pkgdesc="GTK-based graphical interface for the Coq proof assistant"
+ depends=('coq' 'ocaml' 'camlp5' 'gtk2' 'gtksourceview2')
+
+ cd "$srcdir/coq-$pkgver"
+
+ make COQINSTALLPREFIX="$pkgdir" install-coqide
+ install -D -m 644 -t "${pkgdir}/usr/share/man/man1/" man/coqide.1
+
+ # Remove toploop files installed by "install-ide-toploop" in the main package
+ rm -f "${pkgdir}/usr/lib/coq/toploop"/coqidetop.{cma,cmxs}
+ # In coq 8.7 this file is installed both by install-coq and install-coqide, remove the duplicate.
+ rm -f "${pkgdir}/usr/lib/coq/vernac/topfmt.cmi"
+
+ # Desktop file generated by gendesk
+ install -D -m 644 "${srcdir}/${pkgname}.desktop" "${pkgdir}/usr/share/applications/${pkgname}.desktop"
+ install -D -m 644 ide/coq.png "${pkgdir}/usr/share/pixmaps/${pkgname}.png"
+}
+
+package_coq-doc() {
+ pkgdesc="HTML and PDF documentation for the Coq proof assistant"
+ depends=()
+
+ cd "$srcdir/coq-$pkgver"
+
+ make COQINSTALLPREFIX="$pkgdir" install-doc
+}
Deleted: fix-num-build.patch
===================================================================
--- fix-num-build.patch 2018-02-16 09:01:42 UTC (rev 294970)
+++ fix-num-build.patch 2018-02-16 09:01:56 UTC (rev 294971)
@@ -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
More information about the arch-commits
mailing list