rpms/why/devel import.log,1.2,1.3 why.spec,1.4,1.5
Alan Dunn
amdunn at fedoraproject.org
Sat Aug 8 02:35:30 UTC 2009
Author: amdunn
Update of /cvs/pkgs/rpms/why/devel
In directory cvs1.fedora.phx.redhat.com:/tmp/cvs-serv4980/devel
Modified Files:
import.log why.spec
Log Message:
* Fri Aug 07 2009 Alan Dunn <amdunn at gmail.com> - 2.17-4
- Removed now irrelevant check for no OCaml in Fedora < 9 (those
distributions are EOL)
- Changed ExcludeArch to proper Fedora versions
- Builds coq subpackage exactly when Coq can be built, thus making
build independent of whether Coq can be built
- define -> global
- Fixed accidental use of in tar ocamlgraph instead of one that is
separately packaged
Index: import.log
===================================================================
RCS file: /cvs/pkgs/rpms/why/devel/import.log,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -p -r1.2 -r1.3
--- import.log 24 Dec 2008 16:37:05 -0000 1.2
+++ import.log 8 Aug 2009 02:35:30 -0000 1.3
@@ -1,2 +1,3 @@
why-2_14-2_fc9:HEAD:why-2.14-2.fc9.src.rpm:1217954050
why-2_17-1_fc11:HEAD:why-2.17-1.fc11.src.rpm:1230136029
+why-2_17-4_fc10:HEAD:why-2.17-4.fc10.src.rpm:1249698515
Index: why.spec
===================================================================
RCS file: /cvs/pkgs/rpms/why/devel/why.spec,v
retrieving revision 1.4
retrieving revision 1.5
diff -u -p -r1.4 -r1.5
--- why.spec 27 Jul 2009 07:15:16 -0000 1.4
+++ why.spec 8 Aug 2009 02:35:30 -0000 1.5
@@ -1,36 +1,37 @@
-Name: why
-Version: 2.17
-Release: 3%{?dist}
-Summary: Why software verification platform
-
-Group: Applications/Engineering
-License: GPLv2
-URL: http://why.lri.fr/
-Source0: http://why.lri.fr/download/why-%{version}.tar.gz
-Source1: README.why-gwhy.Fedora
-Source2: README.why-coq.Fedora
-Source3: README.why
-Source4: gwhy.desktop
-Source5: gwhy-icon.png
-Source6: min.mlw
-Source7: min_why.why.result
-Source8: http://caduceus.lri.fr/manual/caduceus.ps
-Source9: http://gforge.inria.fr/docman/view.php/999/5097/krakatoa.pdf
-Patch0: gwhy-%{version}.patch
-Patch1: why-%{version}-Makefile.in.patch
-Patch2: why-config.patch
-BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
-BuildRequires: ocaml >= 3.09, ocaml-camlp4-devel, gtk2-devel, ocaml-lablgtk-devel, desktop-file-utils, dos2unix, prelink, coq
-
-%if 0%{?fedora} < 9
-# There's no ocaml for ppc64 in Fedora <= 8
-ExcludeArch: ppc64
+Name: why
+Version: 2.17
+Release: 4%{?dist}
+Summary: Why software verification platform
+
+Group: Applications/Engineering
+License: GPLv2
+URL: http://why.lri.fr/
+Source0: http://why.lri.fr/download/why-%{version}.tar.gz
+Source1: README.why-gwhy.Fedora
+Source2: README.why-coq.Fedora
+Source3: README.why
+Source4: gwhy.desktop
+Source5: gwhy-icon.png
+Source6: min.mlw
+Source7: min_why.why.result
+Source8: http://caduceus.lri.fr/manual/caduceus.ps
+Source9: http://gforge.inria.fr/docman/view.php/999/5097/krakatoa.pdf
+Patch0: gwhy-%{version}.patch
+Patch1: why-%{version}-Makefile.in.patch
+Patch2: why-config.patch
+BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
+BuildRequires: ocaml >= 3.09, ocaml-camlp4-devel, gtk2-devel, ocaml-lablgtk-devel, desktop-file-utils, dos2unix, prelink
+BuildRequires: ocaml-ocamlgraph
+
+%if 0%{?fedora} >= 11
+# Doesn't seem to build on ppc64 for Fedora >= 11
+# bz: 516317
+ExcludeArch: ppc64
%endif
-%if 0%{?fedora} == 11
-# Encountering an odd ocaml ppc64 bug in F11 and don't want to stall the other platforms
-# bz:
-ExcludeArch: ppc64
+# No coq on ppc64 (any Fedora version) at the moment
+%ifnarch ppc64
+%global has_coq 1
%endif
%description
@@ -51,9 +52,9 @@ Zenon is packaged for Fedora) so that th
proven, resulting in a proof of program correctness.
%package gwhy
-Group: Applications/Engineering
-Summary: IDE for Why software verification platform
-Requires: why = %{version}, zenity
+Group: Applications/Engineering
+Summary: IDE for Why software verification platform
+Requires: why = %{version}, zenity
%description gwhy
Gwhy is an optional graphical user interface for the Why software
@@ -62,15 +63,21 @@ assertions that need to be proven to dif
providing an interface to do this and also supports inspection of why
input files.
+# No Coq for ppc64 -> certain subpackages can't be built, but main why can be
+%if 0%{?has_coq} == 1
+
%package coq
-Group: Applications/Engineering
-Summary: Libraries for interfacing Coq with Why
-Requires: why = %{version}
+Group: Applications/Engineering
+Summary: Libraries for interfacing Coq with Why
+Requires: why = %{version}
+BuildRequires: coq
%description coq
This package contains a set of routines that assist in the
manipulation of why Coq-formatted output within Coq.
+%endif
+
%prep
%setup -q
@@ -93,35 +100,35 @@ manipulation of why Coq-formatted output
cp %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 .
%build
-%define opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
+%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
# Native ocaml builds do not seem to work on ppc64 (many packages have
# this problem)
%ifarch ppc64
-%define opt 0
+%global opt 0
%endif
# If not building opt, disable the debug info creation as this would otherwise destroy the bytecode executables
# If we have opt, as this has a dependency on ocaml, we should have ocamlopt.opt
%if ! %{opt}
-%define __os_install_post /usr/lib/rpm/brp-compress %{nil}
-%define _enable_debug_package 0
-%define debug_package %{nil}
-%define opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
+%global __os_install_post /usr/lib/rpm/brp-compress %{nil}
+%global _enable_debug_package 0
+%global debug_package %{nil}
+%global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
%else
-%define opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
+%global opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
%endif
# We actually want to install library files into a non /usr/lib
# directory as they aren't architecture dependent
-./configure --prefix=%{_prefix} --bindir=%{_bindir} --libdir=%{_datadir} --mandir=%{_mandir}
+./configure --prefix=%{_prefix} --bindir=%{_bindir} --libdir=%{_datadir} --mandir=%{_mandir} %{!?has_coq: COQC=no}
make %{opt_option}
%check
%if %opt
-%define why bin/why.opt
+%global why bin/why.opt
%else
-%define why bin/why.byte
+%global why bin/why.byte
%endif
export WHYLIB=lib
%why --why --output min min.mlw
@@ -130,11 +137,17 @@ diff min_why.why min_why.why.result > /d
%install
rm -rf %{buildroot}
-make %{opt_option} BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_datadir} MANDIR=%{buildroot}%{_mandir} COQLIB=%{buildroot}%{_datadir}/coq install
+
+make %{opt_option} BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_datadir} MANDIR=%{buildroot}%{_mandir} %{?has_coq: COQLIB=%{buildroot}%{_datadir}/coq} install
+
+# Fix a small bug in their Makefile: if no Coq, NO .v files should be installed
+%if 0%{?has_coq} != 1
+rm -f `find %{buildroot}%{_datadir}/coq -name '*.v'`
+%endif
# Install desktop icon and menu entry
-%define why_data_dir %{_datadir}/why
+%global why_data_dir %{_datadir}/why
%if %(test -d %{buildroot}%{why_data_dir} && echo 1 || echo 0) != 1
mkdir -p %{buildroot}%{why_data_dir}
%endif
@@ -142,17 +155,22 @@ cp gwhy-icon.png %{buildroot}%{why_data_
sed -i -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' gwhy.desktop
-desktop-file-install --vendor="fedora" \
---dir=%{buildroot}%{_datadir}/applications \
+desktop-file-install --vendor="fedora" \
+--dir=%{buildroot}%{_datadir}/applications \
gwhy.desktop
-%define why_doc_dir %{_defaultdocdir}/%{name}-%{version}/
-%define why_examples_dir %{why_doc_dir}examples/
+%global why_doc_dir %{_defaultdocdir}/%{name}-%{version}/
+%global why_examples_dir %{why_doc_dir}examples/
+
+%global fix_encoding() dos2unix %1; mv %1 %1.old; \
+ iconv -f ISO-8859-1 -t UTF-8 < %1.old > %1; rm %1.old \
+ %{nil}
# Fix up documentation and examples
mkdir -p %{buildroot}%{why_examples_dir}mlw/
mkdir -p %{buildroot}%{why_examples_dir}c/
cp -p doc/manual.ps %{buildroot}%{why_doc_dir}why-manual.ps
+%fix_encoding COPYING
cp -p caduceus.ps krakatoa.pdf README.why COPYING LICENSE %{buildroot}%{why_doc_dir}
# Copy in the example files after converting to proper UTF-8, fix line
@@ -162,7 +180,7 @@ for d in `find -mindepth 1 -maxdepth 1 -
mkdir -p %{buildroot}%{why_examples_dir}mlw/$d
done
for f in `find -regex '.*\(\.mlw\|\.why\)' | egrep -v '_inv|_coq|_why'`; do
-dos2unix $f; mv $f $f.old; iconv -f ISO-8859-1 -t UTF-8 < $f.old > $f; rm $f.old
+%fix_encoding $f
cp -p $f %{buildroot}%{why_examples_dir}mlw/$f
done
@@ -171,7 +189,7 @@ for d in `find -mindepth 1 -maxdepth 1 -
mkdir -p %{buildroot}%{why_examples_dir}c/$d
done
for f in `find -regex '.*\.c'`; do
-dos2unix $f; mv $f $f.old; iconv -f ISO-8859-1 -t UTF-8 < $f.old > $f; rm $f.old
+%fix_encoding $f
cp -p $f %{buildroot}%{why_examples_dir}c/$f
done
@@ -209,6 +227,8 @@ rm -rf %{buildroot}
%{why_data_dir}/gwhy-icon.png
%{_datadir}/applications/fedora-gwhy.desktop
+%if 0%{?has_coq} == 1
+
%files coq
%defattr(-,root,root,-)
%dir %{_datadir}/coq
@@ -224,7 +244,19 @@ rm -rf %{buildroot}
%{_datadir}/coq/jessie_why.v*
%doc README.why-coq.Fedora
+%endif
+
%changelog
+* Fri Aug 07 2009 Alan Dunn <amdunn at gmail.com> - 2.17-4
+- Removed now irrelevant check for no OCaml in Fedora < 9 (those
+ distributions are EOL)
+- Changed ExcludeArch to proper Fedora versions
+- Builds coq subpackage exactly when Coq can be built, thus making
+ build independent of whether Coq can be built
+- define -> global
+- Fixed accidental use of in tar ocamlgraph instead of one that is
+ separately packaged
+
* Mon Jul 27 2009 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 2.17-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild
More information about the fedora-extras-commits
mailing list