Date: Wednesday, February 22, 2017 @ 16:15:29 Author: zorun Revision: 213537
coq: import from AUR Added: coq/ coq/repos/ coq/trunk/ coq/trunk/0001-Fix-incorrect-documentation-that-prevents-successful.patch coq/trunk/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch coq/trunk/PKGBUILD -----------------------------------------------------------------+ 0001-Fix-incorrect-documentation-that-prevents-successful.patch | 26 ++ 0002-Avoid-concurrent-runs-when-producing-html-documentat.patch | 46 ++++ PKGBUILD | 96 ++++++++++ 3 files changed, 168 insertions(+) Added: coq/trunk/0001-Fix-incorrect-documentation-that-prevents-successful.patch =================================================================== --- coq/trunk/0001-Fix-incorrect-documentation-that-prevents-successful.patch (rev 0) +++ coq/trunk/0001-Fix-incorrect-documentation-that-prevents-successful.patch 2017-02-22 16:15:29 UTC (rev 213537) @@ -0,0 +1,26 @@ +From 42f27beb63a629dcef514abb0b31dea193f35a38 Mon Sep 17 00:00:00 2001 +From: Guillaume Melquiond <guillaume.melqui...@inria.fr> +Date: Fri, 16 Dec 2016 11:27:42 +0100 +Subject: [PATCH] Fix incorrect documentation that prevents successful + compilation (bug #5265). + +--- + doc/refman/RefMan-syn.tex | 2 +- + 1 file changed, 1 insertion(+), 1 deletion(-) + +diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex +index 1fcc1c0..21c39de 100644 +--- a/doc/refman/RefMan-syn.tex ++++ b/doc/refman/RefMan-syn.tex +@@ -649,7 +649,7 @@ A recursive pattern for binders can be used in position of a recursive + pattern for terms. Here is an example: + + \begin{coq_example*} +-Notation ``'FUNAPP' x .. y , f'' := ++Notation "'FUNAPP' x .. y , f" := + (fun x => .. (fun y => (.. (f x) ..) y ) ..) + (at level 200, x binder, y binder, right associativity). + \end{coq_example*} +-- +2.10.2 + Added: coq/trunk/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch =================================================================== --- coq/trunk/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch (rev 0) +++ coq/trunk/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch 2017-02-22 16:15:29 UTC (rev 213537) @@ -0,0 +1,46 @@ +From c793d102df3e007d824e79f499e71823207c301a Mon Sep 17 00:00:00 2001 +From: Guillaume Melquiond <guillaume.melqui...@inria.fr> +Date: Mon, 19 Dec 2016 11:58:39 +0100 +Subject: [PATCH 1/4] Avoid concurrent runs when producing html documentation + (bug #5269). + +Make does not allow for rules that produce multiple outputs (unless they +are pattern rules). As a consequence, the hacha rule could be run several +times concurrently, thus causing doc/refman/html to be deleted under the +feet of some runs. + +This commit fixes the issue by turning the rule into a single-output rule +and adding a dummy rule to handle all the other indexes. Note that this is +not a perfect solution since, if the user were to manually delete one of +the auxiliary index, it would not be rebuilt until the main index is. +--- + Makefile.doc | 6 ++++-- + 1 file changed, 4 insertions(+), 2 deletions(-) + +diff --git a/Makefile.doc b/Makefile.doc +index cdd9852e8..9ae20ba76 100644 +--- a/Makefile.doc ++++ b/Makefile.doc +@@ -201,15 +201,17 @@ doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva + $(INSTALLLIB) $< doc/refman + + INDEXES:= doc/refman/html/command-index.html doc/refman/html/tactic-index.html +-ALLINDEXES:= doc/refman/html/index.html $(INDEXES) + +-refman-html-dir $(ALLINDEXES): doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ ++refman-html-dir $(INDEXES): doc/refman/html/index.html ; ++ ++doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ + doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html + - rm -rf doc/refman/html + $(MKDIR) doc/refman/html + $(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html + (cd doc/refman/html; $(HACHA) -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html) + $(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html ++ @touch $(INDEXES) + -$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html + + refman-quick: +-- +2.11.0 + Added: coq/trunk/PKGBUILD =================================================================== --- coq/trunk/PKGBUILD (rev 0) +++ coq/trunk/PKGBUILD 2017-02-22 16:15:29 UTC (rev 213537) @@ -0,0 +1,96 @@ +# Maintainer: Baptiste Jonglez <baptiste--aur at jonglez dot org> +# Contributor: acieroid +# Contributor: spider-mario <spiderma...@free.fr> +# Contributor: Thomas Dziedzic < gostrc at gmail > +# Contributor: George Giorgidze <giorgi...@gmail.com> +# Contributor: William J. Bowman <bluephoeni...@gmail.com> + +pkgname=('coq' 'coqide' 'coq-doc') +pkgver=8.6 +pkgrel=5 +pkgdesc='Formal proof management system' +arch=('i686' 'x86_64') +url='https://coq.inria.fr/' +license=('GPL') +groups=('coq') +options=('!emptydirs') +depends=('ocaml' 'camlp4' '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=("https://coq.inria.fr/distrib/V$pkgver/files/coq-$pkgver.tar.gz" + "0001-Fix-incorrect-documentation-that-prevents-successful.patch" + "0002-Avoid-concurrent-runs-when-producing-html-documentat.patch") +sha1sums=('617a6f86d09dde0e409f3fa22268daf7be3f5bba' + 'ec5e9af33f37d2eb154f8de13815cb7f1f2fba6e' + '201f1db7fd3e7e072ff7c94cfcdabdcc5910ccdd') + +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" + patch -p1 < ../0001-Fix-incorrect-documentation-that-prevents-successful.patch + patch -p1 < ../0002-Avoid-concurrent-runs-when-producing-html-documentat.patch +} + +build() { + cd "$srcdir/coq-$pkgver" + + ./configure \ + -prefix '/usr' \ + -mandir '/usr/share/man' \ + -configdir '/etc/xdg/coq/' \ + -coqide opt \ + -with-doc yes \ + -usecamlp4 + + make world +} + +package_coq() { + depends=('ocaml' 'camlp4') + 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' 'camlp4' '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} + + # 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=() + arch=('any') + + cd "$srcdir/coq-$pkgver" + + make COQINSTALLPREFIX="$pkgdir" install-doc +}