|
|
6a9dfbc |
# Upstream includes option for generation of optimized binaries,
|
|
|
6a9dfbc |
# however, specifically generates bytecode versions for certain
|
|
|
6a9dfbc |
# executables even when optimized option is set, namely the following:
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# coq-tex, coq_makefile, coq-interface, coqwc, coqdoc, parser, coqdep,
|
|
|
6a9dfbc |
# gallina
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# (coqtop.byte, coqide.byte binaries are also made available.)
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# .coqide-gtk2rc also produces an rpmlint warning due to its name,
|
|
|
6a9dfbc |
# however, this name is proper as per the Coq documentation
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# Disable creation of the debug package: if bytecode executables are
|
|
|
6a9dfbc |
# created find-debuginfo.sh will ruin them, while if optimized
|
|
|
6a9dfbc |
# executables are created they will be stripped by the Makefile
|
|
|
6a9dfbc |
# anyway, thus we won't get anything useful from the debug info
|
|
|
6a9dfbc |
# package creation.
|
|
|
6a9dfbc |
#
|
|
|
6a9dfbc |
# It appears as though ALL of these are necessary to prevent unwanted
|
|
|
6a9dfbc |
# stripping
|
|
|
0ed1b62 |
|
|
|
6a9dfbc |
%define __os_install_post /usr/lib/rpm/brp-compress %{nil}
|
|
|
6a9dfbc |
%define _enable_debug_package 0
|
|
|
6a9dfbc |
%define debug_package %{nil}
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
Name: coq
|
|
|
6a9dfbc |
Version: 8.1pl3
|
|
|
4b0d0db |
Release: 2%{?dist}.1
|
|
|
6a9dfbc |
Summary: Coq proof management system
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
Group: Applications/Engineering
|
|
|
6a9dfbc |
License: LGPLv2
|
|
|
6a9dfbc |
URL: http://coq.inria.fr/
|
|
|
6a9dfbc |
Source0: http://coq.inria.fr/V%{version}/files/coq-%{version}.tar.gz
|
|
|
6a9dfbc |
Source1: Coq-Library.pdf.gz
|
|
|
6a9dfbc |
Source2: Coq-Reference-Manual.pdf.gz
|
|
|
6a9dfbc |
Source3: Coq-Tutorial.v.pdf.gz
|
|
|
6a9dfbc |
Source4: Coq-RecTutorial.pdf.gz
|
|
|
6a9dfbc |
Source5: coq-refman-html.tar.gz
|
|
|
6a9dfbc |
Source6: coq-stdlib-html.tar.gz
|
|
|
6a9dfbc |
Source7: RecTutorial.v
|
|
|
6a9dfbc |
Source8: coqide.desktop
|
|
|
6a9dfbc |
Source9: coq-icon.png
|
|
|
6a9dfbc |
Source10: README.coq-emacs
|
|
|
6a9dfbc |
Patch0: makefile.patch
|
|
|
6a9dfbc |
Patch1: cmxa-install.patch
|
|
|
6a9dfbc |
Patch2: makefile-strip.patch
|
|
|
6a9dfbc |
Patch3: check.patch
|
|
|
6a9dfbc |
BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
|
|
|
e9ec0a4 |
BuildRequires: ocaml >= 3.08, ocaml-camlp5-devel, gtk2-devel, ocaml-lablgtk-devel, desktop-file-utils, emacs
|
|
|
0ed1b62 |
|
|
|
0ed1b62 |
%if 0%{?fedora} < 9
|
|
|
e9ec0a4 |
BuildRequires: tetex, tetex-latex
|
|
|
0ed1b62 |
# There's no ocaml-camlp5-devel for ppc64 in Fedora <= 8
|
|
|
0ed1b62 |
ExcludeArch: ppc64
|
|
|
e9ec0a4 |
%else
|
|
|
e9ec0a4 |
BuildRequires: texlive-latex, texlive-texmf
|
|
|
e9ec0a4 |
%endif
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%description
|
|
|
6a9dfbc |
Coq is a formal proof management system. It allows for the development
|
|
|
6a9dfbc |
of theorems through first order logic that are mechanically checked by
|
|
|
6a9dfbc |
the machine. Sets of definitions and theorems can be saved as compiled
|
|
|
6a9dfbc |
modules and loaded into the system.
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
This package provides the main Coq binary without an optional IDE,
|
|
|
6a9dfbc |
Coqide.
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# The IDE's package name will become "coq-coqide". That way,
|
|
|
6a9dfbc |
# searching for either "coqide" (the Ubuntu/Debian package name, and
|
|
|
6a9dfbc |
# also the full name of the IDE) or "coq" and "ide" will find
|
|
|
6a9dfbc |
# this. (If the package were named "coq-ide", the former would fail.)
|
|
|
6a9dfbc |
%package coqide
|
|
|
6a9dfbc |
Group: Applications/Engineering
|
|
|
6a9dfbc |
Summary: Coqide IDE for Coq proof management system
|
|
|
6a9dfbc |
Requires: coq
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%description coqide
|
|
|
6a9dfbc |
Coq is a formal proof management system. It allows for the development
|
|
|
6a9dfbc |
of theorems through first order logic that are mechanically checked by
|
|
|
6a9dfbc |
the machine. Sets of definitions and theorems can be saved as compiled
|
|
|
6a9dfbc |
modules and loaded into the system.
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
This package provides Coqide, a lightweight IDE for Coq.
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%package doc
|
|
|
6a9dfbc |
Group: Applications/Engineering
|
|
|
6a9dfbc |
Summary: Documentation for Coq proof management system
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%description doc
|
|
|
6a9dfbc |
Coq is a formal proof management system. It allows for the development
|
|
|
6a9dfbc |
of theorems through first order logic that are mechanically checked by
|
|
|
6a9dfbc |
the machine. Sets of definitions and theorems can be saved as compiled
|
|
|
6a9dfbc |
modules and loaded into the system.
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
This package provides documentation and tutorials for the system. The
|
|
|
6a9dfbc |
main documentation comes in two parts: the main Library documentation,
|
|
|
6a9dfbc |
which decribes all Coq.* modules, and the Reference Manual, which
|
|
|
6a9dfbc |
gives a more complete description of the whole system. Included are
|
|
|
6a9dfbc |
also HTML versions of both. Furthermore, there are two tutorials, the
|
|
|
6a9dfbc |
main one, and one specifically on recursive types. The example code
|
|
|
6a9dfbc |
for the latter is also included.
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%package emacs
|
|
|
6a9dfbc |
Group: Applications/Engineering
|
|
|
6a9dfbc |
Summary: Elisp files for Coq proof management system
|
|
|
6a9dfbc |
Requires: coq, emacs
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%description emacs
|
|
|
6a9dfbc |
Coq is a formal proof management system. It allows for the development
|
|
|
6a9dfbc |
of theorems through first order logic that are mechanically checked by
|
|
|
6a9dfbc |
the machine. Sets of definitions and theorems can be saved as compiled
|
|
|
6a9dfbc |
modules and loaded into the system.
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
This package provides emacs mode files for formatting Coq input.
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%prep
|
|
|
6a9dfbc |
%setup -q
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# Patch description:
|
|
|
6a9dfbc |
# Considered each of the seven patches from the Debian Coq package:
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# Credit goes to the Debian patch creators for their patches
|
|
|
6a9dfbc |
# (See http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/trunk/debian/patches/?rev=0&sc=0)
|
|
|
6a9dfbc |
#
|
|
|
6a9dfbc |
# For most patches I merely reproduced the results in non-dpatch
|
|
|
6a9dfbc |
# form. I opted for no patching in cases where it did not seem
|
|
|
6a9dfbc |
# necessary or immediately correct.
|
|
|
6a9dfbc |
#
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# - browser.dpatch: changes firefox option for linux, however, link
|
|
|
6a9dfbc |
# x-www-browser does not exist in Fedora setup, and changing this
|
|
|
6a9dfbc |
# option does not actually fix the problem in the IDE wherein a
|
|
|
6a9dfbc |
# browser window needs to be open in order to actually open any help
|
|
|
6a9dfbc |
# file -> do not change until the real source of the problem can be
|
|
|
6a9dfbc |
# detected
|
|
|
6a9dfbc |
# - check.dpatch: suppress a test warning, similar change made in my
|
|
|
6a9dfbc |
# check.patch
|
|
|
6a9dfbc |
# - cmxa-install.dpatch: fixes cmxa install by testing for opt, similar
|
|
|
6a9dfbc |
# change made in cmxa-install.patch
|
|
|
6a9dfbc |
# - configure.dpatch: fixes detection of ocamlopt - We do this detection
|
|
|
6a9dfbc |
# seperately anyway in this RPM, no change made
|
|
|
6a9dfbc |
# - coqdoc_stdlib.dpatch: extra documentation option - Perhaps do this
|
|
|
6a9dfbc |
# in the future, but for now, no change made
|
|
|
6a9dfbc |
# - makefile.dpatch: fix testing on non-native architecture compiles, similar change made in makefile.patch
|
|
|
6a9dfbc |
# - no-complexity-test.dpatch: turn off some of the tests - Perhaps this
|
|
|
6a9dfbc |
# change was made due to a failure in complexity tests when they
|
|
|
6a9dfbc |
# "don't run quickly enough", which is likely to be incredibly
|
|
|
6a9dfbc |
# variable, but unsure, so no change made
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%patch0
|
|
|
6a9dfbc |
%patch1
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# I created patch3 to consistently strip native-code binaries, unlike
|
|
|
6a9dfbc |
# the inconsistent way it was done in the original makefile
|
|
|
6a9dfbc |
%patch2
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# This patch may not be strictly necessary unless the tests are
|
|
|
6a9dfbc |
# incorporated into the build process somehow. However, the tests don't
|
|
|
6a9dfbc |
# work properly without it.
|
|
|
6a9dfbc |
%patch3
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# Fix some files that are not in UTF-8 encoding
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
for f in CHANGES CREDITS COPYRIGHT; do
|
|
|
6a9dfbc |
mv $f $f.old; iconv -f ISO-8859-1 -t UTF-8 < $f.old > $f; rm $f.old
|
|
|
6a9dfbc |
done
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%define emacs_lispdir %{_datadir}/emacs/site-lisp
|
|
|
6a9dfbc |
%define tex_dir %{_datadir}/texmf/tex/latex/misc
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# Seems like setup only sets up the main file
|
|
|
6a9dfbc |
cp %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 %SOURCE10 .
|
|
|
6a9dfbc |
gunzip *.gz
|
|
|
6a9dfbc |
for f in *.tar; do
|
|
|
6a9dfbc |
tar xf $f
|
|
|
6a9dfbc |
done
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%build
|
|
|
6a9dfbc |
%define opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# optimized binary ppc64 building does not work at the moment - the
|
|
|
6a9dfbc |
# log files are no real help, but we fail on bootstrap with the
|
|
|
6a9dfbc |
# optimized compiler:
|
|
|
6a9dfbc |
#
|
|
|
6a9dfbc |
# bin/coqtop.opt -boot -nois -compile theories/Init/Notations
|
|
|
6a9dfbc |
#
|
|
|
6a9dfbc |
# appears to be the command that dies. It appears that the status of
|
|
|
6a9dfbc |
# OCaml has been somewhat uncertain on ppc64, perhaps this is the cause?
|
|
|
6a9dfbc |
# However, bytecode compilation DOES work -> do this for now
|
|
|
6a9dfbc |
%ifarch ppc64
|
|
|
6a9dfbc |
%define opt 0
|
|
|
6a9dfbc |
%endif
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# Define opt flag based upon prior opt detection and restrictions
|
|
|
6a9dfbc |
%if %{opt}
|
|
|
6a9dfbc |
%define opt_option --opt
|
|
|
6a9dfbc |
%else
|
|
|
6a9dfbc |
%define opt_option --byte-only
|
|
|
6a9dfbc |
%endif
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
bash configure -prefix %{_prefix} -libdir %{_datadir}/coq -bindir %{_bindir} -mandir %{_mandir} -emacs %{emacs_lispdir} -coqdocdir %{tex_dir} %{opt_option} -reals all > /dev/null
|
|
|
6a9dfbc |
make world 2>/dev/null
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# Fix permissions in the documentation
|
|
|
6a9dfbc |
chmod -R a+rX refman stdlib
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%install
|
|
|
6a9dfbc |
rm -rf %{buildroot}
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
make COQINSTALLPREFIX="%{buildroot}" install
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# Install desktop icon and menu entry
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%define coqdatadir %{_datadir}/coq
|
|
|
6a9dfbc |
%if %(test -d %{buildroot}%{coqdatadir} && echo 1 || echo 0) != 1
|
|
|
6a9dfbc |
mkdir -p %{buildroot}%{coqdatadir}
|
|
|
6a9dfbc |
%endif
|
|
|
6a9dfbc |
cp coq-icon.png %{buildroot}%{coqdatadir}
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
sed -i -e 's|ICON-LOCATION-BASE|%{coqdatadir}|' coqide.desktop
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
desktop-file-install --vendor="fedora" \
|
|
|
6a9dfbc |
--dir=%{buildroot}%{_datadir}/applications \
|
|
|
6a9dfbc |
coqide.desktop
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# Install tutorial code
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%define tutorialcodedir %{coqdatadir}/tutorial
|
|
|
6a9dfbc |
%if %(test -d %{buildroot}%{tutorialcodedir} && echo 1 || echo 0) != 1
|
|
|
6a9dfbc |
mkdir -p %{buildroot}%{tutorialcodedir}
|
|
|
6a9dfbc |
%endif
|
|
|
6a9dfbc |
mv RecTutorial.v %{buildroot}%{tutorialcodedir}
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%clean
|
|
|
6a9dfbc |
rm -rf %{buildroot}
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# Note: we want to keep both coqtop.opt and coqtop.byte because the
|
|
|
6a9dfbc |
# byte compiled version can be used to compile new version through
|
|
|
6a9dfbc |
# coqmktop
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%files
|
|
|
6a9dfbc |
%defattr(-,root,root,-)
|
|
|
6a9dfbc |
%doc CHANGES COMPATIBILITY COPYRIGHT CREDITS INSTALL KNOWN-BUGS LICENSE README
|
|
|
6a9dfbc |
%doc %{_mandir}/man1/coq*
|
|
|
6a9dfbc |
%doc %{_mandir}/man1/gallina.1.gz
|
|
|
6a9dfbc |
%doc %{_mandir}/man1/parser.1.gz
|
|
|
6a9dfbc |
%{_datadir}/coq
|
|
|
6a9dfbc |
%{_bindir}/coq*
|
|
|
6a9dfbc |
%{_bindir}/gallina
|
|
|
6a9dfbc |
%{_bindir}/parser
|
|
|
6a9dfbc |
%if %{opt}
|
|
|
6a9dfbc |
%{_bindir}/parser.opt
|
|
|
6a9dfbc |
%endif
|
|
|
6a9dfbc |
# Exclude ide files to put in a separate package
|
|
|
6a9dfbc |
%exclude %{_bindir}/coqide*
|
|
|
6a9dfbc |
%exclude %{_datadir}/coq/ide
|
|
|
6a9dfbc |
%if %{opt}
|
|
|
6a9dfbc |
%exclude %{_datadir}/coq/*.cmxa
|
|
|
6a9dfbc |
%endif
|
|
|
6a9dfbc |
%{tex_dir}/coq*
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%files coqide
|
|
|
6a9dfbc |
%defattr(-,root,root,-)
|
|
|
6a9dfbc |
%doc INSTALL.ide
|
|
|
6a9dfbc |
%{_bindir}/coqide*
|
|
|
6a9dfbc |
%{_datadir}/coq/ide
|
|
|
6a9dfbc |
# Exclude a corrupted file from the tarball
|
|
|
6a9dfbc |
%exclude %{_datadir}/coq/ide/coq.png
|
|
|
6a9dfbc |
# Instead include a non-corrupted icon somewhere else
|
|
|
6a9dfbc |
%dir %{coqdatadir}
|
|
|
6a9dfbc |
%{coqdatadir}/coq-icon.png
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
# Is it ok to assume this is what desktop-file-install renames coqide.desktop to?
|
|
|
6a9dfbc |
%{_datadir}/applications/fedora-coqide.desktop
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%files doc
|
|
|
6a9dfbc |
%defattr(-,root,root,-)
|
|
|
6a9dfbc |
%doc Coq-Library.pdf
|
|
|
6a9dfbc |
%doc Coq-Reference-Manual.pdf
|
|
|
6a9dfbc |
%doc Coq-Tutorial.v.pdf
|
|
|
6a9dfbc |
%doc Coq-RecTutorial.pdf
|
|
|
6a9dfbc |
%dir %{coqdatadir}
|
|
|
6a9dfbc |
%{tutorialcodedir}
|
|
|
6a9dfbc |
# Standard permissions with - in defattr make the manual unreadable... unknown how to fix
|
|
|
6a9dfbc |
%doc refman
|
|
|
6a9dfbc |
%doc stdlib
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%files emacs
|
|
|
6a9dfbc |
%defattr(-,root,root,-)
|
|
|
6a9dfbc |
%{_datadir}/emacs/site-lisp/coq*
|
|
|
6a9dfbc |
%doc README.coq-emacs
|
|
|
6a9dfbc |
|
|
|
6a9dfbc |
%changelog
|
|
|
4b0d0db |
* Sun Jul 20 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-2.1
|
|
|
4b0d0db |
- Minor bump for Fedora 8 to bring it into line with the rest.
|
|
|
e9ec0a4 |
* Thu Jul 17 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-2
|
|
|
e9ec0a4 |
- Added check for Fedora distribution number to allow for Fedora 8 release.
|
|
|
6a9dfbc |
* Wed Jun 14 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-1
|
|
|
6a9dfbc |
- Initial Fedora RPM version.
|