[arch-commits] Commit in coq/repos (4 files)
Date: Wednesday, October 18, 2017 @ 10:04:48 Author: zorun Revision: 263228 archrelease: copy trunk to community-i686, community-x86_64 Added: coq/repos/community-i686/PKGBUILD (from rev 263227, coq/trunk/PKGBUILD) coq/repos/community-x86_64/PKGBUILD (from rev 263227, coq/trunk/PKGBUILD) Deleted: coq/repos/community-i686/PKGBUILD coq/repos/community-x86_64/PKGBUILD ---+ /PKGBUILD | 176 community-i686/PKGBUILD | 87 - community-x86_64/PKGBUILD | 87 - 3 files changed, 176 insertions(+), 174 deletions(-) Deleted: community-i686/PKGBUILD === --- community-i686/PKGBUILD 2017-10-18 10:04:23 UTC (rev 263227) +++ community-i686/PKGBUILD 2017-10-18 10:04:48 UTC (rev 263228) @@ -1,87 +0,0 @@ -# Maintainer: Baptiste Jonglez -# Contributor: acieroid -# Contributor: spider-mario -# Contributor: Thomas Dziedzic < gostrc at gmail > -# Contributor: George Giorgidze -# Contributor: William J. Bowman - -pkgname=('coq' 'coqide' 'coq-doc') -pkgver=8.6.1 -pkgrel=1 -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";) -sha1sums=('5dbaf1230c297d7c11c8715c012300a51ad80f9a') - -prepare() { - gendesk -f -n --pkgname "coqide" \ ---name "CoqIDE Proof Assistant" \ ---pkgdesc "Graphical interface for the Coq proof assistant" \ ---categories "Development;Science;Math;IDE;GTK" -} - -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=() - - cd "$srcdir/coq-$pkgver" - - make COQINSTALLPREFIX="$pkgdir" install-doc -} Copied: coq/repos/community-i686/PKGBUILD (from rev 263227, coq/trunk/PKGBUILD) === --- community-i686/PKGBUILD (rev 0) +++ community-i686/PKGBUILD 2017-10-18 10:04:48 UTC (rev 263228) @@ -0,0 +1,88 @@ +# Maintainer: Baptiste Jonglez +# Contributor: acieroid +# Contributor: spider-mario +# Contributor: Thomas Dziedzic < gostrc at gmail > +# Contributor: George Giorgidze +# Contributor: William J. Bowman + +pkgname=('coq' 'coqide' 'coq-doc') +pkgver=8.7.0 +pkgrel=1 +pkgdesc='Formal proof management system' +arch=('i686' 'x86_64') +url='https://coq.inria.fr/' +license=('GPL') +groups=('coq') +options=('!emptydirs') +depends=('ocaml' 'camlp5' '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://github.com/coq/coq/archive/V${pkgver}.tar.gz";) +sha512sums=('c806881d1ab823d9c2d748aa2d7fd3faaa0f6395536942ad214c68658b2688e6c57941947a440ddb69bf1436249067eefd866ecb1d9e4c5e774e3218c80a6fc2') + +prepare() { + gendesk -f -n --pkgname "coqide" \ +--name "CoqIDE Proof Assistant" \ +--pkgdesc "Graphical inter
[arch-commits] Commit in coq/repos (4 files)
Date: Wednesday, February 22, 2017 @ 18:28:13 Author: demize Revision: 213541 archrelease: copy trunk to community-x86_64 Added: coq/repos/community-x86_64/ coq/repos/community-x86_64/0001-Fix-incorrect-documentation-that-prevents-successful.patch (from rev 213540, coq/trunk/0001-Fix-incorrect-documentation-that-prevents-successful.patch) coq/repos/community-x86_64/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch (from rev 213540, coq/trunk/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch) coq/repos/community-x86_64/PKGBUILD (from rev 213540, 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(+) Copied: coq/repos/community-x86_64/0001-Fix-incorrect-documentation-that-prevents-successful.patch (from rev 213540, coq/trunk/0001-Fix-incorrect-documentation-that-prevents-successful.patch) === --- community-x86_64/0001-Fix-incorrect-documentation-that-prevents-successful.patch (rev 0) +++ community-x86_64/0001-Fix-incorrect-documentation-that-prevents-successful.patch 2017-02-22 18:28:13 UTC (rev 213541) @@ -0,0 +1,26 @@ +From 42f27beb63a629dcef514abb0b31dea193f35a38 Mon Sep 17 00:00:00 2001 +From: Guillaume Melquiond +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 + Copied: coq/repos/community-x86_64/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch (from rev 213540, coq/trunk/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch) === --- community-x86_64/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch (rev 0) +++ community-x86_64/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch 2017-02-22 18:28:13 UTC (rev 213541) @@ -0,0 +1,46 @@ +From c793d102df3e007d824e79f499e71823207c301a Mon Sep 17 00:00:00 2001 +From: Guillaume Melquiond +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 + Copied: coq/repos/community-x86_64/PKGBUILD (from rev 213540, coq/trunk/PKGBUILD) =
[arch-commits] Commit in coq/repos (4 files)
Date: Wednesday, February 22, 2017 @ 18:28:05 Author: demize Revision: 213540 archrelease: copy trunk to community-i686 Added: coq/repos/community-i686/ coq/repos/community-i686/0001-Fix-incorrect-documentation-that-prevents-successful.patch (from rev 213539, coq/trunk/0001-Fix-incorrect-documentation-that-prevents-successful.patch) coq/repos/community-i686/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch (from rev 213539, coq/trunk/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch) coq/repos/community-i686/PKGBUILD (from rev 213539, 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(+) Copied: coq/repos/community-i686/0001-Fix-incorrect-documentation-that-prevents-successful.patch (from rev 213539, coq/trunk/0001-Fix-incorrect-documentation-that-prevents-successful.patch) === --- community-i686/0001-Fix-incorrect-documentation-that-prevents-successful.patch (rev 0) +++ community-i686/0001-Fix-incorrect-documentation-that-prevents-successful.patch 2017-02-22 18:28:05 UTC (rev 213540) @@ -0,0 +1,26 @@ +From 42f27beb63a629dcef514abb0b31dea193f35a38 Mon Sep 17 00:00:00 2001 +From: Guillaume Melquiond +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 + Copied: coq/repos/community-i686/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch (from rev 213539, coq/trunk/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch) === --- community-i686/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch (rev 0) +++ community-i686/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch 2017-02-22 18:28:05 UTC (rev 213540) @@ -0,0 +1,46 @@ +From c793d102df3e007d824e79f499e71823207c301a Mon Sep 17 00:00:00 2001 +From: Guillaume Melquiond +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 + Copied: coq/repos/community-i686/PKGBUILD (from rev 213539, coq/trunk/PKGBUILD) ==