[coq] Rebuild with fixed hevea package to get good HTML docs. Hevea is now available on all architectures

Jerry James jjames at fedoraproject.org
Thu Jan 23 20:55:36 UTC 2014 

commit 13c9cabcee844e83db0fdf48e09cd15a2abce3ec
Author: Jerry James <jamesjer at betterlinux.com>
Date:   Thu Jan 23 13:55:10 2014 -0700

    Rebuild with fixed hevea package to get good HTML docs.
    Hevea is now available on all architectures that support ocaml.
    Drop Fedora 18 compatibility now that F-18 has reached EOL.
    Add AppData file.

 coq.spec           |   65 ++++++++++++++++-----------------------------------
 coqide.appdata.xml |   28 ++++++++++++++++++++++
 2 files changed, 49 insertions(+), 44 deletions(-)
---
diff --git a/coq.spec b/coq.spec
index 8f8d25f..71ab232 100644
--- a/coq.spec
+++ b/coq.spec
@@ -1,12 +1,7 @@
 %global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
 %global tex_dir %{_datadir}/texmf/tex/latex
-
-# 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
+%if !%{opt}
+%global debug_package %{nil}
 %endif
 
 # Upstream includes option for generation of optimized binaries,
@@ -23,7 +18,7 @@
 
 Name:           coq
 Version:        8.4pl3
-Release:        1%{?dist}
+Release:        2%{?dist}
 Summary:        Proof management system
 
 Group:          Applications/Engineering
@@ -33,6 +28,7 @@ Source0:        http://coq.inria.fr/V%{version}/files/%{name}-%{version}.tar.gz
 Source1:        coqide.desktop
 Source2:        README.coq-emacs
 Source4:        coq.xml
+Source5:        coqide.appdata.xml
 
 BuildRequires:  ocaml
 BuildRequires:  ocaml-camlp5-devel
@@ -43,9 +39,7 @@ BuildRequires:  emacs-nox
 BuildRequires:  emacs-proofgeneral
 
 # For documentation
-%if %{build_html}
 BuildRequires:  hevea
-%endif
 BuildRequires:  tex(latex)
 BuildRequires:  tex(comment.sty)
 BuildRequires:  tex(epic.sty)
@@ -69,12 +63,6 @@ Requires(postun): tex(tex)
 
 ExclusiveArch: %{ocaml_arches}
 
-# Remove these once Fedora 18 goes EOL
-Obsoletes:      %{name}-xemacs < 8.3pl4
-Provides:       %{name}-xemacs = %{version}-%{release}
-Obsoletes:      %{name}-xemacs-el < 8.3pl4
-Provides:       %{name}-xemacs-el = %{version}-%{release}
-
 %description
 Coq is a formal proof management system. It allows for the development
 of theorems through first order logic that are mechanically checked by
@@ -158,8 +146,10 @@ cp -p %SOURCE1 %SOURCE2 .
 # Fix a Makefile rule that causes installation to fail
 sed -ri '/FULLCONFIGDIR/s/OLDROOT|COQINSTALLPREFIX/&2/g' Makefile.build
 
-# Use full relro due to network use
-sed -i 's/-lunix/& -ccopt -Wl,-z,relro,-z,now/' configure
+# Use full relro due to network use.  Also fix broken CAML_LD_LIBRARY_PATH.
+sed -e 's/-lunix/& -ccopt -Wl,-z,relro,-z,now/' \
+    -e "s,'\$COQTOP'/kernel,\$COQTOP/kernel," \
+    -i configure
 
 %build
 # Define opt flag based upon prior opt detection and restrictions
@@ -185,13 +175,8 @@ sed -i 's/-lunix/& -ccopt -Wl,-z,relro,-z,now/' configure
             -browser "xdg-open %s" \
             -camlp5dir %{_libdir}/ocaml/camlp5
 
