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@xxxxxxxxx> - 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@xxxxxxxxx> - 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@xxxxxxxxxxxxxxxxxxxxxxx> - 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 --- _______________________________________________ Fedora-ocaml-list mailing list Fedora-ocaml-list@xxxxxxxxxx https://www.redhat.com/mailman/listinfo/fedora-ocaml-list