%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)

%global debug_package %{nil}

%global tar_base_name coq-%{version}

%global tex_dir %{_texmf_vendor}/tex/latex/misc

# 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

Name:           coq

Version:        8.3pl2

Release:        2%{?dist}

Summary:        Proof management system

Group:          Applications/Engineering

License:        LGPLv2

URL:            http://coq.inria.fr/

Source0:        http://coq.inria.fr/V%{version}/files/%{tar_base_name}.tar.gz

Source1:        coqide.desktop

Source2:        README.coq-emacs

Source3:        README.coq-xemacs

Source4:        coq.xml

# This patch was suggested by upstream to workaround a camlp5 bug (691913).

# Remove this once ocaml-camlp5 > 6.02.2 is available.

Patch0:         coq-camlp5-bug.patch

BuildRequires:  ocaml >= 3.10.0, ocaml-camlp5-devel, ocaml-lablgtk-devel

BuildRequires:  desktop-file-utils, emacs-nox, xemacs-nox

BuildRequires:  emacs-proofgeneral, xemacs-proofgeneral

# For documentation

BuildRequires:  tex(latex), hevea

Requires(posttrans): tex(tex)

Requires(postun): tex(tex)

# This should always match the list in the ocaml spec file.

# TODO: ppc64 is NOT currently on this list, due to a missing hevea package.

ExclusiveArch: alpha armv4l %{ix86} ia64 x86_64 ppc sparc sparcv9

%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:       %{name} = %{version}-%{release}, xdg-utils

%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

License:        Open Publication

Summary:        Documentation for Coq proof management system

BuildArch:      noarch

%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 describes 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:        GNU Emacs support for Coq proof management system

Requires:       %{name} = %{version}-%{release}

Requires:       emacs(bin) >= %{_emacs_version}

Requires:       emacs-proofgeneral

BuildArch:      noarch

%description emacs

This package provides GNU Emacs mode files for formatting Coq input.

%package emacs-el

Group:          Applications/Engineering

Summary:        Elisp source files for Coq proof management system

Requires:       %{name}-emacs = %{version}-%{release}

BuildArch:      noarch

%description emacs-el

This package contains the Elisp source files for Coq's Emacs support.

This package is not needed to use the Emacs interface.

%package xemacs

Group:          Applications/Engineering

Summary:        XEmacs support for Coq proof management system

Requires:       %{name} = %{version}-%{release}

Requires:       xemacs(bin) >= %{_xemacs_version}

Requires:       xemacs-proofgeneral

BuildArch:      noarch

%description xemacs

This package provides XEmacs mode files for formatting Coq input.

%package xemacs-el

Group:          Applications/Engineering

Summary:        Elisp source files for Coq proof management system

Requires:       %{name}-xemacs = %{version}-%{release}

BuildArch:      noarch

%description xemacs-el

This package contains the Elisp source files for Coq's XEmacs support.

This package is not needed to use the XEmacs interface.

%prep

%setup -q -n %{tar_base_name}

%patch0

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

for f in CHANGES CREDITS doc/LICENSE; do

  iconv -f ISO-8859-1 -t UTF-8 -o $f.utf8 $f

  touch -r $f $f.utf8

  mv -f $f.utf8 $f

done

cp -p %SOURCE1 %SOURCE2 %SOURCE3 .

%build

# Define opt flag based upon prior opt detection and restrictions

%if %{opt}

%global opt_option --opt

%else

%global opt_option --byte-only

%endif

%global coqdocdir %{_defaultdocdir}/coq-%{version}

./configure -prefix %{_prefix}     \

            -libdir %{_libdir}/coq \

            -bindir %{_bindir}     \

            -mandir %{_mandir}     \

            -docdir %{coqdocdir}   \

            -emacs %{_emacs_sitelispdir} \

            -coqdocdir %{tex_dir}  \

            %{opt_option} \

            -browser "xdg-open %s" \

            -camlp5dir %{_libdir}/ocaml/camlp5

export CAML_LD_LIBRARY_PATH=`pwd`/kernel/byterun:${CAML_LD_LIBRARY_PATH}

make world VERBOSE=1

# Strip shared objects (not sure where the best location for a

# makefile patch for this would be).

