[Date Prev][Date Next]   [Thread Prev][Thread Next]   [Thread Index] [Date Index] [Author Index]

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



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 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 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 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 ---


[Date Prev][Date Next]   [Thread Prev][Thread Next]   [Thread Index] [Date Index] [Author Index]