Abandoned by upstream and fails to build from source

Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>

.cvsignore

@@ -1,2 +0,0 @@
-krakatoa.pdf
-why-2.23.tar.gz

Makefile

@@ -1,21 +0,0 @@
-# Makefile for source rpm: why
-# $Id: Makefile,v 1.1 2008/08/04 18:32:10 kevin Exp $
-NAME := why
-SPECFILE = $(firstword $(wildcard *.spec))
-
-define find-makefile-common
-for d in common ../common ../../common ; do if [ -f $$d/Makefile.common ] ; then if [ -f $$d/CVS/Root -a -w $$d/Makefile.common ] ; then cd $$d ; cvs -Q update ; fi ; echo "$$d/Makefile.common" ; break ; fi ; done
-endef
-
-MAKEFILE_COMMON := $(shell $(find-makefile-common))
-
-ifeq ($(MAKEFILE_COMMON),)
-# attept a checkout
-define checkout-makefile-common
-test -f CVS/Root && { cvs -Q -d $$(cat CVS/Root) checkout common && echo "common/Makefile.common" ; } || { echo "ERROR: I can't figure out how to checkout the 'common' module." ; exit -1 ; } >&2
-endef
-
-MAKEFILE_COMMON := $(shell $(checkout-makefile-common))
-endif
-
-include $(MAKEFILE_COMMON)

README.why

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

README.why-coq.Fedora

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

README.why-gwhy.Fedora

@@ -1,6 +0,0 @@
-Fedora why-gwhy package:
-
-Contains the gwhy GUI for Why.
-
-Run gwhy with "gwhy <filename>". (If you forget and run without a
-filename you'll be prompted for it.)

dead.package

@@ -0,0 +1 @@
+Abandoned by upstream and fails to build from source

gwhy-2.23.patch

@@ -1,53 +0,0 @@
---- why-2.23-old/bin/gwhy.sh	2010-01-04 21:08:50.401993553 -0500
-+++ why-2.23/bin/gwhy.sh	2010-01-05 08:31:05.989807947 -0500
-@@ -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
- 
- 

gwhy.desktop

@@ -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;

import.log

@@ -1,4 +0,0 @@
-why-2_14-2_fc9:HEAD:why-2.14-2.fc9.src.rpm:1217954050
-why-2_17-1_fc11:HEAD:why-2.17-1.fc11.src.rpm:1230136029
-why-2_17-4_fc10:HEAD:why-2.17-4.fc10.src.rpm:1249698515
-why-2_23-1_fc12:HEAD:why-2.23-1.fc12.src.rpm:1262980547

min.mlw

@@ -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@ }

min_why.why.result

@@ -1,45 +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 div_int : int, int -> int
-
-logic mod_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)
-

sources

@@ -1,2 +0,0 @@
-14563361a9427e58115825b4e782d23e  krakatoa.pdf
-8b8d8f6376e42c688521abf5d9f21a9c  why-2.23.tar.gz

why-2.23-Makefile.in.patch

@@ -1,49 +0,0 @@
---- why-2.23-old/Makefile.in	2010-01-04 21:08:49.858843630 -0500
-+++ why-2.23/Makefile.in	2010-01-05 20:34:20.912391080 -0500
-@@ -650,14 +650,23 @@
- bin/cadlog.opt: src/version.cmx c/cversion.cmx tools/cadlog.cmx
- 	$(OCAMLOPT) unix.cmxa -o $@ $^
- 
-+ifeq ($(OCAMLBEST), opt)
-+MAKE_FLOAT_MODEL = tools/make_float_model.opt
-+else
-+MAKE_FLOAT_MODEL = tools/make_float_model.byte
-+endif
-+
-+tools/make_float_model.byte: tools/make_float_model.cmo
-+	$(OCAMLC) -o $@ $^
-+
- tools/make_float_model.opt: tools/make_float_model.cmx
- 	$(OCAMLOPT) -o $@ $^
- 
--lib/why/double_model.why lib/why/double_strict.why: tools/make_float_model.opt
--	tools/make_float_model.opt double 53 -1074
-+lib/why/double_model.why lib/why/double_strict.why: $(MAKE_FLOAT_MODEL)
-+	$(MAKE_FLOAT_MODEL) double 53 -1074
- 
--lib/why/single_model.why lib/why/single_strict.why: tools/make_float_model.opt
--	tools/make_float_model.opt single 24 -149
-+lib/why/single_model.why lib/why/single_strict.why: $(MAKE_FLOAT_MODEL)
-+	$(MAKE_FLOAT_MODEL) single 24 -149
- 
- 
- static:: $(STATICBINARY)
-@@ -842,15 +851,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 ; \
--	 cp -f $(V8FILES) $(COQLIB)/user-contrib ; \
--	 cp -f $(VO8) $(COQLIB)/user-contrib ; \
--	else \
--	echo "Cannot copy to Coq standard library. Add $(LIBDIR)/why/coq to Coq include path." ;\
--	mkdir -p $(LIBDIR)/why/coq ;\
--	cp -f $(VO8) $(V8FILES) $(LIBDIR)/why/coq ;\
--	fi
-+	mkdir -p $(COQLIB)/user-contrib
-+	cp -f $(V8FILES) $(COQLIB)/user-contrib
-+	cp -f $(VO8) $(COQLIB)/user-contrib
- 
- install-pvs-no:
- install-pvs-yes: $(PVSFILES)

