rpms/why
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
why/why.spec
Jerry James 5e6572ac93 Rebuild for why3 0.87.2.
2016-09-02 09:20:42 -06:00

632 lines
22 KiB
RPMSpec
Raw Permalink Blame History

# Whether PVS is available
%ifarch %{ix86} x86_64 ppc sparcv9
%global has_pvs 1
%else
%global has_pvs 0
%endif
# What kind of ocaml build to do
%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
Name: why
Version: 2.35
Release: 18%{?dist}
Summary: Software verification platform
License: LGPLv2 with exceptions
URL: http://why.lri.fr/
Source0: http://why.lri.fr/download/%{name}-%{version}.tar.gz
Source1: http://krakatoa.lri.fr/manual/krakatoa.pdf
Source2: README.why-coq.Fedora
Source3: README.why
Source4: jessie.desktop
Source5: jessie.appdata.xml
Source6: div.pvs
Source7: rem.pvs
Source8: patch_jessie_pvs
# Created with gimp from official upstream icon
Source9: %{name}-icons.tar.xz
# This patch makes a Fedora-specific fix to eliminate checking for the
# location of Coq - since we're using the coq package, we know where
# it is and their checking causes the rpm building to fail.
# It also makes a fix necessary to correctly build the bytecode only
# version of why by building the make_float_model tool correctly in
# this case.
Patch0: %{name}-2.35-Makefile.in.patch
# Adapt to ocamlgraph 1.8.6
Patch1: %{name}-ocamlgraph186.patch
# Adapt to Frama-C Aluminium
Patch2: %{name}-frama-c-aluminium.patch
BuildRequires: auto-destdir
BuildRequires: desktop-file-utils
BuildRequires: emacs xemacs xemacs-packages-extra
BuildRequires: frama-c
BuildRequires: gappalib-coq
BuildRequires: ocaml
BuildRequires: ocaml-apron-devel
BuildRequires: ocaml-camlp4-devel
BuildRequires: ocaml-findlib
BuildRequires: ocaml-mlgmpidl-devel
BuildRequires: ocaml-ocamldoc
BuildRequires: ocaml-ocamlgraph-devel
BuildRequires: why3
BuildRequires: coq
%if %{has_pvs}
BuildRequires: pvs
%endif
Requires: hicolor-icon-theme
Requires: emacs-filesystem
Requires: xemacs-filesystem
# Filter out bogus requires
%global __requires_exclude ocaml\\\((Ast|Cc|Env|Error|Jc_ast|Jc_env|Loc|Logic|Logic_decl|Misc|Ptree|Types)\\\)
%description
Why is a software verification platform that applies formal proving
tools to annotated programs. It is currently capable of analysis of C
(through "Frama-C"), Java (through the included tool "Krakatoa"), and
potentially ML programs with some modification into Why's own ML-like
language. Furthermore, Why is capable of analysis of any program that
is mapped onto its own internal language. It uses a weakest
precondition involving calculus to generate potential theorems necessary
for the proof of a program's correctness. It translates these theorems
into formats that can be used by external proof assistants (without any
extra work Coq, PVS, HOL Light, and Mizar are supported - having one is
recommended and both Coq and PVS are packaged for Fedora) and automated
theorem provers (without any extra work Simplify, Alt-Ergo, Yices, Z3,
CVC3, and Zenon are supported and Alt-Ergo, Z3, and Zenon are packaged
for Fedora) so that these results can be externally proven, resulting in
a proof of program correctness.
Note: Each user account must be set up by running "why-config" at the
command line (to set up a configuration file).
%package jessie
Summary: Interface between why and frama-c
Requires: %{name}%{?_isa} = %{version}-%{release}
Requires: frama-c
%description jessie
The Jessie plugin, an interface between why and frama-c. Invoke it with:
frama-c -jessie FILE.c
%package coq
Summary: Libraries for interfacing Coq with Why
Requires: %{name}%{?_isa} = %{version}-%{release}
Requires: gappalib-coq
%description coq
This package contains a set of routines that assist in the manipulation
of why Coq-formatted output within Coq.
%if %{has_pvs}
# Why's integration with PVS depends on the NASA Langley PVS Libraries,
# which have no license information. This provides an alternative:
%package pvs-support
Summary: Complete Why software verification platform suite
Requires: %{name}%{?_isa} = %{version}-%{release}
Requires: pvs
%description pvs-support
This package provides support definitions so that the Why software
verification platform suite can invoke PVS without licensing issues.
%endif
%package all
Summary: Complete Why software verification platform suite
Requires: why%{?_isa} = %{version}-%{release}
Requires: why-jessie%{?_isa} = %{version}-%{release}
Requires: why-coq%{?_isa} = %{version}-%{release}
%if %{has_pvs}
Requires: why-pvs-support%{?_isa} = %{version}-%{release}
%endif
Requires: alt-ergo gappalib-coq z3 zenon
%description all
This package provides a complete software verification platform suite
based on Why, including various automated and interactive provers.
%prep
%setup -q
%setup -q -T -D -a 9
%patch0
%patch1
%patch2
cp -p %SOURCE2 ./
# Link with Fedora LDFLAGS
for flag in $RPM_LD_FLAGS; do
sed -e "\%^bin/jessie\.opt%,\%^bin/jessie\.byte%s|-o|-ccopt $flag &|" \
-e "/gtkThread\.cmx/s|-o|-ccopt $flag &|" \
-i Makefile.in
done
%define fix_encoding() \
iconv -f %2 -t %3 %1 > %1.utf8; \
touch -r %1 %1.utf8; \
mv -f %1.utf8 %1;
# Fix encodings
for f in CHANGES COPYING examples/bresenham/bresenham.mlw \
examples/bresenham/bresenham_coq.mlw examples/bresenham/bresenham_inv.mlw \
examples/edit-distance/distance.mlw examples/heapsort/downheap.mlw \
examples/heapsort/heapsort.mlw examples/heapsort/Inftree.v \
examples/kmp/kmp.mlw examples/kmp/Lex.v examples/kmp/Match.v \
examples/kmp/Next.v examples/misc/matrix.why examples/misc/matrix_why.v \
examples/quicksort/partition.mlw examples/quicksort/Partition.v \
examples/quicksort/quicksort.mlw examples/quicksort/Quicksort.v \
examples/sqrt/sqrt.mlw examples/string-matching/Match.v; do
%fix_encoding $f ISO-8859-1 UTF-8
done
# Fix line endings
for f in examples-c/tutorial/average.c examples-c/tutorial/purse.c \
examples-c/ukkonen/main.c examples-c/ukkonen/ukkonen.c; do
sed "s/\r//" $f > $f.new
touch -r $f $f.new
mv -f $f.new $f
done
# APRON support: add a missing rpath and adapt to newer versions of apron
sed -e "s|-lpolkaMPQ_caml|-Wl,-rpath,%{_libdir}/ocaml/apron|" \
-e "s|box\.cmxa polka.cmxa|boxMPQ.cmxa polkaMPQ.cmxa|" \
-i configure
# Enable debuginfo
sed -i 's,@STRIP@,/usr/bin/true,;s,-dtypes [^-],-g &,' Makefile.in
sed -ri 's,ocaml(c|opt),& -g,' atp/Makefile
# Command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl:
sed -e 's/command = "pvs"/command = "pvs-sbcl"/' \
-e 's/PVS, (pvs, \["pvs"\]);/PVS, (pvs, ["pvs-sbcl" ; "pvs"]);/' \
-i tools/dpConfig.ml
sed -i 's/pvs/pvs-sbcl/' configure
# Allow building with why3 0.87.2, Frama-C Aluminium, and flocq 2.5.1
sed -e 's/0\.85|0\.86/&|0.87.2/' \
-e 's/Sodium-20150201/Aluminium-20160501/;s/Sodium/Aluminium/' \
-e 's/FRAMAC -version.*`/FRAMAC -version`/' \
-e 's/Import Flocq_version/Import Flocq.Flocq_version/' \
-i configure
# Fix detection of why3
sed -i '/WHY3/s/\\+\\) \.\*/*\\).*/' configure
%build
%if ! %{opt}
%global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
%else
%global opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
%endif
%configure --enable-apron --enable-verbosemake
make %{opt_option}
%install
# Avoid a bug in PVS batch mode when using emacs
make install DESTDIR=%{buildroot} %{opt_option} \
PVSLIB=%{buildroot}%{_libdir}/pvs/lib PVSEMACS=xemacs
# Fix permissions
chmod a-x %{buildroot}%{_libdir}/frama-c/plugins/META.frama-c-jessie
chmod a-x %{buildroot}%{_libdir}/frama-c/plugins/Jessie.cmi
chmod a-x %{buildroot}%{_libdir}/frama-c/plugins/top/Jessie.cm{a,o,x}
# If no PVS, no .pvs files should be installed
%if ! %{has_pvs}
rm -fr %{buildroot}%{_libdir}/pvs
%endif
# Install desktop file
desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE4}
# Install AppData files
mkdir -p %{buildroot}%{_datadir}/appdata
install -pm 644 %{SOURCE5} %{buildroot}%{_datadir}/appdata
# Install the icons
mkdir -p %{buildroot}%{_datadir}/icons
cp -a icons %{buildroot}%{_datadir}/icons/hicolor
%if %{has_pvs}
# Get rid of a BUILDROOT reference in a log file (fails QA_CHECK_RPATHS)
sed -i "s|%{buildroot}||" %{buildroot}%{_libdir}/pvs/lib/why/top.out
mkdir -p %{buildroot}%{_libdir}/pvs/lib/ints/
cp -p %{SOURCE6} %{SOURCE7} %{buildroot}%{_libdir}/pvs/lib/ints/
cp -p %{SOURCE8} %{buildroot}%{_bindir}/
%endif
%global why_doc_dir %{?_pkgdocdir}%{!?_pkgdocdir:%{_docdir}/%{name}-%{version}}
%global why_examples_dir %{why_doc_dir}/examples/
# 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
cp -p %{SOURCE1} %{SOURCE3} CHANGES README Version %{buildroot}%{why_doc_dir}
# Copy in the example files, leaving behind all generated files
cd examples
for d in `find -mindepth 1 -maxdepth 1 -type d`; do
mkdir -p %{buildroot}%{why_examples_dir}mlw/$d
done
for f in `find -regex '.*\(\.mlw\|\.why\)' | grep -E -v '_inv|_coq|_why'`; do
cp -p $f %{buildroot}%{why_examples_dir}mlw/$f
done
cd ../examples-c
for d in `find -mindepth 1 -maxdepth 1 -type d`; do
mkdir -p %{buildroot}%{why_examples_dir}c/$d
done
for f in `find -regex '.*\.c'`; do
cp -p $f %{buildroot}%{why_examples_dir}c/$f
done
# Remove a stray coq file (already installed in the right place)
rm -f %{buildroot}%{_libdir}/coq/jessie_why.v
# Move the Emacs support file to the right places and byte compile it
cd ..
mkdir -p %{buildroot}%{_emacs_sitelispdir}
cp -p lib/emacs/why.el %{buildroot}%{_emacs_sitelispdir}
mkdir -p %{buildroot}%{_xemacs_sitelispdir}
cp -p lib/emacs/why.el %{buildroot}%{_xemacs_sitelispdir}
cd %{buildroot}%{_emacs_sitelispdir}
%{_emacs_bytecompile} why.el
cd %{buildroot}%{_xemacs_sitelispdir}
%{_xemacs_bytecompile} why.el
rm -fr %{buildroot}%{_libdir}/why/emacs
%check
make check
%post jessie
update-desktop-database &> /dev/null || :
touch --no-create %{_datadir}/icons/hicolor &>/dev/null
gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
%postun jessie
update-desktop-database &> /dev/null || :
touch --no-create %{_datadir}/icons/hicolor &>/dev/null
gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
%files
%license COPYING LICENSE
%{_bindir}/*
%{_libdir}/why/
%{_datadir}/icons/hicolor/*/apps/%{name}.png
%{_emacs_sitelispdir}/why.el*
%{_xemacs_sitelispdir}/why.el*
%{why_doc_dir}/
# This last example is really an example only for Coq - only .v files
%exclude %{why_examples_dir}mlw/string-matching/
# why-jessie
%exclude %{_bindir}/jessie
# why-pvs-support:
%exclude %{_bindir}/patch_jessie_pvs
%files jessie
%{_bindir}/jessie
%{_libdir}/frama-c/plugins/Jessie.cmi
%{_libdir}/frama-c/plugins/META.frama-c-jessie
%{_libdir}/frama-c/plugins/top/Jessie.*
%{_datadir}/appdata/jessie.appdata.xml
%{_datadir}/applications/jessie.desktop
%files coq
%doc README.why-coq.Fedora
%{_libdir}/coq/user-contrib/Why/
%if %{has_pvs}
%files pvs-support
%{_libdir}/pvs/lib/*
%{_bindir}/patch_jessie_pvs
%endif
# "why-all" is a meta-package; it just depends on other packages, so that
# it's easier to install a useful suite of tools. Thus, it has no files:
%files all
%changelog
* Fri Sep 2 2016 Jerry James <loganjerry@gmail.com> - 2.35-18
- Rebuild for why3 0.87.2
* Fri Jul 22 2016 Jerry James <loganjerry@gmail.com> - 2.35-17
- Rebuild for apron 0.9.11 and gappalib-coq 1.3.0
* Wed Jul 13 2016 Jerry James <loganjerry@gmail.com> - 2.35-16
- Rebuild for coq 8.5pl2
* Wed Jun 1 2016 Jerry James <loganjerry@gmail.com> - 2.35-15
- Rebuild for why3 0.87.1 and Frama-C Aluminium
* Fri Apr 22 2016 Jerry James <loganjerry@gmail.com> - 2.35-14
- Rebuild for coq 8.5pl1
* Sat Apr 16 2016 Jerry James <loganjerry@gmail.com> - 2.35-13
- Rebuild for ocaml-ocamlgraph 1.8.7
* Fri Mar 18 2016 Jerry James <loganjerry@gmail.com> - 2.35-12
- Rebuild for why3 0.87.0
* Fri Feb 12 2016 Jerry James <loganjerry@gmail.com> - 2.35-11
- Rebuild for coq 8.5, flocq 2.5.1, gappalib-coq 1.2.1, why3 0.86.3, and
Frama-C Magnesium
- Use camlp4 in preference to camlp5
- Drop cvc3 support
- Update appdata for latest specification
* Fri Feb 05 2016 Fedora Release Engineering <releng@fedoraproject.org> - 2.35-10
- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
* Wed Oct 14 2015 Jerry James <loganjerry@gmail.com> - 2.35-9
- Rebuild for flocq 2.5.0, gappalib-coq 1.2.0, and why3 0.86.2
* Thu Jul 30 2015 Richard W.M. Jones <rjones@redhat.com> - 2.35-8
- OCaml 4.02.3 rebuild.
* Mon Jun 22 2015 Jerry James <loganjerry@gmail.com> - 2.35-7
- Rebuild for why3 0.86.1
* Fri Jun 19 2015 Richard W.M. Jones <rjones@redhat.com> - 2.35-6
- Rebuild for ocaml-4.02.2.
* Fri Jun 19 2015 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.35-5
- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild
* Sat May 16 2015 Jerry James <loganjerry@gmail.com> - 2.35-4
- Rebuild for why3 0.86
* Mon Apr 13 2015 Jerry James <loganjerry@gmail.com> - 2.35-3
- Rebuild for coq 8.4pl6
* Wed Apr 1 2015 Jerry James <loganjerry@gmail.com> - 2.35-2
- Adjust requires filter
* Tue Mar 31 2015 Jerry James <loganjerry@gmail.com> - 2.35-1
- New upstream release
- Drop upstreamed -flocq24 and -frama-c-sodium patches
- Drop all gwhy-related sources, as gwhy has been retired
- Merge (X)Emacs files into the main package due to change in policy
* Thu Mar 19 2015 Jerry James <loganjerry@gmail.com> - 2.34-18
- Rebuild for Frama-C Sodium
- Add -ocamlgraph186 patch to adapt to ocamlgraph 1.8.6
- Add -frama-c-sodium patch to adapt to Frama-C Sodium
* Thu Feb 19 2015 Richard W.M. Jones <rjones@redhat.com> - 2.34-17
- ocaml-4.02.1 rebuild.
* Sat Nov 15 2014 Jerry James <loganjerry@gmail.com> - 2.34-16
- Fix gwhy-2.33.patch (bz 1164470)
* Thu Nov 13 2014 Richard W.M. Jones <rjones@redhat.com> - 2.34-15
- Bump and rebuild for broken dependencies.
* Thu Oct 30 2014 Jerry James <loganjerry@gmail.com> - 2.34-14
- Rebuild for coq 8.4pl5
* Thu Sep 18 2014 Jerry James <loganjerry@gmail.com> - 2.34-13
- Rebuild for why3 0.85
* Mon Sep 8 2014 Jerry James <loganjerry@gmail.com> - 2.34-12
- Rebuild for fixed frama-c
- Fix license handling
* Tue Sep 2 2014 Jerry James <loganjerry@gmail.com> - 2.34-11
- Rebuild for the final ocaml 4.02.0 release
* Mon Aug 25 2014 Jerry James <loganjerry@gmail.com> - 2.34-10
- ocaml-4.02.0+rc1 rebuild.
* Mon Aug 18 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.34-9
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
* Mon Aug 4 2014 Jerry James <loganjerry@gmail.com> - 2.34-8
- OCaml 4.02.0 beta rebuild
- BR emacs instead of emacs-nox, which no longer exists
* Tue Jun 24 2014 Jerry James <loganjerry@gmail.com> - 2.34-7
- Omit "-z now" when building with relro (bz 1105265)
- Resolve a conflict between Frama-C and why modules both named "Project"
* Sun Jun 08 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.34-6
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
* Tue May 13 2014 Jerry James <loganjerry@gmail.com> - 2.34-5
- Rebuild for coq 8.4pl4
* Mon Apr 21 2014 Jerry James <loganjerry@gmail.com> - 2.34-4
- Rebuild for ocamlgraph 1.8.5 and flocq 2.3.0
- Drop has_coq macro, since coq is now universally available
- Add -flocq23 patch to adapt to flocq 2.3.0
* Tue Apr 15 2014 Richard W.M. Jones <rjones@redhat.com> - 2.34-3
- Remove ocaml_arches macro (RHBZ#1087794).
* Mon Mar 24 2014 Jerry James <loganjerry@gmail.com> - 2.34-2
- Remove dropped patches
- Add icons
- Fix the desktop icon entries
* Tue Mar 18 2014 Jerry James <loganjerry@gmail.com> - 2.34-1
- New upstream release
- Drop upstreamed -hashtbl, -flocq, and -or patches
- Add ocaml-findlib BR
* Wed Feb 26 2014 Jerry James <loganjerry@gmail.com> - 2.33-6
- Rebuild for ocamlgraph 1.8.4
- Update desktop files
- Add AppData files for gwhy and jessie
* Tue Sep 17 2013 Jerry James <loganjerry@gmail.com> - 2.33-5
- Rebuild for OCaml 4.01.0
- Enable debuginfo
- Add -or patch to fix warnings, since warnings are errors
* Sat Jul 27 2013 Ville Skyttä <ville.skytta@iki.fi> - 2.33-4
- Install docs to %%{_pkgdocdir} where available.
* Fri Jun 21 2013 Jerry James <loganjerry@gmail.com> - 2.33-3
- Rebuild for frama-c Fluorine 20130601
* Thu May 23 2013 Jerry James <loganjerry@gmail.com> - 2.33-2
- Rebuild for new frama-c and why3 builds
* Tue May 14 2013 Jerry James <loganjerry@gmail.com> - 2.33-1
- New upstream release
- Drop upstreamed -warning, -coq84, and -ocaml4 patches
- Add -hashtbl patch
- Enable Jessie plugin again
* Sat Feb 09 2013 Parag Nemade <paragn AT fedoraproject DOT org> - 2.31-7
- Remove vendor tag from desktop file as per https://fedorahosted.org/fesco/ticket/1077
* Mon Jan 14 2013 Jerry James <loganjerry@gmail.com> - 2.31-6
- Rebuild for alt-ergo 0.95
* Mon Jan 7 2013 Jerry James <loganjerry@gmail.com> - 2.31-5
- Rebuild for coq 8.4pl1
* Fri Oct 19 2012 Jerry James <loganjerry@gmail.com> - 2.31-4
- Rebuild for OCaml 4.00.1 and frama-c Oxygen
- Recripple the Jessie plugin until it works with frama-c Oxygen
* Tue Sep 11 2012 Jerry James <loganjerry@gmail.com> - 2.31-3
- Rebuild for new frama-c build with altered API.
* Mon Aug 27 2012 Jerry James <loganjerry@gmail.com> - 2.31-2
- Frama-c is fixed; rebuild with the Jessie plugin enabled and functioning
* Thu Aug 23 2012 Jerry James <loganjerry@gmail.com> - 2.31-1
- New upstream version
- Drop upstreamed patches
- Add ocaml-mlgmpidl-devel and why3 BRs
- Add -warning, -ocaml4, and -coq84 patches to fix the build
- Cripple the Jessie plugin until problems with frama-c and hashtables are fixed
* Mon Jul 30 2012 Richard W.M. Jones <rjones@redhat.com> - 2.30-7
- Rebuild for OCaml 4.00.0 official.
* Sun Jul 22 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.30-6
- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
* Wed Jan 11 2012 Jerry James <loganjerry@gmail.com> - 2.30-5
- Patch to work with flocq 2.0.0
* Tue Dec 27 2011 Jerry James <loganjerry@gmail.com> - 2.30-4
- Rebuild for coq 8.3pl3
* Tue Dec 6 2011 Jerry James <loganjerry@gmail.com> - 2.30-3
- Update alt_ergo and yices "okay" version numbers
* Wed Nov 23 2011 Jerry James <loganjerry@gmail.com> - 2.30-2
- Rebuild with APRON and gappalib-coq support
* Fri Oct 28 2011 Jerry James <loganjerry@gmail.com> - 2.30-1
- New upstream release
* Thu Jul 14 2011 Jerry James <loganjerry@gmail.com> - 2.29-2
- Fix broken conditionals
* Mon Jul 11 2011 Jerry James <loganjerry@gmail.com> - 2.29-1
- New upstream release (fixes FTBFS: bz 715902)
- Remove unnecessary spec file elements (BuildRoot, etc.)
- Update approach to filtering provides and requires
- Add has_pvs analogously to has_coq, and simplify macro usage
- Add (X)Emacs support packages
- New subpackage for the jessie plugin to avoid unowned directories and
permit a direct dependency on frama-c
- Prepare for the eventual availability of APRON
* Thu Apr 14 2011 Karsten Hopp <karsten@redhat.com> 2.28-2.2
- add ppc to excludearch, too. No pvs-sbcl available there
* Wed Apr 13 2011 Karsten Hopp <karsten@redhat.com> 2.28-2.1
- add ppc64 to excludearch, no sbcl available there
* Mon Feb 07 2011 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.28-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
* Fri Jan 21 2011 Richard W.M. Jones <rjones@gmail.com> - 2.28-1
- Since 2.26 FTBFS, try latest upstream (2.28).
- Rebase Makefile.in patch.
- Fix(?) test result.
- No libdir/frama-c directory is created any more.
* Fri Jan 21 2011 Richard W.M. Jones <rjones@gmail.com> - 2.26-2
- Bump and rebuild for OCaml 3.12.
* Sat Oct 09 2010 David A. Wheeler + Mark Rader <dwheeler@dwheeler.com> - 2.26-1
- Upgrade to upstream version 2.26 (inc. update of krakatoa.pdf)
- Integrated with Frama-C and PVS (as pvs-sbcl)
* Mon Jan 11 2010 Richard W.M. Jones <rjones@gmail.com> - 2.23-2
- Rebuild to fix dependencies.
* Fri Jan 08 2010 Alan Dunn <amdunn@gmail.com> - 2.23-1
- Upgrade to upstream version 2.23
- Move execstack fixing to spec file from patch
- Moved patch descriptions to initial patch declaration as in examples
in Fedora documentation
- New Caduceus, Krakatoa documentation
- Update test result from small test min.mlw
- Added CVC3 interfacing capabilities
- Removed patch for gwhy configuration, as there is a new mechanism for this
* Tue Sep 22 2009 Dennis Gilmore <dennis@ausil.us> - 2.17-5
- Exclude sparc64 s390 s390x there is no ocaml there
* Fri Aug 07 2009 Alan Dunn <amdunn@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@lists.fedoraproject.org> - 2.17-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild
* Wed Feb 25 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.17-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild
* Wed Dec 24 2008 Alan Dunn <amdunn@gmail.com> 2.17-1
- Upgrade to version 2.17 (bz: 477790)
- Add ownership of two directories common with Coq, but neither program requires the other (bz: 474016)
- Minor filename change in 2.17 (GPL -> LICENSE)
- Added back Coq .v files to match policy for Coq
- Changed directory structure re: jessie and krakatoa to match new structure in 2.17
- Minor changes to patches to ensure they still work in 2.17
- Corrected package location gwhy-icon.png (should only be in gwhy)
* Tue Aug 5 2008 Alan Dunn <amdunn@gmail.com> 2.14-2.1
- ExcludeArch ppc64 on Fedora 8 due to no ocaml.
* Fri Aug 1 2008 Alan Dunn <amdunn@gmail.com> 2.14-2
- Fixed minor issues in response to package review:
- Inclusion of COPYING, GPL license-related files
- Added config.mll patch to make default config file created nicer
- Changes subpackage dependencies to be fully versioned.
- Makes during build allowed to be noisy (allowed to print).
* Wed Jul 30 2008 Alan Dunn <amdunn@gmail.com> 2.14-1
- Changed to new version of why, removed previous why-cpulimit name
change, zenon output format patches as the issues were fixed in
why 2.14.
- Moved doc subpackage back into main package.
- Added example files to documentation subpackage.
- Added check section with test on small why file.
- Reformatted some macro names for greater readability.
* Thu Jul 24 2008 Alan Dunn <amdunn@gmail.com> 2.13-2
- Added several patches: fixed Zenon output, completed fix of rename
of cpulimit -> why-cpulimit.
* Wed Jul 23 2008 Alan Dunn <amdunn@gmail.com> 2.13-1
- Initial Fedora RPM version.
Reference in a new issue View git blame Copy permalink