Compare commits
4 commits
| Author | SHA1 | Date | |
|---|---|---|---|
|
c7cd340a99 | ||
|
|
40a810c1c7 | ||
|
|
b0921e1ae7 | ||
|
96ed6c8a3d |
12 changed files with 915 additions and 1 deletions
5
.gitignore
vendored
Normal file
5
.gitignore
vendored
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
/krakatoa.pdf
|
||||
/why-icons.tar.xz
|
||||
/why-2.36.tar.gz
|
||||
/why-2.38.tar.gz
|
||||
/why-2.39.tar.gz
|
||||
8
README.why
Normal file
8
README.why
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
Fedora why package:
|
||||
|
||||
Contains the main why executable and supporting tools.
|
||||
|
||||
Consider visiting the main Why site - http://why.lri.fr - for more
|
||||
documentation. Also, there is more information about the tools
|
||||
Caduceus and Krakatoa at http://caduceus.lri.fr and
|
||||
http://krakatoa.lri.fr respectively.
|
||||
6
README.why-coq.Fedora
Normal file
6
README.why-coq.Fedora
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
Fedora why-coq package:
|
||||
|
||||
Contains libraries for interfacing why with Coq.
|
||||
|
||||
You shouldn't have to do anything extra - you should now just be able
|
||||
to use the Coq-related capabilities of Why.
|
||||
|
|
@ -1 +0,0 @@
|
|||
Abandoned by upstream and fails to build from source
|
||||
35
div.pvs
Normal file
35
div.pvs
Normal file
|
|
@ -0,0 +1,35 @@
|
|||
% Copyright (c) 2010 Jerry James.
|
||||
%
|
||||
% Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
% of this software and associated documentation files (the "Software"), to deal
|
||||
% in the Software without restriction, including without limitation the rights
|
||||
% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
||||
% copies of the Software, and to permit persons to whom the Software is
|
||||
% furnished to do so, subject to the following conditions:
|
||||
%
|
||||
% The above copyright notice and this permission notice shall be included in
|
||||
% all copies or substantial portions of the Software.
|
||||
%
|
||||
% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
||||
% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
||||
% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
||||
% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
||||
% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
|
||||
% THE SOFTWARE.
|
||||
|
||||
div: THEORY
|
||||
BEGIN
|
||||
|
||||
x : VAR int
|
||||
nzy : VAR nzint
|
||||
|
||||
div(x, nzy): int =
|
||||
IF (x >= 0 AND nzy > 0) THEN ndiv(x, nzy)
|
||||
ELSIF (x >= 0 AND nzy < 0) THEN -ndiv(x, -nzy)
|
||||
ELSIF (x < 0 AND nzy > 0) THEN -ndiv(-x, nzy)
|
||||
ELSE ndiv(-x, -nzy)
|
||||
ENDIF
|
||||
|
||||
END div
|
||||
|
||||
43
jessie.appdata.xml
Normal file
43
jessie.appdata.xml
Normal file
|
|
@ -0,0 +1,43 @@
|
|||
<?xml version="1.0" encoding="UTF-8"?>
|
||||
<component type="desktop">
|
||||
<id>jessie.desktop</id>
|
||||
<metadata_license>CC0-1.0</metadata_license>
|
||||
<project_license>LGPL-2.1</project_license>
|
||||
<name>jessie</name>
|
||||
<summary>Interface between why and Frama-C</summary>
|
||||
<description>
|
||||
<p>
|
||||
Jessie is an interface between why and Frama-C.
|
||||
</p>
|
||||
<p>
|
||||
Why is a software verification platform that applies formal proving tools to
|
||||
annotated programs. The Jessie plugin provide the ability to analyze C
|
||||
programs by invoking Frama-C.
|
||||
</p>
|
||||
</description>
|
||||
<screenshots>
|
||||
<screenshot type="default">
|
||||
<image>http://krakatoa.lri.fr/jessie/max_why3ide.png</image>
|
||||
<caption>Interactive proof session</caption>
|
||||
</screenshot>
|
||||
<screenshot>
|
||||
<image>http://krakatoa.lri.fr/jessie/max_ptr_why3ide.png</image>
|
||||
<caption>Max function proof</caption>
|
||||
</screenshot>
|
||||
<screenshot>
|
||||
<image>http://krakatoa.lri.fr/jessie/binary_search_raw.png</image>
|
||||
<caption>Binary search function proof</caption>
|
||||
</screenshot>
|
||||
<screenshot>
|
||||
<image>http://krakatoa.lri.fr/jessie/binary_search_ovfl.png</image>
|
||||
<caption>Binary search arithmetic overflow</caption>
|
||||
</screenshot>
|
||||
<screenshot>
|
||||
<image>http://krakatoa.lri.fr/jessie/binary_search_behav.png</image>
|
||||
<caption>Binar search function behavior</caption>
|
||||
</screenshot>
|
||||
</screenshots>
|
||||
<update_contact>loganjerry@gmail.com</update_contact>
|
||||
<url type="homepage">http://krakatoa.lri.fr/</url>
|
||||
<url type="bugtracker">https://gforge.inria.fr/tracker/?atid=4012&group_id=999&func=browse</url>
|
||||
</component>
|
||||
7
jessie.desktop
Normal file
7
jessie.desktop
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
[Desktop Entry]
|
||||
Name=jessie
|
||||
Comment=Verify C program using Jessie plug-in
|
||||
Exec=frama-c -jessie %F
|
||||
Icon=why
|
||||
Type=Application
|
||||
Categories=Development;
|
||||
59
patch_jessie_pvs
Executable file
59
patch_jessie_pvs
Executable file
|
|
@ -0,0 +1,59 @@
|
|||
#!/bin/sh
|
||||
|
||||
# To use PVS with frama-c without the NASA Langley PVS library:
|
||||
# frama-c -jessie -jessie-atp pvs FILE.c # Generates PVS files
|
||||
# cd FILE.jessie/pvs
|
||||
# patch_jessie_pvs # Patch jessie_why.pvs to not need NASA Langley library.
|
||||
# You can then run PVS to prove the generated theorems with:
|
||||
# pvs-sbcl FILE_why.pvs
|
||||
#
|
||||
# Copyright (c) 2010 David A. Wheeler
|
||||
#
|
||||
# Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
# of this software and associated documentation files (the "Software"), to deal
|
||||
# in the Software without restriction, including without limitation the rights
|
||||
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
||||
# copies of the Software, and to permit persons to whom the Software is
|
||||
# furnished to do so, subject to the following conditions:
|
||||
#
|
||||
# The above copyright notice and this permission notice shall be included in
|
||||
# all copies or substantial portions of the Software.
|
||||
#
|
||||
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
||||
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
||||
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
||||
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
||||
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
|
||||
# THE SOFTWARE.
|
||||
|
||||
|
||||
if [ ! -f jessie_why.pvs ] ; then
|
||||
echo "Did not find file jessie_why.pvs in current directory"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
patch -p0 -N << END_OF_PATCH
|
||||
--- jessie_why.pvs.ORIGINAL 2010-10-05 14:41:58.965970651 -0400
|
||||
+++ jessie_why.pvs 2010-10-06 14:28:39.250971269 -0400
|
||||
@@ -169,14 +169,14 @@
|
||||
(FORALL (x: real): (FORALL (y: real): min(x, y) = x OR min(x, y) = y))
|
||||
|
||||
%% Why axiom sqrt_pos
|
||||
- sqrt_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x) >= 0.0))
|
||||
+ % sqrt_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x) >= 0.0))
|
||||
|
||||
%% Why axiom sqrt_sqr
|
||||
- sqrt_sqr: AXIOM
|
||||
- (FORALL (x: real): (x >= 0.0 IMPLIES sqr_real(sqrt(x)) = x))
|
||||
+ % sqrt_sqr: AXIOM
|
||||
+ % (FORALL (x: real): (x >= 0.0 IMPLIES sqr_real(sqrt(x)) = x))
|
||||
|
||||
%% Why axiom sqr_sqrt
|
||||
- sqr_sqrt: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x * x) = x))
|
||||
+ % sqr_sqrt: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x * x) = x))
|
||||
|
||||
%% Why axiom abs_real_pos
|
||||
abs_real_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES abs(x) = x))
|
||||
END_OF_PATCH
|
||||
|
||||
35
rem.pvs
Normal file
35
rem.pvs
Normal file
|
|
@ -0,0 +1,35 @@
|
|||
% Copyright (c) 2010 Jerry James.
|
||||
%
|
||||
% Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
% of this software and associated documentation files (the "Software"), to deal
|
||||
% in the Software without restriction, including without limitation the rights
|
||||
% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
||||
% copies of the Software, and to permit persons to whom the Software is
|
||||
% furnished to do so, subject to the following conditions:
|
||||
%
|
||||
% The above copyright notice and this permission notice shall be included in
|
||||
% all copies or substantial portions of the Software.
|
||||
%
|
||||
% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
||||
% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
||||
% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
||||
% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
||||
% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
|
||||
% THE SOFTWARE.
|
||||
|
||||
rem: THEORY
|
||||
BEGIN
|
||||
|
||||
x : VAR int
|
||||
nzy : VAR nzint
|
||||
|
||||
rem(x, nzy): int =
|
||||
IF (x >= 0 AND nzy > 0) THEN rem(nzy)(x)
|
||||
ELSIF (x >= 0 AND nzy < 0) THEN rem(-nzy)(x)
|
||||
ELSIF (x < 0 AND nzy > 0) THEN -rem(nzy)(-x)
|
||||
ELSE -rem(-nzy)(-x)
|
||||
ENDIF
|
||||
|
||||
END rem
|
||||
|
||||
3
sources
Normal file
3
sources
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
SHA512 (krakatoa.pdf) = 5d0f4e6b938ddc1eafa48264c02cf99e68f776a7e190b997e35fb2cd154627b5d27369886f570cbcfdfe5f3a1929a97a1fec9457a6f6662f83cbb2e51f65ca04
|
||||
SHA512 (why-2.39.tar.gz) = b36e9423ff82fa2f51fea40a33021ed0def3719d9421b2f7f1e2aa1d6113faacf932984ac293b6d0ac92f800fd48efbdd8cc3ec6a929003a57da20efab682bad
|
||||
SHA512 (why-icons.tar.xz) = d6ca78cf09540f5742564912470fb8c49f7d11ca16cd8bb60c8790af10c1591198f6020bd792cff8e3464f762b7ef0a690d3e4ba1a2cf670c286c8056d266bc3
|
||||
115
why-project.patch
Normal file
115
why-project.patch
Normal file
|
|
@ -0,0 +1,115 @@
|
|||
--- Makefile.in.orig 2017-08-23 02:08:38.000000000 -0600
|
||||
+++ Makefile.in 2017-12-04 21:00:24.549232019 -0700
|
||||
@@ -154,7 +154,7 @@ CMO_EXPORT = src/lib.cmo src/rc.cmo src
|
||||
src/effect.cmo src/pp.cmo src/option_misc.cmo \
|
||||
src/report.cmo \
|
||||
src/explain.cmo \
|
||||
- src/xml.cmo src/project.cmo
|
||||
+ src/xml.cmo src/whyproject.cmo
|
||||
|
||||
# jessie
|
||||
JCCML_EXPORT = src/why3_kw.ml jc/output.ml \
|
||||
--- src/options.mli.orig 2017-08-23 02:08:38.000000000 -0600
|
||||
+++ src/options.mli 2017-12-04 21:01:17.268996320 -0700
|
||||
@@ -184,7 +184,7 @@ val files : string list
|
||||
(*s GUI? *)
|
||||
|
||||
val gui : bool ref
|
||||
-val gui_project : Project.t option ref
|
||||
+val gui_project : Whyproject.t option ref
|
||||
val lib_files_to_load : string list
|
||||
|
||||
(*
|
||||
--- src/pretty.ml.orig 2017-08-23 02:08:38.000000000 -0600
|
||||
+++ src/pretty.ml 2017-12-04 21:02:42.540615229 -0700
|
||||
@@ -416,12 +416,12 @@ let output_project f =
|
||||
with Not_found ->
|
||||
functions := SMap.add fn SMap.empty !functions)
|
||||
Util.program_locs ;
|
||||
- let p = Project.create (Filename.basename f) in
|
||||
- Project.set_project_context_file p (f ^ "_ctx.why");
|
||||
+ let p = Whyproject.create (Filename.basename f) in
|
||||
+ Whyproject.set_project_context_file p (f ^ "_ctx.why");
|
||||
List.iter
|
||||
(fun (expl,fpo) ->
|
||||
let n = expl.lemma_or_fun_name in
|
||||
- let _ = Project.add_lemma p n expl fpo in ())
|
||||
+ let _ = Whyproject.add_lemma p n expl fpo in ())
|
||||
!lemmas;
|
||||
SMap.iter
|
||||
(fun fname behs ->
|
||||
@@ -431,15 +431,15 @@ let output_project f =
|
||||
floc
|
||||
with Not_found -> Loc.dummy_floc
|
||||
in
|
||||
- let f = Project.add_function p fname floc in
|
||||
+ let f = Whyproject.add_function p fname floc in
|
||||
SMap.iter
|
||||
(fun beh vcs ->
|
||||
- let be = Project.add_behavior f beh floc in
|
||||
+ let be = Whyproject.add_behavior f beh floc in
|
||||
List.iter
|
||||
(fun (expl,fpo) ->
|
||||
- let _ = Project.add_goal be expl fpo in ())
|
||||
+ let _ = Whyproject.add_goal be expl fpo in ())
|
||||
vcs)
|
||||
behs)
|
||||
!functions;
|
||||
- Project.save p f;
|
||||
+ Whyproject.save p f;
|
||||
p
|
||||
--- src/pretty.mli.orig 2017-08-23 02:08:38.000000000 -0600
|
||||
+++ src/pretty.mli 2017-12-04 21:03:05.635512035 -0700
|
||||
@@ -50,4 +50,4 @@ val output_files : string -> unit
|
||||
(* [output_project f] produces a whole project description, in a file
|
||||
[f.wpr], together with other needed files [f_ctx.why], [f_lemmas.why],
|
||||
and each goal in a separate file [f_po<i>.why] for i=1,2,... *)
|
||||
-val output_project : string -> Project.t
|
||||
+val output_project : string -> Whyproject.t
|
||||
--- src/whyweb.ml.orig 2017-08-23 02:08:38.000000000 -0600
|
||||
+++ src/whyweb.ml 2017-12-04 21:04:16.932193463 -0700
|
||||
@@ -29,7 +29,7 @@
|
||||
(**************************************************************************)
|
||||
|
||||
open Format
|
||||
-open Project
|
||||
+open Whyproject
|
||||
|
||||
(*prover*)
|
||||
let provers = [Ergo ; Simplify ; Z3 ; Yices ; Cvc3]
|
||||
@@ -168,7 +168,7 @@ let file = match !file with
|
||||
| None -> ()
|
||||
| Some f -> Arg.usage spec usage; exit 1
|
||||
|
||||
-let proj = ref (Project.create "")
|
||||
+let proj = ref (Whyproject.create "")
|
||||
|
||||
let proj_file = ref ""
|
||||
|
||||
@@ -260,7 +260,7 @@ let interp_com c =
|
||||
let _ = Thread.create (launch_behavior Cvc3) b in ()
|
||||
| `LaunchCvc3Function f ->
|
||||
let _ = Thread.create (launch_function Cvc3) f in ()
|
||||
- | `Save -> Project.save !proj !proj.project_name
|
||||
+ | `Save -> Whyproject.save !proj !proj.project_name
|
||||
end;
|
||||
loc
|
||||
with Not_found -> ("",0,0,0)
|
||||
@@ -343,7 +343,7 @@ let main_page msg =
|
||||
let load_prj file =
|
||||
eprintf "Reading file %s@." file;
|
||||
try
|
||||
- proj := Project.load file;
|
||||
+ proj := Whyproject.load file;
|
||||
proj_file := file;
|
||||
with
|
||||
Sys_error _ ->
|
||||
@@ -526,7 +526,7 @@ wprint "<center><a href=\"%s\">Save Proj
|
||||
<table border=\"1\" cellpadding=\"0\" cellspacing=\"0\">" ns;
|
||||
wprint "<tr><th></th>";
|
||||
List.iter (fun prover ->
|
||||
- wprint "<th>%s</th>" (Project.provers_name prover))
|
||||
+ wprint "<th>%s</th>" (Whyproject.provers_name prover))
|
||||
provers;
|
||||
wprint "</tr>
|
||||
";
|
||||
599
why.spec
Normal file
599
why.spec
Normal file
|
|
@ -0,0 +1,599 @@
|
|||
# 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: 3%{?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
|
||||
# Avoid a clash between Frama-C and why modules both named "Project".
|
||||
# Sent upstream 26 Jun 2014.
|
||||
Patch0: %{name}-project.patch
|
||||
|
||||
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
|
||||
%patch0
|
||||
|
||||
# The other part of avoiding the "Project" module name clash
|
||||
mv src/project.ml src/whyproject.ml
|
||||
mv src/project.mli src/whyproject.mli
|
||||
|
||||
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 Dec 9 2017 Jerry James <loganjerry@gmail.com> - 2.39-3
|
||||
- Bring back the -project patch, still needed (bz 1520483)
|
||||
|
||||
* 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.39-1
|
||||
- Update to 2.39.
|
||||
|
||||
* 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.
|
||||
Loading…
Add table
Add a link
Reference in a new issue