-export CAML_LD_LIBRARY_PATH=`pwd`/kernel/byterun:${CAML_LD_LIBRARY_PATH}
-%if %{build_html}
+export CAML_LD_LIBRARY_PATH=$PWD/kernel/byterun:${CAML_LD_LIBRARY_PATH}
 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
 
 %install
 make COQINSTALLPREFIX="%{buildroot}%{_prefix}" OLDROOT="%{_prefix}" \
@@ -207,12 +192,11 @@ mkdir -p %{buildroot}%{coqdatadir}
 
 sed -i -e 's|ICON-LOCATION-BASE|%{_datadir}/coq/coq.png|' coqide.desktop
 
-desktop-file-install \
-%if 0%{?fedora} && 0%{?fedora} < 19
---vendor="fedora"                  \
-%endif
---dir=%{buildroot}%{_datadir}/applications              \
-coqide.desktop
+desktop-file-install --dir=%{buildroot}%{_datadir}/applications coqide.desktop
+
+# Install AppData file
+mkdir -p %{buildroot}%{_datadir}/appdata
+install -pm 644 %{SOURCE5} %{buildroot}%{_datadir}/appdata
 
 # Make a MIME type for .v files
 mkdir -p %{buildroot}%{_datadir}/mime/packages
@@ -231,16 +215,6 @@ 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 README;
 do cp -p $f %{buildroot}%{coqdocdir};
@@ -307,11 +281,8 @@ mktexlsr &> /dev/null
 %{coqdatadir}/ide
 %exclude %{coqdatadir}/ide/ide.cmxa
 %exclude %{coqdatadir}/ide/ide.a
-%if 0%{?fedora} && 0%{?fedora} < 19
-%{_datadir}/applications/fedora-coqide.desktop
-%else
+%{_datadir}/appdata/coqide.appdata.xml
 %{_datadir}/applications/coqide.desktop
-%endif
 %{_datadir}/mime/packages/coq.xml
 
 %files doc
@@ -332,6 +303,12 @@ mktexlsr &> /dev/null
 %{_emacs_sitelispdir}/coq/*.el
 
 %changelog
+* Thu Jan 23 2014 Jerry James <loganjerry at gmail.com> - 8.4pl3-2
+- Rebuild with fixed hevea package to get good HTML docs
+- Hevea is now available on all architectures that support ocaml
+- Drop Fedora 18 compatibility now that F-18 has reached EOL
+- Add AppData file
+
 * Mon Dec 16 2013 Jerry James <loganjerry at gmail.com> - 8.4pl3-1
 - New upstream release
 
diff --git a/coqide.appdata.xml b/coqide.appdata.xml
new file mode 100644
index 0000000..759e994
--- /dev/null
+++ b/coqide.appdata.xml
@@ -0,0 +1,28 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<application>
+ <id type="desktop">coqide.desktop</id>
+ <licence>CC0</licence>
+ <summary>Coq IDE</summary>
+ <description>
+  <p>
+   Coq is a formal proof management system. It allows for the development of
+   theorems through first order logic that are mechanically checked by the
+   machine.  Sets of definitions and theorems can be saved as compiled modules
+   and loaded into the system.
+  </p>
+  <p>
+   This package provides Coqide, a lightweight IDE for Coq.
+  </p>
+ </description>
+ <screenshots>
+  <screenshot type="default">http://coq.inria.fr/coq/files/coqide/images/capture1.jpg</screenshot>
+  <screenshot>http://coq.inria.fr/coq/files/coqide/images/capture2.jpg</screenshot>
+  <screenshot>http://coq.inria.fr/coq/files/coqide/images/capture3.jpg</screenshot>
+  <screenshot>http://coq.inria.fr/coq/files/coqide/images/capture4.jpg</screenshot>
+  <screenshot>http://coq.inria.fr/coq/files/coqide/images/capture5.jpg</screenshot>
+ </screenshots>
+ <url type="homepage">http://coq.inria.fr/</url>
+ <!-- FIXME: change this to an upstream email address for spec updates
+   <updatecontact>someone_who_cares at upstream_project.org</updatecontact>
+  -->
+</application>

More information about the scm-commits mailing list