# 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 (necessary anymore?)
%global __os_install_post /usr/lib/rpm/brp-compress %{nil}
%global _enable_debug_package 0
%global debug_package %{nil}
%global tar_base_name coq-%{version}
Name: coq
Version: 8.2pl1
Release: 2%{?dist}
Summary: Coq 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
Patch0: coq-makefile-strip-8.2.patch
Patch1: coq-check-8.2.patch
Patch2: coq-micromega-8.2.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
# Needed for execstack, NOT for preventing stripping of custom
# bytecode executables as before
BuildRequires: prelink
# For documentation
BuildRequires: texlive-latex, texlive-texmf, hevea
ExcludeArch: s390 s390x sparc64
# ppc64 build fails in both opt and non-opt versions
# bz: 515813
ExcludeArch: ppc64
%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
License: Open Publication
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 -n %{tar_base_name}
# Patch description:
# 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)
#
# 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
# - coqdoc_stdlib.dpatch: extra documentation option - Perhaps do this
# in the future, but for now, no change made
# - 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
# 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.
%patch1
# 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
for f in CHANGES CREDITS COPYRIGHT doc/LICENSE; do
mv $f $f.old; iconv -f ISO-8859-1 -t UTF-8 < $f.old > $f; rm $f.old
done
%global emacs_lispdir %{_datadir}/emacs/site-lisp
%global tex_dir %{_datadir}/texmf/tex/latex/misc
cp %SOURCE1 %SOURCE2 .
%build
%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
# 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
#
# 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
%global opt 0
%endif
# Define opt flag based upon prior opt detection and restrictions
%if %{opt}
%global opt_option --opt
%else
%global opt_option --byte-only
%endif
# Last flag is to locate the coq .so that will be created for bytecode
# executables
%global coq_sopath %{_libdir}/ocaml/stublibs
%global coqdocdir %{_defaultdocdir}/coq-%{version}
./configure -prefix %{_prefix} \
-libdir %{_datadir}/coq \
-bindir %{_bindir} \
-mandir %{_mandir} \
-docdir %{coqdocdir} \
-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
# Clear any execstack permissions that ELF binaries may have
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}
make COQINSTALLPREFIX="%{buildroot}" install
# Install desktop icon and menu entry
%global coqdatadir %{_datadir}/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
# Install main Coq .v files
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
%global tutorialcodedir %{coqdatadir}/RecTutorial
%if %(test -d %{buildroot}%{tutorialcodedir} && echo 1 || echo 0) != 1
mkdir -p %{buildroot}%{tutorialcodedir}
%endif
cp doc/RecTutorial/RecTutorial.v %{buildroot}%{tutorialcodedir}
# Install documentation not installed by install-doc in Makefile
for f in CHANGES COMPATIBILITY COPYRIGHT CREDITS INSTALL LICENSE README;
do cp $f %{buildroot}%{coqdocdir};
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}
# Micromega contrib tries to sneak an executable into share - move it
mv %{buildroot}%{coqdatadir}/contrib/micromega/csdpcert %{buildroot}%{_bindir}
# Don't install libcoqrun.a (it might not exist, but get rid of it if it does)
rm -f %{buildroot}%{coqdatadir}/libcoqrun.a
%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
# 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}
%{coq_sopath}/dllcoqrun.so
%{_bindir}/coq*
%{_bindir}/gallina
%{_bindir}/csdpcert
%exclude %{_bindir}/coqide*
%exclude %{coqdatadir}/ide
%exclude %{coqdatadir}/config/coq_config.cmo
%if %{opt}
%exclude %{coqdatadir}/*/*.cmxa
%exclude %{coqdatadir}/*/*.cmx
%exclude %{coqdatadir}/*/*.a
%exclude %{coqdatadir}/*/*.o
%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
%dir %{coqdatadir}
# 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,-)
%{tutorialcodedir}
%{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,-)
%{_datadir}/emacs/site-lisp/coq*
%doc README.coq-emacs
%changelog
* 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.