Date: Wednesday, February 22, 2017 @ 19:37:35
Author: demize
Revision: 213547
archrelease: copy trunk to community-i686, community-x86_64
Added:
coq/repos/community-i686/0001-Fix-incorrect-documentation-that-prevents-successful.patch
(from rev 213546,
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 213546,
coq/trunk/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch)
coq/repos/community-i686/PKGBUILD
(from rev 213546, coq/trunk/PKGBUILD)
coq/repos/community-x86_64/0001-Fix-incorrect-documentation-that-prevents-successful.patch
(from rev 213546,
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 213546,
coq/trunk/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch)
coq/repos/community-x86_64/PKGBUILD
(from rev 213546, coq/trunk/PKGBUILD)
Deleted:
coq/repos/community-i686/0001-Fix-incorrect-documentation-that-prevents-successful.patch
coq/repos/community-i686/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch
coq/repos/community-i686/PKGBUILD
coq/repos/community-x86_64/0001-Fix-incorrect-documentation-that-prevents-successful.patch
coq/repos/community-x86_64/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch
coq/repos/community-x86_64/PKGBUILD
----------------------------------------------------------------------------------+
/0001-Fix-incorrect-documentation-that-prevents-successful.patch
| 52 ++
/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch
| 92 ++++
/PKGBUILD
| 190 ++++++++++
community-i686/0001-Fix-incorrect-documentation-that-prevents-successful.patch
| 26 -
community-i686/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch
| 46 --
community-i686/PKGBUILD
| 96 -----
community-x86_64/0001-Fix-incorrect-documentation-that-prevents-successful.patch
| 26 -
community-x86_64/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch
| 46 --
community-x86_64/PKGBUILD
| 96 -----
9 files changed, 334 insertions(+), 336 deletions(-)
Deleted:
community-i686/0001-Fix-incorrect-documentation-that-prevents-successful.patch
===================================================================
---
community-i686/0001-Fix-incorrect-documentation-that-prevents-successful.patch
2017-02-22 19:37:22 UTC (rev 213546)
+++
community-i686/0001-Fix-incorrect-documentation-that-prevents-successful.patch
2017-02-22 19:37:35 UTC (rev 213547)
@@ -1,26 +0,0 @@
-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
-
Copied:
coq/repos/community-i686/0001-Fix-incorrect-documentation-that-prevents-successful.patch
(from rev 213546,
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 19:37:35 UTC (rev 213547)
@@ -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
+
Deleted:
community-i686/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch
===================================================================
---
community-i686/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch
2017-02-22 19:37:22 UTC (rev 213546)
+++
community-i686/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch
2017-02-22 19:37:35 UTC (rev 213547)
@@ -1,46 +0,0 @@
-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
-
Copied:
coq/repos/community-i686/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch
(from rev 213546,
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 19:37:35 UTC (rev 213547)
@@ -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
+
Deleted: community-i686/PKGBUILD
===================================================================
--- community-i686/PKGBUILD 2017-02-22 19:37:22 UTC (rev 213546)
+++ community-i686/PKGBUILD 2017-02-22 19:37:35 UTC (rev 213547)
@@ -1,96 +0,0 @@
-# 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
-}
Copied: coq/repos/community-i686/PKGBUILD (from rev 213546, coq/trunk/PKGBUILD)
===================================================================
--- community-i686/PKGBUILD (rev 0)
+++ community-i686/PKGBUILD 2017-02-22 19:37:35 UTC (rev 213547)
@@ -0,0 +1,95 @@
+# 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=()
+
+ cd "$srcdir/coq-$pkgver"
+
+ make COQINSTALLPREFIX="$pkgdir" install-doc
+}
Deleted:
community-x86_64/0001-Fix-incorrect-documentation-that-prevents-successful.patch
===================================================================
---
community-x86_64/0001-Fix-incorrect-documentation-that-prevents-successful.patch
2017-02-22 19:37:22 UTC (rev 213546)
+++
community-x86_64/0001-Fix-incorrect-documentation-that-prevents-successful.patch
2017-02-22 19:37:35 UTC (rev 213547)
@@ -1,26 +0,0 @@
-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
-
Copied:
coq/repos/community-x86_64/0001-Fix-incorrect-documentation-that-prevents-successful.patch
(from rev 213546,
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 19:37:35 UTC (rev 213547)
@@ -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
+
Deleted:
community-x86_64/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch
===================================================================
---
community-x86_64/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch
2017-02-22 19:37:22 UTC (rev 213546)
+++
community-x86_64/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch
2017-02-22 19:37:35 UTC (rev 213547)
@@ -1,46 +0,0 @@
-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
-
Copied:
coq/repos/community-x86_64/0002-Avoid-concurrent-runs-when-producing-html-documentat.patch
(from rev 213546,
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 19:37:35 UTC (rev 213547)
@@ -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
+
Deleted: community-x86_64/PKGBUILD
===================================================================
--- community-x86_64/PKGBUILD 2017-02-22 19:37:22 UTC (rev 213546)
+++ community-x86_64/PKGBUILD 2017-02-22 19:37:35 UTC (rev 213547)
@@ -1,96 +0,0 @@
-# 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
-}
Copied: coq/repos/community-x86_64/PKGBUILD (from rev 213546,
coq/trunk/PKGBUILD)
===================================================================
--- community-x86_64/PKGBUILD (rev 0)
+++ community-x86_64/PKGBUILD 2017-02-22 19:37:35 UTC (rev 213547)
@@ -0,0 +1,95 @@
+# 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=()
+
+ cd "$srcdir/coq-$pkgver"
+
+ make COQINSTALLPREFIX="$pkgdir" install-doc
+}
