[coq] Rebuild for new ocaml-camlp5; patch for bz 691913 no longer needed. Drop tar_base_name, no longer ne

Thu Oct 27 20:32:16 UTC 2011

commit b486518e2afda06b515afa3d2036b9fc0b639841
Author: Jerry James <loganjerry at gmail.com>
Date:   Thu Oct 27 14:31:45 2011 -0600

    Rebuild for new ocaml-camlp5; patch for bz 691913 no longer needed.
    Drop tar_base_name, no longer necessary.
    Drop versioned dependencies for packages that meet the dep in F14.
    Build without HTML documentation on arches lacking hevea.
    Change ExclusiveArch to %{ocaml_arches}.
    Fix a broken conditional and a typo.

 coq.spec |   70 +++++++++++++++++++++++++++++++++++++++++--------------------
 1 files changed, 47 insertions(+), 23 deletions(-)
---

diff --git a/coq.spec b/coq.spec
index b6c910c..beb66d4 100644
--- a/coq.spec
+++ b/coq.spec
@@ -1,8 +1,15 @@
 %global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
 %global debug_package %{nil}
-%global tar_base_name coq-%{version}
 %global tex_dir %{_texmf_vendor}/tex/latex/misc
 
+# Hevea is not universally available, so HTML documentation cannot be produced
+# on some arches.
+%ifarch ppc64
+%global build_html 0
+%else
+%global build_html 1
+%endif
+
 # Upstream includes option for generation of optimized binaries,
 # however, specifically generates bytecode versions for certain
 # executables even when optimized option is set, namely the following:
@@ -17,32 +24,30 @@
 
 Name:           coq
 Version:        8.3pl2
-Release:        2%{?dist}
+Release:        3%{?dist}
 Summary:        Proof management system
 
 Group:          Applications/Engineering
 License:        LGPLv2
 URL:            http://coq.inria.fr/
-Source0:        http://coq.inria.fr/V%{version}/files/%{tar_base_name}.tar.gz
+Source0:        http://coq.inria.fr/V%{version}/files/%{name}-%{version}.tar.gz
 Source1:        coqide.desktop
 Source2:        README.coq-emacs
 Source3:        README.coq-xemacs
 Source4:        coq.xml
-# This patch was suggested by upstream to workaround a camlp5 bug (691913).
-# Remove this once ocaml-camlp5 > 6.02.2 is available.
-Patch0:         coq-camlp5-bug.patch
 
-BuildRequires:  ocaml >= 3.10.0, ocaml-camlp5-devel, ocaml-lablgtk-devel
+BuildRequires:  ocaml, ocaml-camlp5-devel, ocaml-lablgtk-devel
 BuildRequires:  desktop-file-utils, emacs-nox, xemacs-nox
 BuildRequires:  emacs-proofgeneral, xemacs-proofgeneral
 # For documentation
-BuildRequires:  tex(latex), hevea
+BuildRequires:  tex(latex)
+%if %{build_html}
+BuildRequires:  hevea
+%endif
 Requires(posttrans): tex(tex)
 Requires(postun): tex(tex)
 
-# This should always match the list in the ocaml spec file.
-# TODO: ppc64 is NOT currently on this list, due to a missing hevea package.
-ExclusiveArch: alpha armv4l %{ix86} ia64 x86_64 ppc sparc sparcv9
+ExclusiveArch: %{ocaml_arches}
 
 %description
 Coq is a formal proof management system. It allows for the development
@@ -133,8 +138,7 @@ This package contains the Elisp source files for Coq's XEmacs support.
 This package is not needed to use the XEmacs interface.
 
 %prep
-%setup -q -n %{tar_base_name}
-%patch0
+%setup -q
 
 # Fix some files that are not in UTF-8 encoding
 
@@ -168,7 +172,12 @@ cp -p %SOURCE1 %SOURCE2 %SOURCE3 .
             -camlp5dir %{_libdir}/ocaml/camlp5
 
 export CAML_LD_LIBRARY_PATH=`pwd`/kernel/byterun:${CAML_LD_LIBRARY_PATH}
