[coq] Rebuild for new ocaml-camlp5; patch for bz 691913 no longer needed. Drop tar_base_name, no longer ne
Jerry James
jjames at fedoraproject.org
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.
More information about the scm-commits
mailing list