Author: amdunn Update of /cvs/pkgs/rpms/coq/devel In directory cvs1.fedora.phx.redhat.com:/tmp/cvs-serv5306/devel Modified Files: .cvsignore coq.spec import.log sources Added Files: coq-check-8.2.patch coq-makefile-strip-8.2.patch coq-micromega-8.2.patch Removed Files: check.patch cmxa-install.patch coq-icon.png coq-lablgtk-2.12.patch makefile-parser.patch makefile-strip.patch makefile.patch parser-man.patch Log Message: * Thu Jun 18 2009 Alan Dunn <amdunn@xxxxxxxxx> - 8.2-1 - New upstream release - Seems documentation license has changed or wasn't explicitly stated before, fixed (is ok Fedora license) - Added versioning to documentation - Removed special OCaml, TeX logic for Fedora < 9 (no longer relevant) - Dropped makefile patch for compiling grammar.cma (fixed in Coq 8.2) - Dropped cmxa-install patch (fixed in Coq 8.2) - Changed makefile-strip patch and name (not yet fixed upstream...) - Changed check.patch -> coq-check-(version).patch, slightly changed for 8.2 (not yet fixed upstream...) - Dropped parser-renaming makefile-parser.patch, parser-man.patch (fixed in Coq 8.2) - Dropped coq-lablgtk-2.12.patch (fixed in Coq 8.2) - Changed way source (.v) files are installed - Stopped addition of other icon file (icon fixed in Coq 8.2) - Bytecode executables are now "clean" (not build with custom -> don't need to configure prelink around these) - define -> global - Added ExcludeArch sparc64 coq-check-8.2.patch: --- NEW FILE coq-check-8.2.patch --- --- test-suite/check 2009-01-05 09:01:04.000000000 -0500 +++ test-suite/check 2009-04-08 08:05:08.000000000 -0400 @@ -52,7 +52,7 @@ nbtests=`expr $nbtests + 1` printf " "$f"..." tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` - $command $f 2>&1 | grep -v "Welcome to Coq" | grep -v "Skipping rcfile loading" > $tmpoutput + $command $f 2>&1 | grep -v "Welcome to Coq" | grep -v "Skipping rcfile loading" | grep -v "some rule has been masked" > $tmpoutput foutput=`dirname $f`/`basename $f .v`.out diff $tmpoutput $foutput > /dev/null 2>&1 if [ $? = 0 ]; then coq-makefile-strip-8.2.patch: --- NEW FILE coq-makefile-strip-8.2.patch --- --- Makefile.build 2009-02-17 11:14:07.000000000 -0500 +++ Makefile.build 2009-04-08 07:47:41.000000000 -0400 @@ -468,6 +468,7 @@ bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(INTERFACECMX) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@ $(INTERFACECMX) + $(STRIP) $@ bin/coq-parser$(EXE):$(LIBCOQRUN) $(PARSERCMO) $(SHOW)'OCAMLC -o $@' @@ -478,6 +479,7 @@ $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \ $(LIBCOQRUN) $(DYNLINKCMXA) str.cmxa nums.cmxa $(CMXA) $(PARSERCMX) + $(STRIP) $@ pcoq-files:: $(INTERFACEVO) $(INTERFACERC) coq-micromega-8.2.patch: --- NEW FILE coq-micromega-8.2.patch --- --- contrib/micromega/coq_micromega.ml 2009-01-05 09:01:04.000000000 -0500 +++ contrib/micromega/coq_micromega.ml 2009-04-08 12:52:49.000000000 -0400 @@ -1192,9 +1192,7 @@ let tmp_from = Filename.temp_file "csdpcert" ".out" in output_value ch_to (provername,poly : provername * micromega_polys); close_out ch_to; - let cmdname = - List.fold_left Filename.concat (Envars.coqlib ()) - ["contrib"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in + let cmdname = "csdpcert" in let c = Sys.command (cmdname ^" "^ tmp_to ^" "^ tmp_from) in (try Sys.remove tmp_to with _ -> ()); if c <> 0 then Util.error ("Failed to call csdp certificate generator"); Index: .cvsignore =================================================================== RCS file: /cvs/pkgs/rpms/coq/devel/.cvsignore,v retrieving revision 1.4 retrieving revision 1.5 diff -u -p -r1.4 -r1.5 --- .cvsignore 4 Mar 2009 16:58:27 -0000 1.4 +++ .cvsignore 19 Jun 2009 11:14:51 -0000 1.5 @@ -1,7 +1,7 @@ -Coq-Library.pdf.gz Coq-RecTutorial.pdf.gz -Coq-Reference-Manual.pdf.gz -Coq-Tutorial.v.pdf.gz -coq-8.1pl4.tar.gz -coq-refman-html.tar.gz -coq-stdlib-html.tar.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 Index: coq.spec =================================================================== RCS file: /cvs/pkgs/rpms/coq/devel/coq.spec,v retrieving revision 1.10 retrieving revision 1.11 diff -u -p -r1.10 -r1.11 --- coq.spec 17 Jun 2009 10:53:40 -0000 1.10 +++ coq.spec 19 Jun 2009 11:14:52 -0000 1.11 @@ -17,51 +17,46 @@ # package creation. # # It appears as though ALL of these are necessary to prevent unwanted -# stripping +# stripping (necessary anymore?) -%define __os_install_post /usr/lib/rpm/brp-compress %{nil} -%define _enable_debug_package 0 -%define debug_package %{nil} +%global __os_install_post /usr/lib/rpm/brp-compress %{nil} +%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.1pl4 -Release: 3%{?dist}.1 +Version: 8.2 +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/coq-%{version}.tar.gz -Source1: Coq-Library.pdf.gz -Source2: Coq-Reference-Manual.pdf.gz -Source3: Coq-Tutorial.v.pdf.gz +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.tar.gz -Source6: coq-stdlib-html.tar.gz +Source5: coq-refman-html-%{version}.tar.gz +Source6: coq-stdlib-html-%{version}.tar.gz Source7: RecTutorial.v Source8: coqide.desktop -Source9: coq-icon.png Source10: README.coq-emacs -Patch0: makefile.patch -Patch1: cmxa-install.patch -Patch2: makefile-strip.patch -Patch3: check.patch -Patch4: makefile-parser.patch -Patch5: parser-man.patch -Patch6: coq-lablgtk-2.12.patch +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, prelink - - -%if 0%{?fedora} < 9 -BuildRequires: tetex, tetex-latex -# There's no ocaml-camlp5-devel for ppc64 in Fedora <= 8 -# bz# 458467 +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 +ExcludeArch: s390 s390x sparc64 +# Getting an error re: pthread_atfork - going to file a bugzilla bug +# and number will end up here ExcludeArch: ppc64 -%else -BuildRequires: texlive-latex, texlive-texmf -%endif -ExcludeArch: s390 s390x %description Coq is a formal proof management system. It allows for the development @@ -91,6 +86,7 @@ This package provides Coqide, a lightwei %package doc Group: Applications/Engineering +License: Open Publication Summary: Documentation for Coq proof management system %description doc @@ -121,10 +117,11 @@ modules and loaded into the system. This package provides emacs mode files for formatting Coq input. %prep -%setup -q +%setup -q -n %{tar_base_name} # Patch description: -# Considered each of the seven patches from the Debian Coq package: +# Considered each of the seven patches from the Debian Coq package +# (ones not listed are eliminated from the list - see changelog) # Credit goes to the Debian patch creators for their patches # (See http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/trunk/debian/patches/?rev=0&sc=0) @@ -142,42 +139,25 @@ This package provides emacs mode files f # detected # - check.dpatch: suppress a test warning, similar change made in my # check.patch -# - cmxa-install.dpatch: fixes cmxa install by testing for opt, similar -# change made in cmxa-install.patch -# - configure.dpatch: fixes detection of ocamlopt - We do this detection -# seperately anyway in this RPM, no change made # - coqdoc_stdlib.dpatch: extra documentation option - Perhaps do this # in the future, but for now, no change made -# - makefile.dpatch: fix testing on non-native architecture compiles, similar change made in makefile.patch # - no-complexity-test.dpatch: turn off some of the tests - Perhaps this # change was made due to a failure in complexity tests when they # "don't run quickly enough", which is likely to be incredibly # variable, but unsure, so no change made +# I created patch0 to fix stripping for some native-code binaries, +# unlike the inconsistent way it was done in the original makefile %patch0 -%patch1 - -# I created patch3 to consistently strip native-code binaries, unlike -# the inconsistent way it was done in the original makefile -%patch2 # This patch may not be strictly necessary unless the tests are # incorporated into the build process somehow. However, the tests don't # work properly without it. -%patch3 +%patch1 -# Rename binary parser -> coq-parser to avoid a name conflict with -# other packages (and also to be more informative) -# Patch manpage as well. -# Upstream agreed this was a good idea. -%patch4 -%patch5 -mv man/parser.1 man/coq-parser.1 - -# Minor fix to accommodate a changed signature in lablgtk 2.12 -if grep accepts_tab %{_libdir}/ocaml/lablgtk2/gText.mli; then -%patch6 -fi +# Micromega contrib tries to put a binary into share - move it, but +# ensure the contrib files can still properly call the binary +%patch2 # Fix some files that are not in UTF-8 encoding @@ -185,18 +165,18 @@ for f in CHANGES CREDITS COPYRIGHT; do mv $f $f.old; iconv -f ISO-8859-1 -t UTF-8 < $f.old > $f; rm $f.old done -%define emacs_lispdir %{_datadir}/emacs/site-lisp -%define tex_dir %{_datadir}/texmf/tex/latex/misc +%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 %SOURCE9 %SOURCE10 . +cp %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE10 . gunzip *.gz for f in *.tar; do tar xf $f done %build -%define opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0) +%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0) # optimized binary ppc64 building does not work at the moment - the # log files are no real help, but we fail on bootstrap with the @@ -207,18 +187,28 @@ done # appears to be the command that dies. It appears that the status of # OCaml has been somewhat uncertain on ppc64, perhaps this is the cause? # However, bytecode compilation DOES work -> do this for now +# +# Update: now (6/18) appears that neither works, but I'll keep this +# here for now to remind myself when I can get it working on either +# byte or native %ifarch ppc64 -%define opt 0 +%global opt 0 %endif # Define opt flag based upon prior opt detection and restrictions %if %{opt} -%define opt_option --opt +%global opt_option --opt %else -%define opt_option --byte-only +%global opt_option --byte-only %endif -bash configure -prefix %{_prefix} -libdir %{_datadir}/coq -bindir %{_bindir} -mandir %{_mandir} -emacs %{emacs_lispdir} -coqdocdir %{tex_dir} %{opt_option} -reals all -camlp5dir %{_libdir}/ocaml/camlp5 +# Last flag is to locate the coq .so that will be created for bytecode +# executables + +%global coq_sopath %{_libdir}/ocaml/stublibs + +./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 @@ -229,6 +219,10 @@ for f in bin/*; do file $f | grep "ELF" && execstack -c $f done +# Strip shared object (not sure where the best location for a +# makefile patch for this would be) +strip kernel/byterun/dllcoqrun.so + %install rm -rf %{buildroot} @@ -236,13 +230,12 @@ make COQINSTALLPREFIX="%{buildroot}" ins # Install desktop icon and menu entry -%define coqdatadir %{_datadir}/coq +%global coqdatadir %{_datadir}/coq %if %(test -d %{buildroot}%{coqdatadir} && echo 1 || echo 0) != 1 mkdir -p %{buildroot}%{coqdatadir} %endif -cp coq-icon.png %{buildroot}%{coqdatadir} -sed -i -e 's|ICON-LOCATION-BASE|%{coqdatadir}|' coqide.desktop +sed -i -e 's|ICON-LOCATION-BASE|%{coqdatadir}/ide/coq.png|' coqide.desktop desktop-file-install --vendor="fedora" \ --dir=%{buildroot}%{_datadir}/applications \ @@ -250,32 +243,26 @@ coqide.desktop # Install main Coq .v files -for d in `find contrib theories -mindepth 1 -maxdepth 1 -type d`; do -ls $d/*.v 1>/dev/null 2>&1 && mkdir -p %{buildroot}%{coqdatadir}/$d && cp -pr $d/*.v %{buildroot}%{coqdatadir}/$d 2>/dev/null || true +for f in `find contrib theories -name '*.v' -type f`; do +mkdir -p %{buildroot}%{coqdatadir}/`dirname $f` && cp -p $f %{buildroot}%{coqdatadir}/`dirname $f` done # Install tutorial code -%define tutorialcodedir %{coqdatadir}/tutorial +%global tutorialcodedir %{coqdatadir}/tutorial %if %(test -d %{buildroot}%{tutorialcodedir} && echo 1 || echo 0) != 1 mkdir -p %{buildroot}%{tutorialcodedir} %endif mv RecTutorial.v %{buildroot}%{tutorialcodedir} -# Make sure that prelink does not foul up our bytecode executables by -# stripping them with a cron job. This is done in install to ensure -# that exactly the files that are eventually installed are in the -# list, not all of the files in the bin directory of the build - -%define prelinkfilename %{name}-prelink.conf -cd %{buildroot}%{_bindir} -for f in *; do -file $f | grep "not stripped" | sed -e 's/:.*//' -e 's!^!-b %{_bindir}/!' >> %{prelinkfilename} -done +# Coq tries to move a .so into share - move it (easier than a makefile +# patch) + +mkdir -p %{buildroot}%{coq_sopath} +mv %{buildroot}%{coqdatadir}/dllcoqrun.so %{buildroot}%{coq_sopath} -%define prelinkconfdir %{_sysconfdir}/prelink.conf.d -mkdir -p %{buildroot}%{prelinkconfdir} -mv %{prelinkfilename} %{buildroot}%{prelinkconfdir} +# Micromega contrib tries to sneak an executable into share - move it +mv %{buildroot}%{coqdatadir}/contrib/micromega/csdpcert %{buildroot}%{_bindir} %clean rm -rf %{buildroot} @@ -284,48 +271,46 @@ rm -rf %{buildroot} # byte compiled version can be used to compile new version through # coqmktop +# Exclude libcoqrun.a only when it is installed (this appears to be +# only for the native compile case) + %files %defattr(-,root,root,-) -%doc CHANGES COMPATIBILITY COPYRIGHT CREDITS INSTALL KNOWN-BUGS LICENSE README +%doc CHANGES COMPATIBILITY COPYRIGHT CREDITS INSTALL LICENSE README %doc %{_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}/coq-parser -# %%if %%{opt} -# %%{_bindir}/coq-parser.opt -# %%endif -# Exclude ide files to put in a separate package +%{_bindir}/csdpcert %exclude %{_bindir}/coqide* %exclude %{coqdatadir}/ide %if %{opt} -%exclude %{coqdatadir}/*.cmxa +%exclude %{coqdatadir}/*/*.cmxa +%exclude %{coqdatadir}/*/*.cmx +%exclude %{coqdatadir}/*/*.a +%exclude %{coqdatadir}/*/*.o %endif %{tex_dir}/coq* -# We DO want to replace any such file with this name - it will only be -# for Coq, and we want to correctly reflect the set of files that -# needs to be blacklisted from prelink with this new install -%config %{prelinkconfdir}/%{prelinkfilename} %files coqide %defattr(-,root,root,-) %doc INSTALL.ide %{_bindir}/coqide* -%{_datadir}/coq/ide -# Exclude a corrupted file from the tarball -%exclude %{_datadir}/coq/ide/coq.png -# Instead include a non-corrupted icon somewhere else +%{coqdatadir}/ide %dir %{coqdatadir} -%{coqdatadir}/coq-icon.png # Is it ok to assume this is what desktop-file-install renames coqide.desktop to? %{_datadir}/applications/fedora-coqide.desktop %files doc %defattr(-,root,root,-) -%doc Coq-Library.pdf -%doc Coq-Reference-Manual.pdf -%doc Coq-Tutorial.v.pdf +%doc Coq-Library-%{version}.pdf +%doc Coq-Reference-Manual-%{version}.pdf +%doc Coq-Tutorial-%{version}.pdf %doc Coq-RecTutorial.pdf %dir %{coqdatadir} %{tutorialcodedir} @@ -333,14 +318,33 @@ rm -rf %{buildroot} %doc refman %doc stdlib - %files emacs %defattr(-,root,root,-) %{_datadir}/emacs/site-lisp/coq* %doc README.coq-emacs - %changelog +* Thu Jun 18 2009 Alan Dunn <amdunn@xxxxxxxxx> - 8.2-1 +- New upstream release +- Seems documentation license has changed or wasn't explicitly stated + before, fixed (is ok Fedora license) +- Added versioning to documentation +- Removed special OCaml, TeX logic for Fedora < 9 (no longer relevant) +- Dropped makefile patch for compiling grammar.cma (fixed in Coq 8.2) +- Dropped cmxa-install patch (fixed in Coq 8.2) +- Changed makefile-strip patch and name (not yet fixed upstream...) +- Changed check.patch -> coq-check-(version).patch, slightly changed + for 8.2 (not yet fixed upstream...) +- Dropped parser-renaming makefile-parser.patch, parser-man.patch + (fixed in Coq 8.2) +- Dropped coq-lablgtk-2.12.patch (fixed in Coq 8.2) +- Changed way source (.v) files are installed +- Stopped addition of other icon file (icon fixed in Coq 8.2) +- Bytecode executables are now "clean" (not build with custom -> don't + need to configure prelink around these) +- define -> global +- Added ExcludeArch sparc64 + * Wed Jun 17 2009 S390x secondary arch maintainer <fedora-s390x@xxxxxxxxxxxxxxxxxxxxxxx> 8.1pl4-3.1 - ExcludeArch s390, s390x as we don't have OCaml on those archs Index: import.log =================================================================== RCS file: /cvs/pkgs/rpms/coq/devel/import.log,v retrieving revision 1.7 retrieving revision 1.8 diff -u -p -r1.7 -r1.8 --- import.log 4 Mar 2009 17:07:29 -0000 1.7 +++ import.log 19 Jun 2009 11:14:53 -0000 1.8 @@ -5,3 +5,4 @@ coq-8_1pl3-4_fc9:HEAD:coq-8.1pl3-4.fc9.s coq-8_1pl3-5_fc9:HEAD:coq-8.1pl3-5.fc9.src.rpm:1224703139 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 Index: sources =================================================================== RCS file: /cvs/pkgs/rpms/coq/devel/sources,v retrieving revision 1.4 retrieving revision 1.5 diff -u -p -r1.4 -r1.5 --- sources 4 Mar 2009 16:58:27 -0000 1.4 +++ sources 19 Jun 2009 11:14:53 -0000 1.5 @@ -1,7 +1,7 @@ -8b14a9c8f65ea5bd592901b3649346a7 Coq-Library.pdf.gz 0e3d5eac23416ec75dd59fabdcc1367c Coq-RecTutorial.pdf.gz -021c58a1f2e5d029928ffae0cc9703b0 Coq-Reference-Manual.pdf.gz -bcb4d1c4857bfdae5c22f8fc0be6853c Coq-Tutorial.v.pdf.gz -8fa623538d362d8f48d78e598c43215e coq-8.1pl4.tar.gz -04285e3a76571db6e1d2fbe198c76120 coq-refman-html.tar.gz -17b1edf9122fd89c8b99d4e047b54fb8 coq-stdlib-html.tar.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 --- check.patch DELETED --- --- cmxa-install.patch DELETED --- --- coq-lablgtk-2.12.patch DELETED --- --- makefile-parser.patch DELETED --- --- makefile-strip.patch DELETED --- --- makefile.patch DELETED --- --- parser-man.patch DELETED --- _______________________________________________ Fedora-ocaml-list mailing list Fedora-ocaml-list@xxxxxxxxxx https://www.redhat.com/mailman/listinfo/fedora-ocaml-list