+%if %{build_html}
 make world VERBOSE=1
+%else
+# If documentation wasn't built due to lack of hevea, at least build the PDFs
+make world doc-pdf VERBOSE=1
+%endif
 
 # Strip shared objects (not sure where the best location for a
 # makefile patch for this would be).
@@ -203,19 +212,28 @@ mkdir -p %{buildroot}%{_datadir}/mime/packages
 cp -p %{SOURCE4} %{buildroot}%{_datadir}/mime/packages
 
 # Install main Coq .v files
-
-for f in `find plugin theories -name '*.v' -type f`; do
+for f in `find plugins theories -name '*.v' -type f`; do
 mkdir -p %{buildroot}%{coqdatadir}/`dirname $f` && cp -p $f %{buildroot}%{coqdatadir}/`dirname $f`
 done
 
 # Install tutorial code
 %global tutorialcodedir %{coqdatadir}/RecTutorial
-%if %(test -d %{buildroot}%{tutorialcodedir} && echo 1 || echo 0) != 1
-mkdir -p %{buildroot}%{tutorialcodedir}
-%endif
+if [ ! -d %{buildroot}%{tutorialcodedir} ]; then
+  mkdir -p %{buildroot}%{tutorialcodedir}
+fi
 cp -p doc/RecTutorial/RecTutorial.v %{buildroot}%{tutorialcodedir}
 ln -s %{tutorialcodedir} %{buildroot}%{coqdatadir}/RecTutorial
 
+# No documentation is installed at all if lacking hevea, so copy the PDFs
+%if ! %{build_html}
+mkdir -p %{buildroot}%{coqdocdir}/pdf
+cp -p doc/faq/FAQ.v.pdf %{buildroot}%{coqdocdir}/pdf/FAQ.pdf
+cp -p doc/RecTutorial/RecTutorial.pdf %{buildroot}%{coqdocdir}/pdf
+cp -p doc/refman/Reference-Manual.pdf %{buildroot}%{coqdocdir}/pdf
+cp -p doc/stdlib/Library.pdf %{buildroot}%{coqdocdir}/pdf
+cp -p doc/tutorial/Tutorial.v.pdf %{buildroot}%{coqdocdir}/pdf/Tutorial.pdf
+%endif
+
 # Install documentation not installed by install-doc in Makefile
 for f in CHANGES COMPATIBILITY COPYRIGHT CREDITS INSTALL LICENSE README;
 do cp -p $f %{buildroot}%{coqdocdir};
@@ -245,11 +263,9 @@ update-mime-database %{_datadir}/mime &> /dev/null || :
 update-desktop-database -q &> /dev/null || :
 
 %postun
-if [ $1 -eq 0 ]; then
-  update-desktop-database -q &> /dev/null
-  update-mime-database %{_datadir}/mime &> /dev/null || :
-  mktexlsr &> /dev/null
-fi
+update-desktop-database -q &> /dev/null
+update-mime-database %{_datadir}/mime &> /dev/null || :
+mktexlsr &> /dev/null
 
 # Note: we want to keep both coqtop.opt and coqtop.byte because the
 # byte compiled version can be used to compile new version through
@@ -328,6 +344,14 @@ fi
 %{_xemacs_sitelispdir}/coq/*.el
 
 %changelog
+* Thu Oct 27 2011 Jerry James <loganjerry at gmail.com> - 8.3pl2-3
+- Rebuild for new ocaml-camlp5; patch for bz 691913 no longer needed
+- Drop tar_base_name, no longer necessary
+- Drop versioned dependencies for packages that meet the dep in F14
+- Build without HTML documentation on arches lacking hevea
+- Change ExclusiveArch to %%{ocaml_arches}
+- Fix a broken conditional and a typo
+
 * Wed Jun 15 2011 Jerry James <loganjerry at gmail.com> - 8.3pl2-2
 - Remove workaround for bad documentation link in 8.3pl1, fixed in 8.3pl2
 - Revert change in 8.3pl1-1 to split arch-specific stuff from noarch stuff.
