jjames pushed to why (master). "New upstream release. (..more)"
notifications at fedoraproject.org
notifications at fedoraproject.org
Tue Mar 31 21:58:59 UTC 2015
>From e031c5b41e25324d0e18dbcec1b2b74fdfde58d0 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry at gmail.com>
Date: Tue, 31 Mar 2015 15:58:10 -0600
Subject: 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.
diff --git a/.gitignore b/.gitignore
index fc049f3..ed00d3a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,3 @@
/krakatoa.pdf
-/why-2.34.tar.gz
+/why-2.35.tar.gz
/why-icons.tar.xz
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 <filename>". (If you forget and run without a
-filename you'll be prompted for it.)
\ No newline at end of file
diff --git a/gwhy-2.33.patch b/gwhy-2.33.patch
deleted file mode 100644
index d55b90f..0000000
--- a/gwhy-2.33.patch
+++ /dev/null
@@ -1,51 +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,22 @@
- 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 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<application>
- <id type="desktop">gwhy.desktop</id>
- <licence>CC0</licence>
- <description>
- <p>
- 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.
- </p>
- </description>
- <screenshots>
- <screenshot type="default">http://why.lri.fr/manual/manual001.png</screenshot>
- </screenshots>
- <url type="homepage">http://why.lri.fr/</url>
- <!-- FIXME: change this to an upstream email address for spec updates
- <updatecontact>someone_who_cares at upstream_project.org</updatecontact>
- -->
-</application>
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/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/sources b/sources
index a95f254..e3fda8e 100644
--- a/sources
+++ b/sources
@@ -1,3 +1,3 @@
cc7a2e360acf8569a2eb878f51bfc8ff krakatoa.pdf
-e622157c9b5cfc4e454a2a98bcc5828c why-2.34.tar.gz
+10bde72f95de8bc34135a8207cfcc9ec why-2.35.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-2.35-Makefile.in.patch b/why-2.35-Makefile.in.patch
new file mode 100644
index 0000000..5b490d5
--- /dev/null
+++ b/why-2.35-Makefile.in.patch
@@ -0,0 +1,23 @@
+--- Makefile.in.orig 2015-03-25 08:32:17.000000000 -0600
++++ Makefile.in 2015-03-30 20:00:00.000000000 -0600
+@@ -815,17 +815,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-flocq24.patch b/why-flocq24.patch
deleted file mode 100644
index e4f10a4..0000000
--- a/why-flocq24.patch
+++ /dev/null
@@ -1,14 +0,0 @@
---- ./lib/coq/WhyFloats.v.orig 2014-03-17 16:01:46.000000000 -0600
-+++ ./lib/coq/WhyFloats.v 2014-09-02 17:40:03.356028320 -0600
-@@ -106,9 +106,9 @@ apply Zlt_succ_le.
- change (Zpos m < Zsucc (Zpred (Zpower_pos 2 prec)))%Z.
- rewrite <- Zsucc_pred.
- generalize (Zeq_bool_eq _ _ H1). clear.
--rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat.
-+rewrite Fcore_digits.Zpos_digits2_pos.
- intros H.
--apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
-+apply (Fcore_digits.Zpower_gt_Zdigits Fcore_Zaux.radix2 (Zpos prec) (Zpos m)).
- revert H.
- unfold FLT_exp.
- generalize (Fcore_digits.Zdigits radix2 (Zpos m)).
diff --git a/why-frama-c-sodium.patch b/why-frama-c-sodium.patch
deleted file mode 100644
index 6f79ce2..0000000
--- a/why-frama-c-sodium.patch
+++ /dev/null
@@ -1,100 +0,0 @@
---- ./configure.orig 2014-03-17 16:01:46.000000000 -0600
-+++ ./configure 2015-03-18 20:00:00.000000000 -0600
-@@ -2660,16 +2660,16 @@ $as_echo_n "checking Frama-c version...
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: $FRAMACVERSION" >&5
- $as_echo "$FRAMACVERSION" >&6; }
- case $FRAMACVERSION in
-- Neon-rc1|Neon-rc2|Neon-rc3|Neon-rc4|Neon-20140301)
-+ Sodium-rc1|Sodium-rc2|Sodium-rc3|Sodium-rc4|Sodium-20150201)
- FRAMACPLUGIN=yes
- ;;
-- Neon-*)
-- FRAMACMSG="Found unknown variant of Frama-C Neon (hope this works)"
-+ Sodium-*)
-+ FRAMACMSG="Found unknown variant of Frama-C Sodium (hope this works)"
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: $FRAMACMSG" >&5
- $as_echo "$as_me: WARNING: $FRAMACMSG" >&2;}
- FRAMACPLUGIN=yes
- ;;
-- *) FRAMACMSG="you need Frama-C version Neon"
-+ *) FRAMACMSG="you need Frama-C version Sodium"
- FRAMACPLUGIN=no
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: $FRAMACMSG" >&5
- $as_echo "$as_me: WARNING: $FRAMACMSG" >&2;}
---- ./frama-c-plugin/jessie_options.ml.orig 2014-03-17 16:01:46.000000000 -0600
-+++ ./frama-c-plugin/jessie_options.ml 2015-03-18 20:00:00.000000000 -0600
-@@ -38,7 +38,7 @@ include
- end)
-
- module ProjectName =
-- EmptyString
-+ Empty_string
- (struct
- let option_name = "-jessie-project-name"
- let arg_name = ""
-@@ -46,7 +46,7 @@ module ProjectName =
- end)
-
- module Behavior =
-- EmptyString
-+ Empty_string
- (struct
- let option_name = "-jessie-behavior"
- let arg_name = ""
-@@ -98,14 +98,14 @@ let () =
- ~from:Analysis.self [ ForceAdHocNormalization.self ]
-
- module JcOpt =
-- StringSet(struct
-+ String_set(struct
- let option_name = "-jessie-jc-opt"
- let arg_name = ""
- let help = "give an option to Jc (e.g., -jessie-jc-opt=\"-trust-ai\")"
- end)
-
- module WhyOpt =
-- StringSet
-+ String_set
- (struct
- let option_name = "-jessie-why-opt"
- let arg_name = ""
-@@ -113,7 +113,7 @@ module WhyOpt =
- end)
-
- module Why3Opt =
-- StringSet
-+ String_set
- (struct
- let option_name = "-jessie-why3-opt"
- let arg_name = ""
-@@ -127,7 +127,7 @@ module GenOnly =
- end)
-
- module InferAnnot =
-- EmptyString
-+ Empty_string
- (struct
- let option_name = "-jessie-infer-annot"
- let arg_name = ""
---- ./frama-c-plugin/register.ml.orig 2014-03-17 16:01:46.000000000 -0600
-+++ ./frama-c-plugin/register.ml 2015-03-18 20:00:00.000000000 -0600
-@@ -244,7 +244,7 @@ let run () =
- s);
- !res
- in
-- let jc_opt = Jessie_options.JcOpt.get_set ~sep:" " () in
-+ let jc_opt = Jessie_options.JcOpt.As_string.get () in
- let debug_opt = if Jessie_options.debug_atleast 1 then " -d " else " " in
- let behav_opt =
- if Jessie_options.Behavior.get () <> "" then
---- ./tests/c/oracle/sparse_array.res.oracle.orig 2014-03-17 16:01:46.000000000 -0600
-+++ ./tests/c/oracle/sparse_array.res.oracle 2015-03-18 20:00:00.000000000 -0600
-@@ -119,7 +119,7 @@ tests/c/sparse_array.c:72:[kernel] warni
-
- Unexpected error (File "src/kernel/ast_info.ml", line 391, characters 11-17: Assertion failed).
- Please report as 'crash' at http://bts.frama-c.com/.
-- Your Frama-C version is Neon-20140301.
-+ Your Frama-C version is Sodium-20150201.
- Note that a version and a backtrace alone often do not contain enough
- information to understand the bug. Guidelines for reporting bugs are at:
- http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
diff --git a/why-ocamlgraph186.patch b/why-ocamlgraph186.patch
index 7e86801..fd15ef4 100644
--- a/why-ocamlgraph186.patch
+++ b/why-ocamlgraph186.patch
@@ -1,6 +1,6 @@
---- src/hypotheses_filtering.ml.orig 2014-03-17 16:01:46.000000000 -0600
-+++ src/hypotheses_filtering.ml 2015-03-18 12:30:00.000000000 -0600
-@@ -1686,9 +1686,9 @@
+--- src/hypotheses_filtering.ml.orig 2015-03-25 08:32:17.000000000 -0600
++++ src/hypotheses_filtering.ml 2015-03-30 20:00:00.000000000 -0600
+@@ -1680,9 +1680,9 @@
*******************)
module W = struct
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<i>.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 at ." file;
- try
-- proj := Project.load file;
-+ proj := Whyproject.load file;
- proj_file := file;
- with
- Sys_error _ ->
-@@ -527,7 +527,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>
- ";
diff --git a/why.spec b/why.spec
index faf814a..1e54602 100644
--- a/why.spec
+++ b/why.spec
@@ -9,35 +9,23 @@
%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
Name: why
-Version: 2.34
-Release: 18%{?dist}
+Version: 2.35
+Release: 1%{?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
+Source1: http://krakatoa.lri.fr/manual/krakatoa.pdf
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
+Source4: jessie.desktop
+Source5: jessie.appdata.xml
+Source6: div.pvs
+Source7: rem.pvs
+Source8: patch_jessie_pvs
# 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
+Source9: %{name}-icons.tar.xz
# 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
@@ -45,20 +33,10 @@ Patch0: gwhy-2.33.patch
# 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.4.0
-Patch2: %{name}-flocq24.patch
-
-# Avoid a clash between Frama-C and why modules both named "Project".
-# Sent upstream 26 Jun 2014.
-Patch3: %{name}-project.patch
+Patch0: %{name}-2.35-Makefile.in.patch
# Adapt to ocamlgraph 1.8.6
-Patch4: %{name}-ocamlgraph186.patch
-
-# Adapt to Frama-C Sodium
-Patch5: %{name}-frama-c-sodium.patch
+Patch1: %{name}-ocamlgraph186.patch
BuildRequires: auto-destdir
BuildRequires: cvc3
@@ -66,12 +44,10 @@ BuildRequires: desktop-file-utils
BuildRequires: emacs xemacs xemacs-packages-extra
BuildRequires: frama-c
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
@@ -82,6 +58,20 @@ BuildRequires: pvs
%endif
Requires: hicolor-icon-theme
+Requires: emacs-filesystem
+Requires: xemacs-filesystem
+
+# This can be removed once Fedora 22 reaches EOL
+Obsoletes: %{name}-gwhy < 2.35-1%{?dist}
+Provides: %{name}-gwhy = %{version}-%{release}
+Obsoletes: %{name}-emacs < 2.35-1%{?dist}
+Provides: %{name}-emacs = %{version}-%{release}
+Obsoletes: %{name}-emacs-el < 2.35-1%{?dist}
+Provides: %{name}-emacs-el = %{version}-%{release}
+Obsoletes: %{name}-xemacs < 2.35-1%{?dist}
+Provides: %{name}-xemacs = %{version}-%{release}
+Obsoletes: %{name}-xemacs-el < 2.35-1%{?dist}
+Provides: %{name}-xemacs-el = %{version}-%{release}
# Filter out bogus requires
%global __requires_exclude ocaml\\\((Ast|Cc|Env|Error|Logic|Logic_decl|Misc|Ptree|Types)\\\)
@@ -106,18 +96,6 @@ 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
@@ -152,51 +130,10 @@ 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}
@@ -210,19 +147,11 @@ based on Why, including various automated and interactive provers.
%prep
%setup -q
-%setup -q -T -D -a 15
+%setup -q -T -D -a 9
%patch0
%patch1
-%patch2
-%patch3
-%patch4
-%patch5
-
-# 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 ./
+cp -p %SOURCE2 ./
# Link with Fedora LDFLAGS
for flag in $RPM_LD_FLAGS; do
@@ -270,12 +199,6 @@ sed -e 's/command = "pvs"/command = "pvs-sbcl"/' \
-i tools/dpConfig.ml
sed -i 's/pvs/pvs-sbcl/' configure
-# Don't fail the build because of use of deprecated features
-sed -i 's/ -warn-error A//' Makefile.in
-
-# Build with why3 0.85
-sed -i 's/0\.83/0.85/' configure
-
%build
%if ! %{opt}
%global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
@@ -296,16 +219,12 @@ make install DESTDIR=%{buildroot} %{opt_option} \
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}
+# Install desktop file
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 -pm 644 %{SOURCE5} %{buildroot}%{_datadir}/appdata
# Install the icons
mkdir -p %{buildroot}%{_datadir}/icons
@@ -315,9 +234,9 @@ cp -a icons %{buildroot}%{_datadir}/icons/hicolor
# 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}/
+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}}
@@ -327,7 +246,7 @@ cp -p %{SOURCE12} %{buildroot}%{_bindir}/
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 README Version %{buildroot}%{why_doc_dir}
+cp -p %{SOURCE1} %{SOURCE3} CHANGES README Version %{buildroot}%{why_doc_dir}
# Copy in the example files, leaving behind all generated files
cd examples
@@ -362,29 +281,13 @@ cd %{buildroot}%{_xemacs_sitelispdir}
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 || :
+make check
%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
@@ -394,29 +297,19 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
%license COPYING LICENSE
%{_bindir}/*
%{_libdir}/why/
-%{_mandir}/man1/why.1*
%{_datadir}/icons/hicolor/*/apps/%{name}.png
+%{_emacs_sitelispdir}/why.el*
+%{_xemacs_sitelispdir}/why.el*
%{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
@@ -431,24 +324,18 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
%{_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 Mar 31 2015 Jerry James <loganjerry at 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 at gmail.com> - 2.34-18
- Rebuild for Frama-C Sodium
- Add -ocamlgraph186 patch to adapt to ocamlgraph 1.8.6
--
cgit v0.10.2
http://pkgs.fedoraproject.org/cgit/why.git/commit/?h=master&id=e031c5b41e25324d0e18dbcec1b2b74fdfde58d0
More information about the scm-commits
mailing list