diff --git a/.gitignore b/.gitignore deleted file mode 100644 index fc049f3..0000000 --- a/.gitignore +++ /dev/null @@ -1,3 +0,0 @@ -/krakatoa.pdf -/why-2.34.tar.gz -/why-icons.tar.xz diff --git a/README.why b/README.why deleted file mode 100644 index ba95dfa..0000000 --- a/README.why +++ /dev/null @@ -1,8 +0,0 @@ -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. \ No newline at end of file diff --git a/README.why-coq.Fedora b/README.why-coq.Fedora deleted file mode 100644 index 406a7a9..0000000 --- a/README.why-coq.Fedora +++ /dev/null @@ -1,6 +0,0 @@ -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. \ No newline at end of file diff --git a/README.why-gwhy.Fedora b/README.why-gwhy.Fedora deleted file mode 100644 index 3cc41b4..0000000 --- a/README.why-gwhy.Fedora +++ /dev/null @@ -1,6 +0,0 @@ -Fedora why-gwhy package: - -Contains the gwhy GUI for Why. - -Run gwhy with "gwhy ". (If you forget and run without a -filename you'll be prompted for it.) \ No newline at end of file diff --git a/dead.package b/dead.package new file mode 100644 index 0000000..497866a --- /dev/null +++ b/dead.package @@ -0,0 +1 @@ +Abandoned by upstream and fails to build from source diff --git a/div.pvs b/div.pvs deleted file mode 100644 index 4005fe3..0000000 --- a/div.pvs +++ /dev/null @@ -1,35 +0,0 @@ -% 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 - diff --git a/gwhy-2.33.patch b/gwhy-2.33.patch deleted file mode 100644 index d106a7e..0000000 --- a/gwhy-2.33.patch +++ /dev/null @@ -1,49 +0,0 @@ ---- bin/gwhy.sh.orig 2013-04-20 00:34:04.000000000 -0600 -+++ bin/gwhy.sh 2013-05-10 09:12:22.968553542 -0600 -@@ -1,11 +1,17 @@ - #!/bin/sh - --case $1 in -+if ! test $1; then -+ file=`zenity --file-selection --title="Select the file you want to open with gwhy"`; -+else -+ file=$1 -+fi -+ -+case $file in - *.java) -- b=`basename $1 .java` -- krakatoa -gen-only $1 || exit 1 -+ b=`basename $file .java` -+ krakatoa -gen-only $file || exit 1 - echo "krakatoa on $b.java done" -- d=`dirname $1` -+ d=`dirname $file` - echo "cd $d" - cd $d - jessie -locs $b.jloc -why-opt -split-user-conj $b.jc || exit 2 -@@ -13,18 +19,20 @@ - make -f $b.makefile gui - ;; - *.c) -- frama-c -jessie -jessie-atp=gui -jessie-why-opt="-split-user-conj" $1 || exit 1 -+ frama-c -jessie -jessie-atp=gui -jessie-why-opt="-split-user-conj" $file || exit 1 - ;; - *.jc) -- b=`basename $1 .jc` -+ b=`basename $file .jc` - jessie -why-opt -split-user-conj $b.jc || exit 1 - make -f $b.makefile gui - ;; - *.mlw|*.why) -- gwhy-bin -split-user-conj $1 -+ gwhy-bin -split-user-conj $file - ;; -+ ?*) -+ echo "$file does not have file type extension recognized by gwhy" - *) -- echo "don't know what to do with $1" -+ echo "gwhy needs the name of a file to inspect in order to run" - esac - - diff --git a/gwhy-icon.png b/gwhy-icon.png deleted file mode 100644 index 9a1b76c..0000000 Binary files a/gwhy-icon.png and /dev/null differ diff --git a/gwhy.appdata.xml b/gwhy.appdata.xml deleted file mode 100644 index f9126b8..0000000 --- a/gwhy.appdata.xml +++ /dev/null @@ -1,20 +0,0 @@ - - - gwhy.desktop - CC0 - -

- Gwhy is a graphical user interface for the Why software coordination - platform. It assists in the coordination of dispatching assertions that - need to be proven to different theorem provers by providing an interface to - do this and also supports inspection of why input files. -

- - - http://why.lri.fr/manual/manual001.png - - http://why.lri.fr/ - - diff --git a/gwhy.desktop b/gwhy.desktop deleted file mode 100644 index 8940b49..0000000 --- a/gwhy.desktop +++ /dev/null @@ -1,7 +0,0 @@ -[Desktop Entry] -Name=gwhy -Comment=Examine and develop Why .why files -Exec=gwhy -Icon=why -Type=Application -Categories=Development; diff --git a/jessie.appdata.xml b/jessie.appdata.xml deleted file mode 100644 index fc64aad..0000000 --- a/jessie.appdata.xml +++ /dev/null @@ -1,26 +0,0 @@ - - - jessie.desktop - CC0 - -

- Jessie is an interface between why and Frama-C. -

-

- 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. -

- - - http://krakatoa.lri.fr/jessie/max_why3ide.png - http://krakatoa.lri.fr/jessie/max_ptr_why3ide.png - http://krakatoa.lri.fr/jessie/binary_search_raw.png - http://krakatoa.lri.fr/jessie/binary_search_ovfl.png - http://krakatoa.lri.fr/jessie/binary_search_behav.png - - http://krakatoa.lri.fr/ - - diff --git a/jessie.desktop b/jessie.desktop deleted file mode 100644 index 099b3ad..0000000 --- a/jessie.desktop +++ /dev/null @@ -1,7 +0,0 @@ -[Desktop Entry] -Name=jessie -Comment=Verify C program using Jessie plug-in -Exec=frama-c -jessie %F -Icon=why -Type=Application -Categories=Development; diff --git a/min.mlw b/min.mlw deleted file mode 100644 index ae72dea..0000000 --- a/min.mlw +++ /dev/null @@ -1,4 +0,0 @@ -logic min: int, int -> int -axiom min_ax: forall x,y:int. min(x,y) <= x -parameter r: int ref -let f (n:int) = {} r := min !r n { r <= r@ } \ No newline at end of file diff --git a/min_why.why.result b/min_why.why.result deleted file mode 100644 index 04848f9..0000000 --- a/min_why.why.result +++ /dev/null @@ -1,41 +0,0 @@ -logic eq_unit : unit, unit -> prop - -logic neq_unit : unit, unit -> prop - -logic eq_bool : bool, bool -> prop - -logic neq_bool : bool, bool -> prop - -logic lt_int : int, int -> prop - -logic le_int : int, int -> prop - -logic gt_int : int, int -> prop - -logic ge_int : int, int -> prop - -logic eq_int : int, int -> prop - -logic neq_int : int, int -> prop - -logic add_int : int, int -> int - -logic sub_int : int, int -> int - -logic mul_int : int, int -> int - -logic neg_int : int -> int - -predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b)) - -logic min : int, int -> int - -axiom min_ax: (forall x:int. (forall y:int. (min(x, y) <= x))) - -goal f_po_1: - forall n:int. - forall r0:int. - forall r:int. - (r = min(r0, n)) -> - (r <= r0) - diff --git a/patch_jessie_pvs b/patch_jessie_pvs deleted file mode 100755 index 3e4abca..0000000 --- a/patch_jessie_pvs +++ /dev/null @@ -1,59 +0,0 @@ -#!/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 - diff --git a/rem.pvs b/rem.pvs deleted file mode 100644 index 4f126a6..0000000 --- a/rem.pvs +++ /dev/null @@ -1,35 +0,0 @@ -% 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 - diff --git a/sources b/sources deleted file mode 100644 index a95f254..0000000 --- a/sources +++ /dev/null @@ -1,3 +0,0 @@ -cc7a2e360acf8569a2eb878f51bfc8ff krakatoa.pdf -e622157c9b5cfc4e454a2a98bcc5828c why-2.34.tar.gz -ed5648bbfb5e74fdfb814cdd725b191e why-icons.tar.xz diff --git a/why-2.34-Makefile.in.patch b/why-2.34-Makefile.in.patch deleted file mode 100644 index 931bc76..0000000 --- a/why-2.34-Makefile.in.patch +++ /dev/null @@ -1,23 +0,0 @@ ---- Makefile.in.orig 2014-03-17 16:01:46.000000000 -0600 -+++ Makefile.in 2014-03-17 20:00:00.000000000 -0600 -@@ -805,17 +805,9 @@ - mkdir -p $(LIBDIR)/why/coq7 - cp -f $(VO7) $(LIBDIR)/why/coq7 - install-coq-v8 install-coq-v8.1: -- if test -w $(COQLIB) ; then \ -- rm -f $(COQLIB)/user-contrib/Why*.v* ; \ -- rm -f $(COQLIB)/user-contrib/caduceus*.v* $(COQLIB)/user-contrib/Caduceus*.v* ; \ -- rm -f $(COQLIB)/user-contrib/jessie*.v* $(COQLIB)/user-contrib/Jessie*.v* ; \ -- mkdir -p $(COQLIB)/user-contrib/Why ; \ -- cp -f $(VO8) $(COQLIB)/user-contrib/Why ; \ -- else \ -- echo "Cannot copy to Coq standard library. Add \"-R $(LIBDIR)/why/coq Why\" to Coq options." ;\ -- fi -- mkdir -p $(LIBDIR)/why/coq -- cp -f $(VO8) $(LIBDIR)/why/coq -+ mkdir -p $(COQLIB)/user-contrib/Why -+ cp -pf $(V8FILES) $(COQLIB)/user-contrib/Why -+ cp -pf $(VO8) $(COQLIB)/user-contrib/Why - - install-pvs-no: - install-pvs-yes: $(PVSFILES) diff --git a/why-flocq23.patch b/why-flocq23.patch deleted file mode 100644 index b54d85a..0000000 --- a/why-flocq23.patch +++ /dev/null @@ -1,11 +0,0 @@ ---- lib/coq/WhyFloats.v.orig 2014-03-17 16:01:46.000000000 -0600 -+++ lib/coq/WhyFloats.v 2014-04-21 15:39:55.680771647 -0600 -@@ -108,7 +108,7 @@ - generalize (Zeq_bool_eq _ _ H1). clear. - rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat. - intros H. --apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)). -+apply (Fcore_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)). - revert H. - unfold FLT_exp. - generalize (Fcore_digits.Zdigits radix2 (Zpos m)). diff --git a/why-project.patch b/why-project.patch deleted file mode 100644 index a280c81..0000000 --- a/why-project.patch +++ /dev/null @@ -1,124 +0,0 @@ ---- ./Makefile.in.orig 2014-03-17 16:01:46.000000000 -0600 -+++ ./Makefile.in 2014-06-26 12:30:00.000000000 -0600 -@@ -222,7 +222,7 @@ CMO_EXPORT = src/lib.cmo src/rc.cmo src - src/effect.cmo src/pp.cmo src/option_misc.cmo \ - src/parser.cmo src/lexer.cmo src/report.cmo \ - src/explain.cmo \ -- src/xml.cmo src/project.cmo -+ src/xml.cmo src/whyproject.cmo - - CMO = src/lib.cmo src/rc.cmo tools/dpConfig.cmo \ - src/version.cmo src/options.cmo src/linenum.cmo src/loc.cmo \ -@@ -239,7 +239,7 @@ CMO = src/lib.cmo src/rc.cmo tools/dpCon - src/holl.cmo src/harvey.cmo src/simplify.cmo \ - src/regen.cmo src/mizar.cmo src/smtlib.cmo src/coq.cmo \ - src/zenon.cmo src/z3.cmo src/cvcl.cmo tools/calldp.cmo \ -- src/xml.cmo src/project.cmo \ -+ src/xml.cmo src/whyproject.cmo \ - src/why3_kw.cmo src/why3.cmo src/pretty.cmo \ - src/unionfind.cmo src/theoryreducer.cmo \ - src/theory_filtering.cmo src/hypotheses_filtering.cmo \ ---- ./src/options.mli.orig 2014-03-17 16:01:46.000000000 -0600 -+++ ./src/options.mli 2014-06-26 12:30:00.000000000 -0600 -@@ -185,7 +185,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 2014-03-17 16:01:46.000000000 -0600 -+++ ./src/pretty.ml 2014-06-26 12:30:00.000000000 -0600 -@@ -415,12 +415,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 -> -@@ -430,15 +430,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 2014-03-17 16:01:46.000000000 -0600 -+++ ./src/pretty.mli 2014-06-26 12:30:00.000000000 -0600 -@@ -51,4 +51,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.why] for i=1,2,... *) --val output_project : string -> Project.t -+val output_project : string -> Whyproject.t ---- ./src/whyweb.ml.orig 2014-03-17 16:01:46.000000000 -0600 -+++ ./src/whyweb.ml 2014-06-26 12:30:00.000000000 -0600 -@@ -30,7 +30,7 @@ - (**************************************************************************) - - open Format --open Project -+open Whyproject - - (*prover*) - let provers = [Ergo ; Simplify ; Z3 ; Yices ; Cvc3] -@@ -169,7 +169,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 "" - -@@ -261,7 +261,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 -> Whyroject.save !proj !proj.project_name - end; - loc - with Not_found -> ("",0,0,0) -@@ -344,7 +344,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 _ -> -@@ -527,7 +527,7 @@ wprint "
Save Proj - " ns; - wprint ""; - List.iter (fun prover -> -- wprint "" (Project.provers_name prover)) -+ wprint "" (Whyproject.provers_name prover)) - provers; - wprint " - "; diff --git a/why.spec b/why.spec deleted file mode 100644 index 8ca5b82..0000000 --- a/why.spec +++ /dev/null @@ -1,630 +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.34 -Release: 7%{?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: 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://krakatoa.lri.fr/manual/krakatoa.pdf -Source9: jessie.desktop -Source10: div.pvs -Source11: rem.pvs -Source12: patch_jessie_pvs -Source13: gwhy.appdata.xml -Source14: jessie.appdata.xml -# Created with gimp from official upstream icon -Source15: %{name}-icons.tar.xz - -# The gwhy execution shell script is not particularly informative -# about when bad parameters are passed to it - this patch fixes that. -# Upstream has been informed about this issue and a better fix is on -# their todo list -Patch0: gwhy-2.33.patch - -# 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. -Patch1: %{name}-2.34-Makefile.in.patch - -# Adapt to flocq 2.3.0 -Patch2: %{name}-flocq23.patch - -# Avoid a clash between Frama-C and why modules both named "Project". -# Sent upstream 26 Jun 2014. -Patch3: %{name}-project.patch - -BuildRequires: auto-destdir -BuildRequires: cvc3 -BuildRequires: desktop-file-utils -BuildRequires: emacs-nox xemacs xemacs-packages-extra -BuildRequires: frama-c-devel -BuildRequires: gappalib-coq -BuildRequires: gtk2-devel -BuildRequires: ocaml -BuildRequires: ocaml-apron-devel -BuildRequires: ocaml-camlp4-devel -BuildRequires: ocaml-findlib -BuildRequires: ocaml-lablgtk-devel -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 - -# Filter out bogus requires -%global __requires_exclude ocaml\\\((Ast|Cc|Env|Error|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, CVC3, 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 gwhy -Group: Applications/Engineering -Summary: IDE for Why software verification platform -Requires: %{name}%{?_isa} = %{version}-%{release}, zenity - -%description gwhy -Gwhy is an optional graphical user interface for the Why software -coordination platform. It assists in the coordination of dispatching -assertions that need to be proven to different theorem provers by -providing an interface to do this and also supports inspection of why -input files. - -%package jessie -Group: Applications/Engineering -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 -Group: Applications/Engineering -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 -Group: Applications/Engineering -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 emacs -Summary: Emacs support file for why files -Group: Development/Languages -Requires: %{name} = %{version}-%{release} -Requires: emacs(bin) -BuildArch: noarch - -%description emacs -This package contains an Emacs support file for working with why files. - -%package emacs-el -Summary: Emacs source file for why support -Group: Development/Languages -Requires: %{name}-emacs = %{version}-%{release} -BuildArch: noarch - -%description emacs-el -This package contains the Emacs source file for the Emacs why support. -This package is not needed to use the Emacs support. - -%package xemacs -Summary: XEmacs support file for why files -Group: Development/Languages -Requires: %{name} = %{version}-%{release} -Requires: xemacs(bin) -BuildArch: noarch - -%description xemacs -This package contains an XEmacs support file for working with why files. - -%package xemacs-el -Summary: XEmacs source file for why support -Group: Development/Languages -Requires: %{name}-xemacs = %{version}-%{release} -BuildArch: noarch - -%description xemacs-el -This package contains the XEmacs source file for the XEmacs why support. -This package is not needed to use the Emacs support. - -%package all -Group: Applications/Engineering -Summary: Complete Why software verification platform suite -Requires: why%{?_isa} = %{version}-%{release} -Requires: why-gwhy%{?_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 cvc3 gappalib-coq 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 15 -%patch0 -%patch1 -%patch2 -%patch3 - -# 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 %SOURCE1 %SOURCE2 %SOURCE6 %SOURCE7 ./ - -# Link with Fedora LDFLAGS -sed -e "\%^bin/jessie\.opt%,\%^bin/jessie\.byte%s/-o/-ccopt $RPM_LD_FLAGS &/" \ - -e "/gtkThread\.cmx/s/-o/-ccopt $RPM_LD_FLAGS &/" \ - -i Makefile.in - -%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 -sed -i "s|-lpolkaMPQ_caml|-Wl,-rpath,%{_libdir}/ocaml/apron|" 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 - -%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 - -# If no PVS, no .pvs files should be installed -%if ! %{has_pvs} -rm -fr %{buildroot}%{_libdir}/pvs -%endif - -# Install desktop icon and menu entry -%global why_data_dir %{_datadir}/why -mkdir -p %{buildroot}%{why_data_dir} -cp -p %{SOURCE5} %{buildroot}%{why_data_dir} -desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE4} -desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE9} - -# Install AppData files -mkdir -p %{buildroot}%{_datadir}/appdata -install -pm 644 %{SOURCE13} %{SOURCE14} %{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 %{SOURCE10} %{SOURCE11} %{buildroot}%{_libdir}/pvs/lib/ints/ -cp -p %{SOURCE12} %{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 %{SOURCE8} %{SOURCE3} CHANGES COPYING LICENSE 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 -%if %opt -%global why bin/why.opt -%else -%global why bin/why.byte -%endif -WHYLIB=lib %why --why --output min.why min.mlw -diff -u min.why min_why.why.result # Show differences from correct result. - -%post gwhy -update-desktop-database &> /dev/null || : -touch --no-create %{_datadir}/icons/hicolor &>/dev/null -gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : - -%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 gwhy -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 -%{_bindir}/* -%{_libdir}/why/ -%{_mandir}/man1/why.1* -%{_datadir}/icons/hicolor/*/apps/%{name}.png -%{why_doc_dir}/ -# This last example is really an example only for Coq - only .v files -%exclude %{why_examples_dir}mlw/string-matching/ -# why-gwhy: -%exclude %{_bindir}/gwhy* -# why-jessie -%exclude %{_bindir}/jessie -# why-pvs-support: -%exclude %{_bindir}/patch_jessie_pvs - -%files gwhy -%doc README.why-gwhy.Fedora -%{_bindir}/gwhy -%{_bindir}/gwhy-bin -%{why_data_dir}/ -%{_datadir}/appdata/gwhy.appdata.xml -%{_datadir}/applications/gwhy.desktop - -%files jessie -%{_bindir}/jessie -%{_libdir}/jessie/ -%{_libdir}/frama-c/plugins/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 - -%files emacs -%{_emacs_sitelispdir}/why.elc - -%files emacs-el -%{_emacs_sitelispdir}/why.el - -%files xemacs -%{_xemacs_sitelispdir}/why.elc - -%files xemacs-el -%{_xemacs_sitelispdir}/why.el - -# "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 -* Tue Jun 24 2014 Jerry James - 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 - 2.34-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild - -* Tue May 13 2014 Jerry James - 2.34-5 -- Rebuild for coq 8.4pl4 - -* Mon Apr 21 2014 Jerry James - 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 - 2.34-3 -- Remove ocaml_arches macro (RHBZ#1087794). - -* Mon Mar 24 2014 Jerry James - 2.34-2 -- Remove dropped patches -- Add icons -- Fix the desktop icon entries - -* Tue Mar 18 2014 Jerry James - 2.34-1 -- New upstream release -- Drop upstreamed -hashtbl, -flocq, and -or patches -- Add ocaml-findlib BR - -* Wed Feb 26 2014 Jerry James - 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 - 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ä - 2.33-4 -- Install docs to %%{_pkgdocdir} where available. - -* Fri Jun 21 2013 Jerry James - 2.33-3 -- Rebuild for frama-c Fluorine 20130601 - -* Thu May 23 2013 Jerry James - 2.33-2 -- Rebuild for new frama-c and why3 builds - -* Tue May 14 2013 Jerry James - 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 - 2.31-7 -- Remove vendor tag from desktop file as per https://fedorahosted.org/fesco/ticket/1077 - -* Mon Jan 14 2013 Jerry James - 2.31-6 -- Rebuild for alt-ergo 0.95 - -* Mon Jan 7 2013 Jerry James - 2.31-5 -- Rebuild for coq 8.4pl1 - -* Fri Oct 19 2012 Jerry James - 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 - 2.31-3 -- Rebuild for new frama-c build with altered API. - -* Mon Aug 27 2012 Jerry James - 2.31-2 -- Frama-c is fixed; rebuild with the Jessie plugin enabled and functioning - -* Thu Aug 23 2012 Jerry James - 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 - 2.30-7 -- Rebuild for OCaml 4.00.0 official. - -* Sun Jul 22 2012 Fedora Release Engineering - 2.30-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild - -* Wed Jan 11 2012 Jerry James - 2.30-5 -- Patch to work with flocq 2.0.0 - -* Tue Dec 27 2011 Jerry James - 2.30-4 -- Rebuild for coq 8.3pl3 - -* Tue Dec 6 2011 Jerry James - 2.30-3 -- Update alt_ergo and yices "okay" version numbers - -* Wed Nov 23 2011 Jerry James - 2.30-2 -- Rebuild with APRON and gappalib-coq support - -* Fri Oct 28 2011 Jerry James - 2.30-1 -- New upstream release - -* Thu Jul 14 2011 Jerry James - 2.29-2 -- Fix broken conditionals - -* Mon Jul 11 2011 Jerry James - 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 2.28-2.2 -- add ppc to excludearch, too. No pvs-sbcl available there - -* Wed Apr 13 2011 Karsten Hopp 2.28-2.1 -- add ppc64 to excludearch, no sbcl available there - -* Mon Feb 07 2011 Fedora Release Engineering - 2.28-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild - -* Fri Jan 21 2011 Richard W.M. Jones - 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 - 2.26-2 -- Bump and rebuild for OCaml 3.12. - -* Sat Oct 09 2010 David A. Wheeler + Mark Rader - 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 - 2.23-2 -- Rebuild to fix dependencies. - -* Fri Jan 08 2010 Alan Dunn - 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 - 2.17-5 -- Exclude sparc64 s390 s390x there is no ocaml there - -* Fri Aug 07 2009 Alan Dunn - 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 - 2.17-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild - -* Wed Feb 25 2009 Fedora Release Engineering - 2.17-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild - -* Wed Dec 24 2008 Alan Dunn 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 2.14-2.1 -- ExcludeArch ppc64 on Fedora 8 due to no ocaml. -* Fri Aug 1 2008 Alan Dunn 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 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 2.13-2 -- Added several patches: fixed Zenon output, completed fix of rename - of cpulimit -> why-cpulimit. -* Wed Jul 23 2008 Alan Dunn 2.13-1 -- Initial Fedora RPM version.
%s%s