# Upstream includes option for generation of optimized binaries,

# however, specifically generates bytecode versions for certain

# executables even when optimized option is set, namely the following:

# coq-tex, coq_makefile, coq-interface, coqwc, coqdoc, parser, coqdep,

# gallina

# (coqtop.byte, coqide.byte binaries are also made available.)

# .coqide-gtk2rc also produces an rpmlint warning due to its name,

# however, this name is proper as per the Coq documentation

# Disable creation of the debug package: if bytecode executables are

# created find-debuginfo.sh will ruin them, while if optimized

# executables are created they will be stripped by the Makefile

# anyway, thus we won't get anything useful from the debug info

# package creation.

#

# It appears as though ALL of these are necessary to prevent unwanted

# stripping

%define __os_install_post /usr/lib/rpm/brp-compress %{nil}

%define _enable_debug_package 0

%define debug_package %{nil}

Name:		coq

Version:	8.1pl4

Release:	3%{?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 

Source4:	Coq-RecTutorial.pdf.gz

Source5:	coq-refman-html.tar.gz

Source6:	coq-stdlib-html.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

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

ExcludeArch: ppc64

%else

BuildRequires: texlive-latex, texlive-texmf

%endif

%description

Coq is a formal proof management system. It allows for the development

of theorems through first order logic that are mechanically checked by

the machine. Sets of definitions and theorems can be saved as compiled

modules and loaded into the system.

This package provides the main Coq binary without an optional IDE,

Coqide.

# The IDE's package name will become "coq-coqide".  That way,

# searching for either "coqide" (the Ubuntu/Debian package name, and

# also the full name of the IDE) or "coq" and "ide" will find

# this. (If the package were named "coq-ide", the former would fail.)

%package coqide

Group:		Applications/Engineering

Summary:	Coqide IDE for Coq proof management system

Requires:	coq

%description coqide

Coq is a formal proof management system. It allows for the development

of theorems through first order logic that are mechanically checked by

the machine. Sets of definitions and theorems can be saved as compiled

modules and loaded into the system.

This package provides Coqide, a lightweight IDE for Coq.

%package doc

Group:		Applications/Engineering

Summary:	Documentation for Coq proof management system

%description doc

Coq is a formal proof management system. It allows for the development

of theorems through first order logic that are mechanically checked by

the machine. Sets of definitions and theorems can be saved as compiled

modules and loaded into the system.

This package provides documentation and tutorials for the system. The

main documentation comes in two parts: the main Library documentation,

which decribes all Coq.* modules, and the Reference Manual, which

gives a more complete description of the whole system. Included are

also HTML versions of both. Furthermore, there are two tutorials, the

main one, and one specifically on recursive types. The example code

for the latter is also included.

%package emacs

Group:		Applications/Engineering

Summary:	Elisp files for Coq proof management system

Requires:	coq, emacs

%description emacs

Coq is a formal proof management system. It allows for the development

of theorems through first order logic that are mechanically checked by

the machine. Sets of definitions and theorems can be saved as compiled

modules and loaded into the system.

This package provides emacs mode files for formatting Coq input.

%prep

%setup -q

# Patch description:

# Considered each of the seven patches from the Debian Coq package:

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

#

# For most patches I merely reproduced the results in non-dpatch

# form. I opted for no patching in cases where it did not seem

# necessary or immediately correct.

#

# - browser.dpatch: changes firefox option for linux, however, link

# x-www-browser does not exist in Fedora setup, and changing this

# option does not actually fix the problem in the IDE wherein a

# browser window needs to be open in order to actually open any help

# file -> do not change until the real source of the problem can be

# 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

%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

# 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

# Fix some files that are not in UTF-8 encoding

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

# Seems like setup only sets up the main file

cp %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 %SOURCE10 .

gunzip *.gz

for f in *.tar; do

tar xf $f

done

%build

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

# optimized compiler:

#

# bin/coqtop.opt -boot -nois -compile theories/Init/Notations

#

# 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

%ifarch ppc64

%define opt 0

%endif

# Define opt flag based upon prior opt detection and restrictions

%if %{opt}

%define opt_option --opt

%else

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

make world VERBOSE=1

# Fix permissions in the documentation

chmod -R a+rX refman stdlib

# Clear any execstack permissions that ELF binaries may have

for f in bin/*; do

file $f | grep "ELF" && execstack -c $f

done

%install

rm -rf %{buildroot}

make COQINSTALLPREFIX="%{buildroot}" install

# Install desktop icon and menu entry

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

desktop-file-install --vendor="fedora"			\

--dir=%{buildroot}%{_datadir}/applications		\

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

done

# Install tutorial code

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

%define prelinkconfdir %{_sysconfdir}/prelink.conf.d

mkdir -p %{buildroot}%{prelinkconfdir}

mv %{prelinkfilename} %{buildroot}%{prelinkconfdir}

%clean

rm -rf %{buildroot}

# Note: we want to keep both coqtop.opt and coqtop.byte because the

# byte compiled version can be used to compile new version through

# coqmktop

%files

%defattr(-,root,root,-)

%doc CHANGES COMPATIBILITY COPYRIGHT CREDITS INSTALL KNOWN-BUGS LICENSE README

%doc %{_mandir}/man1/*

%{coqdatadir}

%{_bindir}/coq*

%{_bindir}/gallina

# %%{_bindir}/coq-parser

# %%if %%{opt}

# %%{_bindir}/coq-parser.opt

# %%endif

# Exclude ide files to put in a separate package

%exclude %{_bindir}/coqide*

%exclude %{coqdatadir}/ide

%if %{opt}

%exclude %{coqdatadir}/*.cmxa

%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

%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-RecTutorial.pdf

%dir %{coqdatadir}

%{tutorialcodedir}

# Standard permissions with - in defattr make the manual unreadable... unknown how to fix

%doc refman

%doc stdlib

%files emacs

%defattr(-,root,root,-)

%{_datadir}/emacs/site-lisp/coq*

%doc README.coq-emacs

%changelog

* Wed Mar 04 2009 Alan Dunn <amdunn@gmail.com> - 8.1pl4-3

- Minor change to cmxa-install patch instruction

- Fixed to work with lablgtk 2.12

* Tue Feb 24 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 8.1pl4-2

- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild 

* Fri Dec  5 2008 Richard W.M. Jones <rjones@redhat.com> - 8.1pl4-1

- New upstream version 8.1pl4.

- Attempt to rebuild against OCaml 3.11.0.

- Run make with VERBOSE=1 so we can see the actual commands.

- Pass -camlp5dir to configure so it uses camlp5 (overriding existence

  of camlp4 if it happens to be installed).

* Wed Oct 22 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-5

- Added Coq .v files into the main package at user request.

* Tue Sep 09 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-4

- Added creation of prelink blacklist for any bytecode files.

- Fixed execstack status for binaries.

* Tue Aug 05 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-3

- Changed parser to coq-parser to avoid name conflict with

  coda-client.

- Made make process noisy again.

* Sun Jul 20 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-2.1

- Minor bump for Fedora 8 to bring it into line with the rest.

* Thu Jul 17 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-2

- Added check for Fedora distribution number to allow for Fedora 8 release.

* Wed Jun 14 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-1

- Initial Fedora RPM version.