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