rpms/coq/devel .cvsignore, 1.5, 1.6 coq.spec, 1.12, 1.13 import.log, 1.8, 1.9 sources, 1.5, 1.6 RecTutorial.v, 1.1, NONE
Alan Dunn
amdunn at fedoraproject.org
Wed Aug 5 21:33:00 UTC 2009
Author: amdunn
Update of /cvs/pkgs/rpms/coq/devel
In directory cvs1.fedora.phx.redhat.com:/tmp/cvs-serv7642/devel
Modified Files:
.cvsignore coq.spec import.log sources
Removed Files:
RecTutorial.v
Log Message:
* Wed Aug 05 2009 Alan Dunn <amdunn at gmail.com> - 8.2pl1-1
- New upstream release
- Eliminated modification of tar_base_name that occurred for only version 8.2
- Added reference to bugzilla bug for ppc64 ExcludeArch
- HTML form of documentation seems to no longer be distributed -> must generate
Decided for consistency to generate all documentation
- Additional file for iconv - documentation license file
- Changed tutorial directory name, now also using bundled version
of tutorial
Index: .cvsignore
===================================================================
RCS file: /cvs/pkgs/rpms/coq/devel/.cvsignore,v
retrieving revision 1.5
retrieving revision 1.6
diff -u -p -r1.5 -r1.6
--- .cvsignore 19 Jun 2009 11:14:51 -0000 1.5
+++ .cvsignore 5 Aug 2009 21:32:59 -0000 1.6
@@ -1,7 +1 @@
-Coq-RecTutorial.pdf.gz
-Coq-Library-8.2.pdf.gz
-Coq-Reference-Manual-8.2.pdf.gz
-Coq-Tutorial-8.2.pdf.gz
-coq-8.2-1.tar.gz
-coq-refman-html-8.2.tar.gz
-coq-stdlib-html-8.2.tar.gz
+coq-8.2pl1.tar.gz
Index: coq.spec
===================================================================
RCS file: /cvs/pkgs/rpms/coq/devel/coq.spec,v
retrieving revision 1.12
retrieving revision 1.13
diff -u -p -r1.12 -r1.13
--- coq.spec 24 Jul 2009 19:29:30 -0000 1.12
+++ coq.spec 5 Aug 2009 21:33:00 -0000 1.13
@@ -23,39 +23,32 @@
%global _enable_debug_package 0
%global debug_package %{nil}
-# The "-1" will have to be removed at the next version upgrade... this is
-# just for 8.2
-%global tar_base_name coq-%{version}-1
-
-Name: coq
-Version: 8.2
-Release: 2%{?dist}
-Summary: Coq 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
-Source1: Coq-Library-%{version}.pdf.gz
-Source2: Coq-Reference-Manual-%{version}.pdf.gz
-Source3: Coq-Tutorial-%{version}.pdf.gz
-Source4: Coq-RecTutorial.pdf.gz
-Source5: coq-refman-html-%{version}.tar.gz
-Source6: coq-stdlib-html-%{version}.tar.gz
-Source7: RecTutorial.v
-Source8: coqide.desktop
-Source10: README.coq-emacs
-Patch0: coq-makefile-strip-%{version}.patch
-Patch1: coq-check-%{version}.patch
-Patch2: coq-micromega-%{version}.patch
-BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
-BuildRequires: ocaml >= 3.08, ocaml-camlp5-devel, gtk2-devel, ocaml-lablgtk-devel, desktop-file-utils, emacs
+%global tar_base_name coq-%{version}
+
+Name: coq
+Version: 8.2pl1
+Release: 1%{?dist}
+Summary: Coq 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
+Source1: coqide.desktop
+Source2: README.coq-emacs
+Patch0: coq-makefile-strip-8.2.patch
+Patch1: coq-check-8.2.patch
+Patch2: coq-micromega-8.2.patch
+BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
+BuildRequires: ocaml >= 3.08, ocaml-camlp5-devel, gtk2-devel, ocaml-lablgtk-devel, desktop-file-utils, emacs
# Needed for execstack, NOT for preventing stripping of custom
# bytecode executables as before
BuildRequires: prelink
+# For documentation
+BuildRequires: texlive-latex, texlive-texmf, hevea
ExcludeArch: s390 s390x sparc64
-# Getting an error re: pthread_atfork - going to file a bugzilla bug
-# and number will end up here
+# ppc64 build fails in both opt and non-opt versions
+# bz: 515813
ExcludeArch: ppc64
%description
@@ -72,9 +65,9 @@ Coqide.
# also the full name of the IDE) or "coq" and "ide" will find
# this. (If the package were named "coq-ide", the former would fail.)
%package coqide
-Group: Applications/Engineering
-Summary: Coqide IDE for Coq proof management system
-Requires: coq
+Group: Applications/Engineering
+Summary: Coqide IDE for Coq proof management system
+Requires: coq
%description coqide
Coq is a formal proof management system. It allows for the development
@@ -85,9 +78,9 @@ modules and loaded into the system.
This package provides Coqide, a lightweight IDE for Coq.
%package doc
-Group: Applications/Engineering
-License: Open Publication
-Summary: Documentation for Coq proof management system
+Group: Applications/Engineering
+License: Open Publication
+Summary: Documentation for Coq proof management system
%description doc
Coq is a formal proof management system. It allows for the development
@@ -104,9 +97,9 @@ main one, and one specifically on recurs
for the latter is also included.
%package emacs
-Group: Applications/Engineering
-Summary: Elisp files for Coq proof management system
-Requires: coq, emacs
+Group: Applications/Engineering
+Summary: Elisp files for Coq proof management system
+Requires: coq, emacs
%description emacs
Coq is a formal proof management system. It allows for the development
@@ -161,19 +154,14 @@ This package provides emacs mode files f
# Fix some files that are not in UTF-8 encoding
-for f in CHANGES CREDITS COPYRIGHT; do
+for f in CHANGES CREDITS COPYRIGHT doc/LICENSE; do
mv $f $f.old; iconv -f ISO-8859-1 -t UTF-8 < $f.old > $f; rm $f.old
done
%global emacs_lispdir %{_datadir}/emacs/site-lisp
%global tex_dir %{_datadir}/texmf/tex/latex/misc
-# Seems like setup only sets up the main file
-cp %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE10 .
-gunzip *.gz
-for f in *.tar; do
-tar xf $f
-done
+cp %SOURCE1 %SOURCE2 .
%build
%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
@@ -206,14 +194,23 @@ done
# executables
%global coq_sopath %{_libdir}/ocaml/stublibs
+%global coqdocdir %{_defaultdocdir}/coq-%{version}
+
+./configure -prefix %{_prefix} \
+ -libdir %{_datadir}/coq \
+ -bindir %{_bindir} \
+ -mandir %{_mandir} \
+ -docdir %{coqdocdir} \
+ -emacs %{emacs_lispdir} \
+ -coqdocdir %{tex_dir} \
+ %{opt_option} \
+ -reals all \
+ -camlp5dir %{_libdir}/ocaml/camlp5 \
+ -coqrunbyteflags "-dllib -lcoqrun -dllpath %{coq_sopath}"
-./configure -prefix %{_prefix} -libdir %{_datadir}/coq -bindir %{_bindir} -mandir %{_mandir} -emacs %{emacs_lispdir} -coqdocdir %{tex_dir} %{opt_option} -reals all -camlp5dir %{_libdir}/ocaml/camlp5 -coqrunbyteflags "-dllib -lcoqrun -dllpath %{coq_sopath}"
export CAML_LD_LIBRARY_PATH=`pwd`/kernel/byterun:${CAML_LD_LIBRARY_PATH}
make world VERBOSE=1
-# Fix permissions in the documentation
-chmod -R a+rX refman stdlib
-
# Clear any execstack permissions that ELF binaries may have
for f in bin/*; do
file $f | grep "ELF" && execstack -c $f
@@ -237,8 +234,8 @@ mkdir -p %{buildroot}%{coqdatadir}
sed -i -e 's|ICON-LOCATION-BASE|%{coqdatadir}/ide/coq.png|' coqide.desktop
-desktop-file-install --vendor="fedora" \
---dir=%{buildroot}%{_datadir}/applications \
+desktop-file-install --vendor="fedora" \
+--dir=%{buildroot}%{_datadir}/applications \
coqide.desktop
# Install main Coq .v files
@@ -249,11 +246,16 @@ done
# Install tutorial code
-%global tutorialcodedir %{coqdatadir}/tutorial
+%global tutorialcodedir %{coqdatadir}/RecTutorial
%if %(test -d %{buildroot}%{tutorialcodedir} && echo 1 || echo 0) != 1
mkdir -p %{buildroot}%{tutorialcodedir}
%endif
-mv RecTutorial.v %{buildroot}%{tutorialcodedir}
+cp doc/RecTutorial/RecTutorial.v %{buildroot}%{tutorialcodedir}
+
+# Install documentation not installed by install-doc in Makefile
+for f in CHANGES COMPATIBILITY COPYRIGHT CREDITS INSTALL LICENSE README;
+do cp $f %{buildroot}%{coqdocdir};
+done
# Coq tries to move a .so into share - move it (easier than a makefile
# patch)
@@ -264,6 +266,9 @@ mv %{buildroot}%{coqdatadir}/dllcoqrun.s
# Micromega contrib tries to sneak an executable into share - move it
mv %{buildroot}%{coqdatadir}/contrib/micromega/csdpcert %{buildroot}%{_bindir}
+# Don't install libcoqrun.a (it might not exist, but get rid of it if it does)
+rm -f %{buildroot}%{coqdatadir}/libcoqrun.a
+
%clean
rm -rf %{buildroot}
@@ -276,18 +281,16 @@ rm -rf %{buildroot}
%files
%defattr(-,root,root,-)
-%doc CHANGES COMPATIBILITY COPYRIGHT CREDITS INSTALL LICENSE README
-%doc %{_mandir}/man1/*
+# DON'T use the doc macro here or else it wipes out all the other documentation installed!
+%{_mandir}/man1/*
%{coqdatadir}
-%if %(test -e %{buildroot}%{coqdatadir}/libcoqrun.a && echo 1 || echo 0) == 1
-%exclude %{coqdatadir}/libcoqrun.a
-%endif
%{coq_sopath}/dllcoqrun.so
%{_bindir}/coq*
%{_bindir}/gallina
%{_bindir}/csdpcert
%exclude %{_bindir}/coqide*
%exclude %{coqdatadir}/ide
+%exclude %{coqdatadir}/config/coq_config.cmo
%if %{opt}
%exclude %{coqdatadir}/*/*.cmxa
%exclude %{coqdatadir}/*/*.cmx
@@ -295,6 +298,17 @@ rm -rf %{buildroot}
%exclude %{coqdatadir}/*/*.o
%endif
%{tex_dir}/coq*
+# A few documentation files here should stay in the main package (and
+# are excluded from doc), but the bulk of the documentation is in the
+# doc subpackage
+%dir %{coqdocdir}
+%{coqdocdir}/CHANGES
+%{coqdocdir}/COMPATIBILITY
+%{coqdocdir}/COPYRIGHT
+%{coqdocdir}/CREDITS
+%{coqdocdir}/INSTALL
+%{coqdocdir}/LICENSE
+%{coqdocdir}/README
%files coqide
%defattr(-,root,root,-)
@@ -308,15 +322,15 @@ rm -rf %{buildroot}
%files doc
%defattr(-,root,root,-)
-%doc Coq-Library-%{version}.pdf
-%doc Coq-Reference-Manual-%{version}.pdf
-%doc Coq-Tutorial-%{version}.pdf
-%doc Coq-RecTutorial.pdf
-%dir %{coqdatadir}
%{tutorialcodedir}
-# Standard permissions with - in defattr make the manual unreadable... unknown how to fix
-%doc refman
-%doc stdlib
+%{coqdocdir}/*
+%exclude %{coqdocdir}/CHANGES
+%exclude %{coqdocdir}/COMPATIBILITY
+%exclude %{coqdocdir}/COPYRIGHT
+%exclude %{coqdocdir}/CREDITS
+%exclude %{coqdocdir}/INSTALL
+%exclude %{coqdocdir}/LICENSE
+%exclude %{coqdocdir}/README
%files emacs
%defattr(-,root,root,-)
@@ -324,6 +338,16 @@ rm -rf %{buildroot}
%doc README.coq-emacs
%changelog
+* Wed Aug 05 2009 Alan Dunn <amdunn at gmail.com> - 8.2pl1-1
+- New upstream release
+- Eliminated modification of tar_base_name that occurred for only version 8.2
+- Added reference to bugzilla bug for ppc64 ExcludeArch
+- HTML form of documentation seems to no longer be distributed -> must generate
+ Decided for consistency to generate all documentation
+- Additional file for iconv - documentation license file
+- Changed tutorial directory name, now also using bundled version
+ of tutorial
+
* Fri Jul 24 2009 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 8.2-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild
Index: import.log
===================================================================
RCS file: /cvs/pkgs/rpms/coq/devel/import.log,v
retrieving revision 1.8
retrieving revision 1.9
diff -u -p -r1.8 -r1.9
--- import.log 19 Jun 2009 11:14:53 -0000 1.8
+++ import.log 5 Aug 2009 21:33:00 -0000 1.9
@@ -6,3 +6,4 @@ coq-8_1pl3-5_fc9:HEAD:coq-8.1pl3-5.fc9.s
coq-8_1pl4-2_fc10:HEAD:coq-8.1pl4-2.fc10.src.rpm:1236185498
coq-8_1pl4-3_fc10:HEAD:coq-8.1pl4-3.fc10.src.rpm:1236186130
coq-8_2-1_fc10:HEAD:coq-8.2-1.fc10.src.rpm:1245409718
+coq-8_2pl1-1_fc10:HEAD:coq-8.2pl1-1.fc10.src.rpm:1249507545
Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/coq/devel/sources,v
retrieving revision 1.5
retrieving revision 1.6
diff -u -p -r1.5 -r1.6
--- sources 19 Jun 2009 11:14:53 -0000 1.5
+++ sources 5 Aug 2009 21:33:00 -0000 1.6
@@ -1,7 +1 @@
-0e3d5eac23416ec75dd59fabdcc1367c Coq-RecTutorial.pdf.gz
-127760a6d9b9bcd213cdd58ab191a363 Coq-Library-8.2.pdf.gz
-b97ab411eb3288ded1d9f8c27e308115 Coq-Reference-Manual-8.2.pdf.gz
-29b7e61e742b17c904739f546223f2e0 Coq-Tutorial-8.2.pdf.gz
-6907d97342e7b547e2e6d905a474235d coq-8.2-1.tar.gz
-cc0005c859cbfd574f22242ec9557dc5 coq-refman-html-8.2.tar.gz
-9ff70e125ba31d53b866b8b322031ac6 coq-stdlib-html-8.2.tar.gz
+36eed48bc63ada8abf27f96eb126906c coq-8.2pl1.tar.gz
--- RecTutorial.v DELETED ---
More information about the scm-commits
mailing list