diff --git a/.gitignore b/.gitignore deleted file mode 100644 index 02ffd25..0000000 --- a/.gitignore +++ /dev/null @@ -1,3 +0,0 @@ -/why-2.29.tar.gz -/krakatoa.pdf -/caduceus.ps 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.26.patch b/gwhy-2.26.patch deleted file mode 100644 index 15a2576..0000000 --- a/gwhy-2.26.patch +++ /dev/null @@ -1,53 +0,0 @@ ---- bin/gwhy.sh.orig 2011-03-02 01:27:41.000000000 -0700 -+++ bin/gwhy.sh 2011-07-07 15:41:07.232455718 -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 $1 || exit 1 -+ b=`basename $file .java` -+ krakatoa $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,20 +19,23 @@ - make -f $b.makefile gui - ;; - *.c) -- b=`basename $1 .c` -- caduceus -why-opt -split-user-conj $1 || exit 1 -+ b=`basename $file .c` -+ caduceus -why-opt -split-user-conj $b.c || exit 1 - make -f $b.makefile gui - ;; - *.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.desktop b/gwhy.desktop deleted file mode 100644 index 27f853a..0000000 --- a/gwhy.desktop +++ /dev/null @@ -1,8 +0,0 @@ -[Desktop Entry] -Encoding=UTF-8 -Name=gwhy -Comment=Examine and develop Why .why files -Exec=gwhy -Icon=ICON-LOCATION-BASE/gwhy-icon.png -Type=Application -Categories=Development; \ No newline at end of file diff --git a/jessie.desktop b/jessie.desktop deleted file mode 100644 index 239f37a..0000000 --- a/jessie.desktop +++ /dev/null @@ -1,8 +0,0 @@ -[Desktop Entry] -Encoding=UTF-8 -Name=jessie -Comment=Verify C program using Jessie plug-in -Exec=frama-c -jessie %f -Icon=ICON-LOCATION-BASE/gwhy-icon.png -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 760ff1b..0000000 --- a/sources +++ /dev/null @@ -1,3 +0,0 @@ -34d8772de3d68c15a3a12935d90a0d60 krakatoa.pdf -a7eb00d1f78e59221629604167eb3151 caduceus.ps -cbb3b109a37f968bea9ffa6e43e3b822 why-2.29.tar.gz diff --git a/why-2.28-Makefile.in.patch b/why-2.28-Makefile.in.patch deleted file mode 100644 index 128b4e9..0000000 --- a/why-2.28-Makefile.in.patch +++ /dev/null @@ -1,20 +0,0 @@ ---- Makefile.in.orig 2011-03-02 01:27:41.000000000 -0700 -+++ Makefile.in 2011-07-07 15:41:43.759455717 -0600 -@@ -844,14 +844,9 @@ - cp -f $(V7FILES) $(LIBDIR)/why/coq7 - cp -f $(VO7) $(LIBDIR)/why/coq7 - install-coq-v8 install-coq-v8.1: -- if test -w $(COQLIB) ; then \ -- 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." ;\ -- mkdir -p $(LIBDIR)/why/coq ;\ -- cp -f $(VO8) $(V8FILES) $(LIBDIR)/why/coq ;\ -- fi -+ mkdir -p $(COQLIB)/user-contrib/Why -+ cp -f $(V8FILES) $(COQLIB)/user-contrib/Why -+ cp -f $(VO8) $(COQLIB)/user-contrib/Why - - install-pvs-no: - install-pvs-yes: $(PVSFILES) diff --git a/why.spec b/why.spec deleted file mode 100644 index 1c62b01..0000000 --- a/why.spec +++ /dev/null @@ -1,536 +0,0 @@ -# Whether coq is available -%ifarch alpha %{arm} %{ix86} ia64 x86_64 ppc sparc sparcv9 -%global has_coq 1 -%else -%global has_coq 0 -%endif - -# 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) - -# Don't create debuginfo; it's not particularly useful for OCaml programs. -%global debug_package %{nil} - -Name: why -Version: 2.29 -Release: 2%{?dist} -Summary: Software verification platform - -Group: Applications/Engineering -License: LPGLv2 with exceptions -URL: http://why.lri.fr/ -Source0: http://why.lri.fr/download/why-%{version}.tar.gz -Source1: README.why-gwhy.Fedora -Source2: README.why-coq.Fedora -Source3: README.why -Source4: gwhy.desktop -Source5: gwhy-icon.png -Source6: min.mlw -Source7: min_why.why.result -Source8: http://caduceus.lri.fr/manual/caduceus.ps -Source9: http://krakatoa.lri.fr/manual/krakatoa.pdf -Source10: jessie.desktop -Source11: div.pvs -Source12: rem.pvs -Source13: patch_jessie_pvs - -# 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.26.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: why-2.28-Makefile.in.patch - -BuildRequires: auto-destdir -BuildRequires: cvc3 -BuildRequires: desktop-file-utils -BuildRequires: emacs-nox xemacs-nox -BuildRequires: frama-c-devel -BuildRequires: gtk2-devel -BuildRequires: ocaml -BuildRequires: ocaml-camlp4-devel -BuildRequires: ocaml-lablgtk-devel -BuildRequires: ocaml-ocamldoc -BuildRequires: ocaml-ocamlgraph-devel -%if %{has_coq} -BuildRequires: coq -%endif -%if %{has_pvs} -BuildRequires: pvs -%endif - -# Only build on arches that support ocaml -ExclusiveArch: %{ocaml_arches} - -# Filter out names that should not be exposed externally -%global __requires_exclude ocaml\\\(((Ast)|(Cc)|(Env)|(Error)|(Loc)|(Logic)|(Logic_decl)|(Misc)|(Parser)|(Project)|(Ptree)|(Types))\\\) -%global __provides_exclude ocaml\\\(((Lexer)|(Lib)|(Loc)|(Output)|(Parser)|(Project)|(Report)|(Xml))\\\) - -%description -Why is a software verification platform that applies formal proving -tools to annotated programs. It is currently capable of analysis of C -(through the included tool "Caduceus"), 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 - -%if %{has_coq} -%package coq -Group: Applications/Engineering -Summary: Libraries for interfacing Coq with Why -Requires: %{name}%{?_isa} = %{version}-%{release} -Requires: coq - -%description coq -This package contains a set of routines that assist in the manipulation -of why Coq-formatted output within Coq. -%endif - -%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} -%if %{has_coq} -Requires: why-coq%{?_isa} = %{version}-%{release} -%endif -%if %{has_pvs} -Requires: why-pvs-support%{?_isa} = %{version}-%{release} -%endif -Requires: alt-ergo cvc3 gappa zenon - -%description all -This package provides a complete software verification platform suite -based on Why, including various automated and interactive provers. - -%prep -%setup -q -%patch0 -%patch1 - -cp -p %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 %SOURCE10 %SOURCE11 %SOURCE12 %SOURCE13 ./ - -# Fix missing DESTDIRs in the makefile -sed -e 's|$(COQLIB)/user-contrib/Why|$(DESTDIR)$(COQLIB)/user-contrib/Why|' \ - -e 's|$(PVSLIB)/why|$(DESTDIR)$(PVSLIB)/why|' \ - -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 a doubly utf8-encoded file -%fix_encoding examples/sqrt/sqrt_why.v UTF-8 ISO-8859-1 - -# 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: fix some warnings that -warn-error turns into errors -sed -i "s/| JCTrange _/| JCTlet _ | JCTrange _/" jc/jc_annot_inference.ml - -# APRON support: add a missing include and a missing rpath -sed -e "s|-I +apron|-I +apron -I +mlgmpidl|" \ - -e "s|-lpolkaMPQ_caml|-Wl,-rpath,%{_libdir}/ocaml/apron|" \ - -i 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 - -# Update the version numbers of external programs -# Also, command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl: -sed -e 's/versions_ok = \["0\.13\.0"\]/versions_ok = ["0.15.0"]/' \ - -e 's/versions_ok = \["0\.91";.*\]/versions_ok = ["0.93"]/' \ - -e 's/versions_ok = \["1\.0\.17";.*\]/versions_ok = ["1.0.29"]/' \ - -e 's/versions_ok = \["8\.0";.*\]/versions_ok = ["8.3pl2"]/' \ - -e 's/versions_ok = \["4\.1"\]/versions_ok = ["5.0"]/' \ - -e 's/command = "pvs"/command = "pvs-sbcl"/' \ - -e 's/PVS, (pvs, \["pvs"\]);/PVS, (pvs, ["pvs-sbcl" ; "pvs"]);/' \ - -i tools/dpConfig.ml -sed -e 's/pvs/pvs-sbcl/' -i configure - -%if %{has_coq} -%configure --enable-verbosemake -%else -%configure --enable-verbosemake COQC=no -%endif -make %{opt_option} - -# Strip binaries (the Makefile misses some of them) -strip bin/why-cpulimit -strip frama-c-plugin/Jessie.cmxs -%if %opt -strip bin/rv_merge.opt bin/simplify2why.opt bin/tool-stat.opt \ - bin/why2html.opt bin/why-dp.opt bin/why-obfuscator.opt bin/why-stat.opt -%endif - -%install -make install DESTDIR=%{buildroot} %{opt_option} PVSLIB=%{_libdir}/pvs/lib - -# Fix a small bug in their Makefile: if no Coq, NO .v files should be installed -%if ! %{has_coq} -rm -f `find %{buildroot}%{_datadir}/coq -name '*.v'` -%endif - -# 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 gwhy-icon.png %{buildroot}%{why_data_dir} -sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' -i gwhy.desktop -desktop-file-install --vendor="fedora" \ - --dir=%{buildroot}%{_datadir}/applications gwhy.desktop -sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' -i jessie.desktop -desktop-file-install --vendor="fedora" \ - --dir=%{buildroot}%{_datadir}/applications jessie.desktop - -%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 div.pvs rem.pvs %{buildroot}%{_libdir}/pvs/lib/ints/ -cp -p patch_jessie_pvs %{buildroot}%{_bindir}/ -%endif - -%global why_doc_dir %{_defaultdocdir}/%{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 caduceus.ps krakatoa.pdf README.why 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. - -%files -%{_bindir}/* -%{_libdir}/caduceus/ -%{_libdir}/why/ -%{_mandir}/man1/why.1* -%{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 -# why-coq: -%exclude %{_libdir}/caduceus/coq/ - -%files gwhy -%doc README.why-gwhy.Fedora -%{_bindir}/gwhy -%{_bindir}/gwhy-bin -%{why_data_dir}/ -%{_datadir}/applications/fedora-gwhy.desktop - -%files jessie -%{_bindir}/jessie -%{_libdir}/jessie/ -%{_libdir}/frama-c/plugins/Jessie.* -%{_datadir}/applications/fedora-jessie.desktop - -%if %{has_coq} -%files coq -%doc README.why-coq.Fedora -%{_libdir}/coq/user-contrib/Why/ -%{_libdir}/caduceus/coq/ -%endif - -%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 -* 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. - -# TODO: -# If file $HOME/.gwhyrc does not exist, autorun "why-config". -# Finish packaging/integrating "APRON" (for Inference of annotations) -