strip kernel/byterun/dllcoqrun.so

find plugins -name \*.cmxs | xargs strip

%install

make COQINSTALLPREFIX="%{buildroot}%{_prefix}" OLDROOT="%{_prefix}" install

# Install desktop icon and menu entry

%global coqdatadir %{_libdir}/coq

%if %(test -d %{buildroot}%{coqdatadir} && echo 1 || echo 0) != 1

mkdir -p %{buildroot}%{coqdatadir}

%endif

sed -i -e 's|ICON-LOCATION-BASE|%{coqdatadir}/ide/coq.png|' coqide.desktop

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

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

coqide.desktop

# Temporary workaround for coq 8.3 install bugs.

# These files have to be installed for coq's provides to match its requires.

cp -p plugins/dp/fol.cmi %{buildroot}%{coqdatadir}/plugins/dp

cp -p plugins/extraction/miniml.cmi %{buildroot}%{coqdatadir}/plugins/extraction

cp -p plugins/micromega/sos_lib.cmi %{buildroot}%{coqdatadir}/plugins/micromega

cp -p proofs/decl_expr.cmi %{buildroot}%{coqdatadir}/proofs

# Make a MIME type for .v files

mkdir -p %{buildroot}%{_datadir}/mime/packages

cp -p %{SOURCE4} %{buildroot}%{_datadir}/mime/packages

# Install main Coq .v files

for f in `find plugin theories -name '*.v' -type f`; do

mkdir -p %{buildroot}%{coqdatadir}/`dirname $f` && cp -p $f %{buildroot}%{coqdatadir}/`dirname $f`

done

# Install tutorial code

%global tutorialcodedir %{coqdatadir}/RecTutorial

%if %(test -d %{buildroot}%{tutorialcodedir} && echo 1 || echo 0) != 1

mkdir -p %{buildroot}%{tutorialcodedir}

%endif

cp -p doc/RecTutorial/RecTutorial.v %{buildroot}%{tutorialcodedir}

ln -s %{tutorialcodedir} %{buildroot}%{coqdatadir}/RecTutorial

# Install documentation not installed by install-doc in Makefile

for f in CHANGES COMPATIBILITY COPYRIGHT CREDITS INSTALL LICENSE README;

do cp -p $f %{buildroot}%{coqdocdir};

done

# We don't need both PostScript and PDF documentation

rm -fr %{buildroot}%{coqdocdir}/ps

# Don't install libcoqrun.a (it might not exist, but get rid of it if it does)

rm -f %{buildroot}%{coqdatadir}/libcoqrun.a

# Copy the Emacs support files for XEmacs, and byte compile

mkdir -p %{buildroot}%{_xemacs_sitelispdir}/coq

cp -p %{buildroot}%{_emacs_sitelispdir}/* %{buildroot}%{_xemacs_sitelispdir}/coq

cd %{buildroot}%{_xemacs_sitelispdir}/coq

%{_xemacs_bytecompile} *.el

# Move Emacs support files to a subdir and byte compile

mkdir -p %{buildroot}%{_emacs_sitelispdir}/coq

cd %{buildroot}%{_emacs_sitelispdir}/coq

mv ../*.el .

%{_emacs_bytecompile} *.el

%posttrans

mktexlsr &> /dev/null || :

update-mime-database %{_datadir}/mime &> /dev/null || :

update-desktop-database -q &> /dev/null || :

%postun

if [ $1 -eq 0 ]; then

  update-desktop-database -q &> /dev/null

  update-mime-database %{_datadir}/mime &> /dev/null || :

  mktexlsr &> /dev/null

fi

# 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

# Exclude libcoqrun.a only when it is installed (this appears to be

# only for the native compile case)

%files

%defattr(-,root,root,-)

# DON'T use the doc macro here or else it wipes out all the other documentation installed!

%{_mandir}/man1/*

%{coqdatadir}

%{_bindir}/coq*

%{_bindir}/gallina

%exclude %{_bindir}/coqide*

%exclude %{coqdatadir}/ide

%if %{opt}

%exclude %{coqdatadir}/*/*.cmxa

