The full spec file is below -
My motivation for doing things the way I did was that I wanted to
incorporate arbitrarily deep (admittedly I know the depth for this
particular version in advance, but one can imagine this changing
between versions and it didn't seem like a good solution to create
something that would have to be fixed with each upgrade) directory
structures instead of including
/usr/lib/coq/*
/usr/lib/coq/*/*
(etc)
so instead I just took the directory structure as it was created with
find. That's why some files are excluded in the main package and
included in the subpackage. Of course, I suppose I could also just
change the find query to do the exclusion as well... perhaps that's
better? Or perhaps it's considered poor practice to do what I've done
here, is that so? (I don't really know what tradition is as this is my
first package, but I didn't see anything guiding advice in docs and
I've seen other packages do this.)
The full spec file:
Name: coq
Version: 8.1pl3
Release: 1%{?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
BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
BuildRequires: ocaml >= 3.08, ocaml-camlp5-devel
%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.
%package coqide
Group: Applications/Engineering
Summary: Coqide IDE for Coq proof system.
Requires: coq
BuildRequires: ocaml >= 3.08, ocaml-camlp5-devel, gtk+-devel,
ocaml-lablgtk-devel
%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.
%prep
%setup -q
rm -f coqlibfiles coqfiles
rm -f install-emacs install-tex
# Test for emacs site_lisp directory, if so, add relevant files to
roster, else, don't try and install
%define emacsdir %{_datadir}/emacs/site-lisp
%if %(test -e %{emacsdir} && echo 1 || echo 0)
%define emacsopt -emacs %{emacsdir}
echo '%{emacsdir}/coq*' >> coqfiles
%else
%define emacsopt
touch install-emacs
%endif
# Test for tex directory, if so, add relevant files to roster, else,
don't try and install
%define texdir %{_datadir}/texmf/tex/latex/misc
%if %(test -e %{texdir} && echo 1 || echo 0)
%define texopt -coqdocdir %{texdir}
echo "%{texdir}/coqdoc.sty" >> coqfiles
%else
%define texopt
touch install-latex
%endif
%build
./configure -prefix %{_prefix} -bindir %{_bindir} -mandir %{_mandir}
%{emacsopt} %{texopt} -reals all > /dev/null
make world
# Test if we built an optimized parser
%if %(test -e %{buildroot}%{_bindir}/parser.opt && echo 1 || echo 0)
echo "%{_bindir}/parser.opt" >> coqfiles
%endif
%install
rm -rf %{buildroot}
make COQINSTALLPREFIX="%{buildroot}" install
# Build file list for ones that are hard to account for otherwise
find %{buildroot}%{_libdir}/coq -fprint coqlibfiles
sed -i -e "s|%{buildroot}||" coqlibfiles
cat coqlibfiles >> coqfiles
%clean
rm -rf %{buildroot}
make clean
%files -f coqfiles
%defattr(-,root,root)
%doc CHANGES COMPATIBILITY COPYRIGHT CREDITS INSTALL INSTALL.ide
KNOWN-BUGS LICENSE README
%doc %{_mandir}/man1/coq*
%doc %{_mandir}/man1/gallina.1.gz
%doc %{_mandir}/man1/parser.1.gz
%{_bindir}/coq*
%{_bindir}/gallina
%{_bindir}/parser
# Parser.opt included seperately
%exclude %{_bindir}/coqide*
%exclude %{_libdir}/coq/ide/*
%files coqide
%defattr(-,root,root)
%{_bindir}/coqide*
%{_libdir}/coq/ide/*
%changelog
* Wed Jun 14 2008 Alan Dunn <amdunn@xxxxxxxxx> 8.1pl3-1
- Initial version.
Thanks,
- Alan
On Wed, Jun 4, 2008 at 4:57 PM, Michael Schwendt <mschwendt@xxxxxxxxx> wrote:
> On Wed, 4 Jun 2008 14:26:51 -0400, Alan Dunn wrote:
>
>> I'm trying to package the Coq theorem proving system.
>>
>> My goal is to create a main package with the system and then a
>> subpackage for the (optional) IDE. I've written out a spec file, and
>> it does compile (that is, I can generate rpms with "rpmbuild -bb
>> SPECS/coq.spec"), but this process generates quite a number of "file
>> listed twice" warnings that I would like to eliminate like:
>>
>> warning: File listed twice: /usr/lib/coq/contrib
>> warning: File listed twice: /usr/lib/coq/contrib.cma
>> warning: File listed twice: /usr/lib/coq/contrib.cmxa
>> warning: File listed twice: /usr/lib/coq/contrib/field
>> warning: File listed twice: /usr/lib/coq/contrib/field
>> warning: File listed twice: /usr/lib/coq/contrib/field/LegacyField.vo
>> warning: File listed twice: /usr/lib/coq/contrib/field/LegacyField.vo
>> warning: File listed twice: /usr/lib/coq/contrib/field/LegacyField.vo
>> ...
>>
>> (the duplicated warnings are listed multiple times in the output, as
>> are many files)
>>
>> I thought that somehow things could've gone wrong in the files list
>> that I generate to use in the %files section via:
>>
>> find %{buildroot}%{_libdir}/coq -fprint coqlibfiles
>> sed -i -e "s|%{buildroot}||" coqlibfiles
>
> What is in "coqfiles" at this point?
>
>> cat coqlibfiles >> coqfiles
>>
>> but none of the files are duplicated in the coqfiles file
>
> Post the full spec file, because your quoted fragment is incomplete.
> You create "coqlibfiles", then append it to "coqfiles", but whether
> "coqfiles" is empty or set up with other contents is unknown. If
> empty, you could use "-f coqlibiles" directly instead of creating
> a copy.
>
>> %files -f coqfiles
>> %defattr(-,root,root)
>> %doc CHANGES COMPATIBILITY COPYRIGHT CREDITS INSTALL INSTALL.ide
>> KNOWN-BUGS LICENSE README
>> %doc %{_mandir}/man1/coq*
>> %doc %{_mandir}/man1/gallina.1.gz
>> %doc %{_mandir}/man1/parser.1.gz
>> %{_bindir}/coq*
>> %{_bindir}/gallina
>> %{_bindir}/parser
>> # Parser.opt included seperately
>> %exclude %{_bindir}/coqide*
>> %exclude %{_libdir}/coq/ide/*
>>
>> %files coqide
>> %defattr(-,root,root)
>> %{_bindir}/coqide*
>> %{_libdir}/coq/ide/*
>>
>> Anyone know what I'm doing wrong?
>
> Why don't you include and exclude the directories directly
> in the %files sections?
>
> --
> Fedora release 8 (Werewolf) - Linux 2.6.23.15-137.fc8
> loadavg: 1.00 1.04 1.12
>
> --
> fedora-devel-list mailing list
> fedora-devel-list@xxxxxxxxxx
> https://www.redhat.com/mailman/listinfo/fedora-devel-list
>
--
fedora-devel-list mailing list
fedora-devel-list@xxxxxxxxxx
https://www.redhat.com/mailman/listinfo/fedora-devel-list