why.spec

@@ -1,333 +0,0 @@
-Name:           why
-Version:        2.23
-Release:        2%{?dist}
-Summary:        Why software verification platform
-
-Group:          Applications/Engineering
-License:        GPLv2
-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
-
-# 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-%{version}.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-%{version}-Makefile.in.patch
-
-BuildRoot:      %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
-BuildRequires:  ocaml >= 3.09, ocaml-camlp4-devel, gtk2-devel, ocaml-lablgtk-devel, desktop-file-utils, dos2unix, prelink
-BuildRequires:  ocaml-ocamlgraph-devel
-BuildRequires:  cvc3
-
-ExcludeArch:    sparc64 s390 s390x
-%if 0%{?fedora} >= 11
-# Doesn't seem to build on ppc64 for Fedora >= 11
-# bz: 516317
-ExcludeArch:    ppc64
-%endif
-
-# No coq on ppc64 (any Fedora version) at the moment
-%ifnarch ppc64
-%global has_coq 1
-%endif
-
-%global __ocaml_requires_opts -i Ast -i Cc -i Error -i Logic -i Logic_decl -i Ptree -i 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 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, Mizar are supported - having one is recommended and Coq is
-packaged for Fedora) and automated theorem provers (without any extra
-work, Simplify, Alt-Ergo, Yices, Z3, CVC Lite, Zenon are supported and
-Zenon is packaged for Fedora) so that these results can be externally
-proven, resulting in a proof of program correctness.
-
-%package gwhy
-Group:          Applications/Engineering
-Summary:        IDE for Why software verification platform
-Requires:       why = %{version}, 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.
-
-# No Coq for ppc64 -> certain subpackages can't be built, but main why can be
-%if 0%{?has_coq} == 1
-
-%package coq
-Group:          Applications/Engineering
-Summary:        Libraries for interfacing Coq with Why
-Requires:       why = %{version}
-BuildRequires:  coq
-
-%description coq
-This package contains a set of routines that assist in the
-manipulation of why Coq-formatted output within Coq.
-
-%endif
-
-%prep
-%setup -q
-
-%patch0 -p1
-%patch1 -p1
-
-cp %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 .
-
-%build
-%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
-
-# Native ocaml builds do not seem to work on ppc64 (many packages have
-# this problem)
-%ifarch ppc64
-%global opt 0
-%endif
-
-# It seems that we should not be creating debuginfo regardless of
-# whether we have opt or not, as debuginfo is not particularly useful
-# for OCaml programs
-
-# If we have opt, as this has a dependency on ocaml, we should have ocamlopt.opt
-
-%global debug_package %{nil}
-
-%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
-
-# We actually want to install library files into a non /usr/lib
-# directory as they aren't architecture dependent
-
-./configure --prefix=%{_prefix} --bindir=%{_bindir} --libdir=%{_datadir} --mandir=%{_mandir} \
-            %{!?has_coq: COQC=no}
-make %{opt_option}
-
-# Remove unnecessary execstack permissions
-%if %opt
-execstack -c bin/*.opt bin/why-cpulimit
-%endif
-
-# Strip binaries (Makefile misses some of them, and don't want to add an extra patch)
-strip bin/why-cpulimit
-%if %opt
-strip bin/*.opt
-%endif
-
-%check
-%if %opt
-%global why bin/why.opt
-%else
-%global why bin/why.byte
-%endif
-export WHYLIB=lib
-%why --why --output min min.mlw
-unset WHYLIB
-diff min_why.why min_why.why.result > /dev/null
-
-%install
-rm -rf %{buildroot}
-
-make %{opt_option} BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_datadir} MANDIR=%{buildroot}%{_mandir} \
-     %{?has_coq: COQLIB=%{buildroot}%{_datadir}/coq} install
-
-# Fix a small bug in their Makefile: if no Coq, NO .v files should be installed
-%if 0%{?has_coq} != 1
-rm -f `find %{buildroot}%{_datadir}/coq -name '*.v'`
-%endif
-
-# Install desktop icon and menu entry
-
-%global why_data_dir %{_datadir}/why
-%if %(test -d %{buildroot}%{why_data_dir} && echo 1 || echo 0) != 1
-mkdir -p %{buildroot}%{why_data_dir}
-%endif
-cp gwhy-icon.png %{buildroot}%{why_data_dir}
-
-sed -i -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' gwhy.desktop
-
-desktop-file-install --vendor="fedora"                  \
---dir=%{buildroot}%{_datadir}/applications              \
-gwhy.desktop
-
-%global why_doc_dir %{_defaultdocdir}/%{name}-%{version}/
-%global why_examples_dir %{why_doc_dir}examples/
-
-%global fix_encoding() dos2unix %1; mv %1 %1.old; \
-                       iconv -f ISO-8859-1 -t UTF-8 < %1.old > %1; rm %1.old \
-                       %{nil}
-
-# 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
-%fix_encoding COPYING
-cp -p caduceus.ps krakatoa.pdf README.why COPYING LICENSE %{buildroot}%{why_doc_dir}
-
-# Copy in the example files after converting to proper UTF-8, fix line
-# encodings, 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\)' | egrep -v '_inv|_coq|_why'`; do
-%fix_encoding $f
-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
-%fix_encoding $f
-cp -p $f %{buildroot}%{why_examples_dir}c/$f
-done
-
-%clean
-rm -rf %{buildroot}
-
-%files
-%defattr(-,root,root,-)
-# Binaries
-%{_bindir}/*
-%exclude %{_bindir}/gwhy*
-# Data for programs
-%{why_data_dir}
-%exclude %{why_data_dir}/gwhy-icon.png
-%{_datadir}/caduceus
-%{_datadir}/jessie
-# % {_datadir}/krakatoa
-%exclude %{_datadir}/jessie/jc.cmo
-%if %opt
-%exclude %{_datadir}/jessie/jc.cmx
-%exclude %{_datadir}/jessie/jc.o
-%endif
-# Man page
-%{_mandir}/man1/why.1.gz
-# Documentation and examples
-%{why_doc_dir}
-# This last example is really an example only for Coq - only .v files
-%exclude %{why_examples_dir}mlw/string-matching/
-
-%files gwhy
-%defattr(-,root,root,-)
-%{_bindir}/gwhy
-%{_bindir}/gwhy-bin
-%dir %{why_data_dir}
-%doc README.why-gwhy.Fedora
-%{why_data_dir}/gwhy-icon.png
-%{_datadir}/applications/fedora-gwhy.desktop
-
-%if 0%{?has_coq} == 1
-
-%files coq
-%defattr(-,root,root,-)
-%dir %{_datadir}/coq
-%dir %{_datadir}/coq/user-contrib
-%{_datadir}/coq/user-contrib/Why*
-# % exclude % {_datadir}/coq/user-contrib/Why*.v
-%{_datadir}/coq/user-contrib/caduceus*
-# % exclude % {_datadir}/coq/user-contrib/caduceus*.v
-%{_datadir}/coq/user-contrib/Caduceus.v*
-# % exclude % {_datadir}/coq/user-contrib/Caduceus.v
-%{_datadir}/coq/user-contrib/jessie_why.v*
-# % exclude % {_datadir}/coq/user-contrib/jessie_why.v
-%{_datadir}/coq/jessie_why.v*
-%doc README.why-coq.Fedora
-
-%endif
-
-%changelog
-* 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.