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

[Baptiste Jonglez]

    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 <guillaume.melquiond at 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
-

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 <guillaume.melquiond at 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
-

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 <bluephoenix47 at gmail.com>
 
 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() {