%exclude %{coqdatadir}/*/*.a

%endif

%{tex_dir}/coq*

# A few documentation files here should stay in the main package (and

# are excluded from doc), but the bulk of the documentation is in the

# doc subpackage

%dir %{coqdocdir}

%{coqdocdir}/CHANGES

%{coqdocdir}/COMPATIBILITY

%{coqdocdir}/COPYRIGHT

%{coqdocdir}/CREDITS

%{coqdocdir}/INSTALL

%{coqdocdir}/LICENSE

%{coqdocdir}/README

%files coqide

%defattr(-,root,root,-)

%doc INSTALL.ide

%{_bindir}/coqide*

%{coqdatadir}/ide

%exclude %{coqdatadir}/ide/ide.cmxa

%exclude %{coqdatadir}/ide/ide.a

# Is it ok to assume this is what desktop-file-install renames coqide.desktop to?

%{_datadir}/applications/fedora-coqide.desktop

%{_datadir}/mime/packages/coq.xml

%files doc

%defattr(-,root,root,-)

%{coqdocdir}/*

%exclude %{coqdocdir}/CHANGES

%exclude %{coqdocdir}/COMPATIBILITY

%exclude %{coqdocdir}/COPYRIGHT

%exclude %{coqdocdir}/CREDITS

%exclude %{coqdocdir}/INSTALL

%exclude %{coqdocdir}/LICENSE

%exclude %{coqdocdir}/README

%files emacs

%defattr(-,root,root,-)

%dir %{_emacs_sitelispdir}/coq

%{_emacs_sitelispdir}/coq/*.elc

%doc README.coq-emacs

%files emacs-el

%defattr(-,root,root,-)

%{_emacs_sitelispdir}/coq/*.el

%files xemacs

%defattr(-,root,root,-)

%dir %{_xemacs_sitelispdir}/coq

%{_xemacs_sitelispdir}/coq/*.elc

%doc README.coq-xemacs

%files xemacs-el

%defattr(-,root,root,-)

%{_xemacs_sitelispdir}/coq/*.el

%changelog

* Wed Jun 15 2011 Jerry James <loganjerry@gmail.com> - 8.3pl2-2

- Remove workaround for bad documentation link in 8.3pl1, fixed in 8.3pl2

- Revert change in 8.3pl1-1 to split arch-specific stuff from noarch stuff.

  Coq tactics are written in ocaml, which compiles to arch-specific files,

  and those files are stored in the same place as the noarch proof files.

- Move tutorial code into main package; it is small and we can then leave

  all the rest of the documentation as noarch

* Tue Apr 26 2011 Jerry James <loganjerry@gmail.com> - 8.3pl2-1

- New upstream release

- Change the list of supported arches to match the ocaml list, except for

  ppc64, which is missing hevea

* Mon Apr  4 2011 Jerry James <loganjerry@gmail.com> - 8.3pl1-2

- Change the mime type to application/x-coq, and inherit from text/plain

  (bz 530254)

* Thu Mar 31 2011 Jerry James <loganjerry@gmail.com> - 8.3pl1-1

- New upstream release

- Drop BuildRoot tag and clean section

- Drop all patches (all merged or otherwise fixed upstream)

- Comply with latest Ocaml packaging specs

- Identify xdg-open as the default web browser

- Comply with the emacs packaging guidelines, and build an XEmacs package

- The -doc and -emacs* subpackages are now noarch

- Workaround bug 691913

- Drop PostScript documentation; it's identical to PDF documentation

- Deal with arch-specific files in /usr/share; install everything to libdir,

  then move the noarch stuff to datadir, but leave symlinks behind

- Add a new mime type application/x-coqide and use it in the desktop file

- Add post and postun scripts

* Tue Feb 08 2011 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 8.2pl1-2

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

* Wed Aug 05 2009 Alan Dunn <amdunn@gmail.com> - 8.2pl1-1

- New upstream release

- Eliminated modification of tar_base_name that occurred for only version 8.2

- Added reference to bugzilla bug for ppc64 ExcludeArch

- HTML form of documentation seems to no longer be distributed -> must generate

  Decided for consistency to generate all documentation

- Additional file for iconv - documentation license file

- Changed tutorial directory name, now also using bundled version

  of tutorial

* Fri Jul 24 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 8.2-2

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

* 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

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