rpms/coq/devel coq-check-8.2.patch, NONE, 1.1 coq-makefile-strip-8.2.patch, NONE, 1.1 coq-micromega-8.2.patch, NONE, 1.1 .cvsignore, 1.4, 1.5 coq.spec, 1.10, 1.11 import.log, 1.7, 1.8 sources, 1.4, 1.5 check.patch, 1.1, NONE cmxa-install.patch, 1.3, NONE coq-icon.png, 1.1, NONE coq-lablgtk-2.12.patch, 1.1, NONE makefile-parser.patch, 1.1, NONE makefile-strip.patch, 1.1, NONE makefile.patch, 1.1, NONE parser-man.patch, 1.1, NONE
Alan Dunn
amdunn at fedoraproject.org
Fri Jun 19 11:14:54 UTC 2009
- Previous message: rpms/jabberd/devel jabberd.spec,1.33,1.34
- Next message: rpms/blender/devel export-3ds-0.71.py, 1.1, NONE import-3ds-0.7.py, 1.1, NONE blender.png, 1.1, NONE blender.desktop, 1.3, NONE
- Messages sorted by:
[ date ]
[ thread ]
[ subject ]
[ author ]
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 at gmail.com> - 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 at gmail.com> - 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 at lists.fedoraproject.org> 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 ---
- Previous message: rpms/jabberd/devel jabberd.spec,1.33,1.34
- Next message: rpms/blender/devel export-3ds-0.71.py, 1.1, NONE import-3ds-0.7.py, 1.1, NONE blender.png, 1.1, NONE blender.desktop, 1.3, NONE
- Messages sorted by:
[ date ]
[ thread ]
[ subject ]
[ author ]
More information about the scm-commits
mailing list