|
|
|
|
@ -1,585 +0,0 @@
|
|
|
|
|
# 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.39
|
|
|
|
|
Release: 2%{?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
|
|
|
|
|
|
|
|
|
|
BuildRequires: auto-destdir
|
|
|
|
|
BuildRequires: desktop-file-utils
|
|
|
|
|
BuildRequires: 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: ocaml-zarith-devel
|
|
|
|
|
BuildRequires: why3
|
|
|
|
|
BuildRequires: coq
|
|
|
|
|
%if %{has_pvs}
|
|
|
|
|
BuildRequires: pvs
|
|
|
|
|
%endif
|
|
|
|
|
|
|
|
|
|
Requires: gappalib-coq
|
|
|
|
|
Requires: hicolor-icon-theme
|
|
|
|
|
Requires: emacs-filesystem
|
|
|
|
|
|
|
|
|
|
# This can be removed once Fedora 25 reaches EOL
|
|
|
|
|
Obsoletes: %{name}-coq < 2.36-1
|
|
|
|
|
Provides: %{name}-coq = %{version}-%{release}
|
|
|
|
|
|
|
|
|
|
# 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
|
|
|
|
|
|
|
|
|
|
%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}
|
|
|
|
|
%if %{has_pvs}
|
|
|
|
|
Requires: why-pvs-support%{?_isa} = %{version}-%{release}
|
|
|
|
|
%endif
|
|
|
|
|
Requires: alt-ergo 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
|
|
|
|
|
|
|
|
|
|
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; do
|
|
|
|
|
%fix_encoding $f ISO-8859-1 UTF-8
|
|
|
|
|
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 octMPQ.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 -i 's/pvs/pvs-sbcl/' configure
|
|
|
|
|
|
|
|
|
|
# Allow building with OCaml 4.05
|
|
|
|
|
sed -i 's/4\.04\.\*/4.04.*|4.05.*/' configure
|
|
|
|
|
|
|
|
|
|
%build
|
|
|
|
|
%if ! %{opt}
|
|
|
|
|
%global opt_option OCAMLBEST=byte OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
|
|
|
|
|
%else
|
|
|
|
|
%global opt_option OCAMLBEST=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}}
|
|
|
|
|
|
|
|
|
|
# Fix up documentation and examples
|
|
|
|
|
mkdir -p %{buildroot}%{why_doc_dir}
|
|
|
|
|
cp -p %{SOURCE1} %{SOURCE3} CHANGES README Version %{buildroot}%{why_doc_dir}
|
|
|
|
|
|
|
|
|
|
%check
|
|
|
|
|
make check
|
|
|
|
|
|
|
|
|
|
%post jessie
|
|
|
|
|
touch --no-create %{_datadir}/icons/hicolor &>/dev/null
|
|
|
|
|
gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
|
|
|
|
|
|
|
|
|
|
%postun jessie
|
|
|
|
|
touch --no-create %{_datadir}/icons/hicolor &>/dev/null
|
|
|
|
|
gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
|
|
|
|
|
|
|
|
|
|
%files
|
|
|
|
|
%doc README.why-coq.Fedora
|
|
|
|
|
%license COPYING LICENSE
|
|
|
|
|
%{_bindir}/*
|
|
|
|
|
%{_libdir}/why/
|
|
|
|
|
%{_datadir}/icons/hicolor/*/apps/%{name}.png
|
|
|
|
|
%{why_doc_dir}/
|
|
|
|
|
# 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
|
|
|
|
|
|
|
|
|
|
%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
|
|
|
|
|
* Sat Oct 7 2017 Jerry James <loganjerry@gmail.com> - 2.39-2
|
|
|
|
|
- Rebuild for why3 0.88.0
|
|
|
|
|
|
|
|
|
|
* Thu Sep 7 2017 Jerry James <loganjerry@gmail.com> - 2.39-1
|
|
|
|
|
- New upstream release
|
|
|
|
|
|
|
|
|
|
* Wed Sep 06 2017 Richard W.M. Jones <rjones@redhat.com> - 2.38-6
|
|
|
|
|
- OCaml 4.05.0 rebuild.
|
|
|
|
|
|
|
|
|
|
* Thu Aug 03 2017 Fedora Release Engineering <releng@fedoraproject.org> - 2.38-5
|
|
|
|
|
- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild
|
|
|
|
|
|
|
|
|
|
* Thu Jul 27 2017 Fedora Release Engineering <releng@fedoraproject.org> - 2.38-4
|
|
|
|
|
- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
|
|
|
|
|
|
|
|
|
|
* Sat Jul 01 2017 Richard W.M. Jones <rjones@redhat.com> - 2.38-3
|
|
|
|
|
- Rebuild for OCaml 4.04.2.
|
|
|
|
|
|
|
|
|
|
* Mon May 15 2017 Richard W.M. Jones <rjones@redhat.com> - 2.38-2
|
|
|
|
|
- Rebuild for OCaml 4.04.1.
|
|
|
|
|
|
|
|
|
|
* Fri Mar 24 2017 Jerry James <loganjerry@gmail.com> - 2.38-1
|
|
|
|
|
- New upstream release
|
|
|
|
|
|
|
|
|
|
* Sat Feb 11 2017 Fedora Release Engineering <releng@fedoraproject.org> - 2.36-2
|
|
|
|
|
- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
|
|
|
|
|
|
|
|
|
|
* Thu Jan 12 2017 Jerry James <loganjerry@gmail.com> - 2.36-1
|
|
|
|
|
- New upstream release
|
|
|
|
|
|
|
|
|
|
* Wed Nov 30 2016 Jerry James <loganjerry@gmail.com> - 2.35-23
|
|
|
|
|
- Rebuild for gappalib-coq 1.3.2
|
|
|
|
|
|
|
|
|
|
* Sun Nov 06 2016 Richard W.M. Jones <rjones@redhat.com> - 2.35-21
|
|
|
|
|
- Rebuild for OCaml 4.04.0.
|
|
|
|
|
- Modify configure script to allow building with OCaml 4.04.
|
|
|
|
|
- Modify configure script to use octMPQ library (part of Apron).
|
|
|
|
|
|
|
|
|
|
* Fri Oct 28 2016 Jerry James <loganjerry@gmail.com> - 2.35-20
|
|
|
|
|
- Rebuild for coq 8.5pl3
|
|
|
|
|
- Remove obsolete scriptlets
|
|
|
|
|
|
|
|
|
|
* Thu Sep 29 2016 Jerry James <loganjerry@gmail.com> - 2.35-19
|
|
|
|
|
- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1
|
|
|
|
|
|
|
|
|
|
* 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.
|
