Date: Wednesday, July 26, 2017 @ 07:24:34 Author: zorun Revision: 246398
upgpkg: coq 8.6.1-1 Modified: coq/trunk/PKGBUILD Deleted: coq/trunk/0001-Fix-incorrect-documentation-that-prevents-successful.patch coq/trunk/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch -----------------------------------------------------------------+ 0001-Fix-incorrect-documentation-that-prevents-successful.patch | 26 ----- 0002-Avoid-concurrent-runs-when-producing-html-documentat.patch | 46 ---------- PKGBUILD | 16 --- 3 files changed, 4 insertions(+), 84 deletions(-) Deleted: 0001-Fix-incorrect-documentation-that-prevents-successful.patch =================================================================== --- 0001-Fix-incorrect-documentation-that-prevents-successful.patch 2017-07-26 07:18:59 UTC (rev 246397) +++ 0001-Fix-incorrect-documentation-that-prevents-successful.patch 2017-07-26 07:24:34 UTC (rev 246398) @@ -1,26 +0,0 @@ -From 42f27beb63a629dcef514abb0b31dea193f35a38 Mon Sep 17 00:00:00 2001 -From: Guillaume Melquiond <[email protected]> -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 - Deleted: 0002-Avoid-concurrent-runs-when-producing-html-documentat.patch =================================================================== --- 0002-Avoid-concurrent-runs-when-producing-html-documentat.patch 2017-07-26 07:18:59 UTC (rev 246397) +++ 0002-Avoid-concurrent-runs-when-producing-html-documentat.patch 2017-07-26 07:24:34 UTC (rev 246398) @@ -1,46 +0,0 @@ -From c793d102df3e007d824e79f499e71823207c301a Mon Sep 17 00:00:00 2001 -From: Guillaume Melquiond <[email protected]> -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 - Modified: PKGBUILD =================================================================== --- PKGBUILD 2017-07-26 07:18:59 UTC (rev 246397) +++ PKGBUILD 2017-07-26 07:24:34 UTC (rev 246398) @@ -6,8 +6,8 @@ # Contributor: William J. Bowman <[email protected]> pkgname=('coq' 'coqide' 'coq-doc') -pkgver=8.6 -pkgrel=8 +pkgver=8.6.1 +pkgrel=1 pkgdesc='Formal proof management system' arch=('i686' 'x86_64') url='https://coq.inria.fr/' @@ -20,12 +20,8 @@ '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') +source=("https://coq.inria.fr/distrib/V$pkgver/files/coq-$pkgver.tar.gz";) +sha1sums=('5dbaf1230c297d7c11c8715c012300a51ad80f9a') prepare() { gendesk -f -n --pkgname "coqide" \ @@ -32,10 +28,6 @@ --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() {
