diff --git a/alt-ergo-menhir.patch b/alt-ergo-menhir.patch new file mode 100644 index 0000000..4ab3e45 --- /dev/null +++ b/alt-ergo-menhir.patch @@ -0,0 +1,18 @@ +--- alt-ergo-2.3.0-free/sources/plugins/AB-Why3/dune.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/plugins/AB-Why3/dune 2022-06-20 13:27:36.662944620 -0600 +@@ -3,13 +3,13 @@ + + (menhir + (infer false) +- (flags --fixed-exception) ++ (flags --fixed-exception --table) + (modules why3_parser) + ) + + (library + (name ABWhy3Plugin) +- (libraries alt-ergo-lib alt-ergo-parsers) ++ (libraries alt-ergo-lib alt-ergo-parsers menhirLib) + (modules Why3_lexer Why3_parser Why3_loc Why3_ptree) + ) + diff --git a/alt-ergo-pervasives.patch b/alt-ergo-pervasives.patch index 4c0a255..bd72f54 100644 --- a/alt-ergo-pervasives.patch +++ b/alt-ergo-pervasives.patch @@ -14,451 +14,8 @@ close_out cout ---- alt-ergo-2.3.0-free/sources/lib/frontend/typechecker.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/frontend/typechecker.ml 2022-02-23 12:57:12.849376944 -0700 -@@ -37,7 +37,7 @@ module S = Set.Make(String) - module HSS = Hstring.Set - - module MString = -- Map.Make(struct type t = string let compare = Pervasives.compare end) -+ Map.Make(struct type t = string let compare = Stdlib.compare end) - - module Types = struct - -@@ -86,7 +86,7 @@ module Types = struct - List.for_all2 - (fun pp x -> - match pp with -- | PPTvarid (y, _) -> Pervasives.(=) x y -+ | PPTvarid (y, _) -> Stdlib.(=) x y - | _ -> false - ) lpp lvars - with Invalid_argument _ -> false -@@ -105,7 +105,7 @@ module Types = struct - to_tyvars := MString.add s nty !to_tyvars; - nty - end -- | PPTexternal (l, s, loc) when Pervasives.(=) s "farray" -> -+ | PPTexternal (l, s, loc) when Stdlib.(=) s "farray" -> - let t1,t2 = match l with - | [t2] -> PPTint,t2 - | [t1;t2] -> t1,t2 -@@ -116,7 +116,7 @@ module Types = struct - | PPTexternal (l, s, loc) -> - begin - match rectype with -- | Some (id, vars, ty) when Pervasives.(=) s id && -+ | Some (id, vars, ty) when Stdlib.(=) s id && - equal_pp_vars l vars -> ty - | _ -> - try ---- alt-ergo-2.3.0-free/sources/lib/reasoners/fun_sat.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/reasoners/fun_sat.ml 2022-02-23 12:57:12.849376944 -0700 -@@ -75,7 +75,7 @@ module Make (Th : Theory.S) : Sat_solver - SE.fold - (fun f mp -> - let w = var_inc +. try ME.find f mp with Not_found -> 0. in -- stable := !stable && Pervasives.(<=) w 1e100; -+ stable := !stable && Stdlib.(<=) w 1e100; - ME.add f w mp - )(Ex.bj_formulas_of expl) mp - in -@@ -118,9 +118,9 @@ module Make (Th : Theory.S) : Sat_solver - let dec = - List.fast_sort - (fun (_, x1, b1) (_, x2, b2) -> -- let c = Pervasives.compare b2 b1 in -+ let c = Stdlib.compare b2 b1 in - if c <> 0 then c -- else Pervasives.compare x2 x1 -+ else Stdlib.compare x2 x1 - )dec - in - (* -@@ -1171,7 +1171,7 @@ module Make (Th : Theory.S) : Sat_solver - let i = abs (interpretation ()) in - assert (i = 1 || i = 2 || i = 3); - if not !(env.model_gen_mode) && -- Pervasives.(<>) (Options.interpretation_timelimit ()) 0. then -+ Stdlib.(<>) (Options.interpretation_timelimit ()) 0. then - begin - Options.Time.unset_timeout ~is_gui:(Options.get_is_gui()); - Options.Time.set_timeout ---- alt-ergo-2.3.0-free/sources/lib/reasoners/ite_rel.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/reasoners/ite_rel.ml 2022-02-23 12:57:12.850376945 -0700 -@@ -32,7 +32,7 @@ module TB = - type t = E.t * bool - let compare (a1, b1) (a2, b2) = - let c = E.compare a1 a2 in -- if c <> 0 then c else Pervasives.compare b1 b2 -+ if c <> 0 then c else Stdlib.compare b1 b2 - end) - - type t = ---- alt-ergo-2.3.0-free/sources/lib/reasoners/satml_frontend.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/reasoners/satml_frontend.ml 2022-02-23 12:57:12.850376945 -0700 -@@ -508,7 +508,7 @@ module Make (Th : Theory.S) : Sat_solver - if res <> 0 then res - else - (* higher weight is better hence compare w2 w1 *) -- let res = Pervasives.compare w2 w1 in -+ let res = Stdlib.compare w2 w1 in - if res <> 0 then res - else - (* lower index is better *) -@@ -844,7 +844,7 @@ module Make (Th : Theory.S) : Sat_solver - } - - let normal_mconf () = -- {Util.nb_triggers = Pervasives.max 2 (nb_triggers () * 2); -+ {Util.nb_triggers = Stdlib.max 2 (nb_triggers () * 2); - no_ematching = no_Ematching(); - triggers_var = triggers_var (); - use_cs = false; -@@ -853,7 +853,7 @@ module Make (Th : Theory.S) : Sat_solver - } - - let greedy_mconf () = -- {Util.nb_triggers = Pervasives.max 10 (nb_triggers () * 10); -+ {Util.nb_triggers = Stdlib.max 10 (nb_triggers () * 10); - no_ematching = false; - triggers_var = true; - use_cs = true; -@@ -951,7 +951,7 @@ module Make (Th : Theory.S) : Sat_solver - - (* copied from sat_solvers.ml *) - let max_term_depth_in_sat env = -- let aux mx f = Pervasives.max mx (E.depth f) in -+ let aux mx f = Stdlib.max mx (E.depth f) in - let max_t = ME.fold (fun f _ mx -> aux mx f) env.gamma 0 in - ME.fold (fun _ ({ E.ff = f; _ }, _) mx -> aux mx f) env.ground_preds max_t - ---- alt-ergo-2.3.0-free/sources/lib/reasoners/satml.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/reasoners/satml.ml 2022-02-23 12:57:12.850376945 -0700 -@@ -361,7 +361,7 @@ module Make (Th : Theory.S) : SAT_ML wit - *) - - let f_weight env i j = -- Pervasives.(<) (Vec.get env.vars j).weight (Vec.get env.vars i).weight -+ Stdlib.(<) (Vec.get env.vars j).weight (Vec.get env.vars i).weight - - (* unused -- let f_filter env i = (Vec.get env.vars i).level < 0 *) - -@@ -375,7 +375,7 @@ module Make (Th : Theory.S) : SAT_ML wit - - let var_bump_activity env v = - v.weight <- v.weight +. env.var_inc; -- if Pervasives.(>) v.weight 1e100 then begin -+ if Stdlib.(>) v.weight 1e100 then begin - for i = 0 to env.vars.Vec.sz - 1 do - (Vec.get env.vars i).weight <- (Vec.get env.vars i).weight *. 1e-100 - done; -@@ -387,7 +387,7 @@ module Make (Th : Theory.S) : SAT_ML wit - - let clause_bump_activity env c = - c.activity <- c.activity +. env.clause_inc; -- if Pervasives.(>) c.activity 1e20 then begin -+ if Stdlib.(>) c.activity 1e20 then begin - for i = 0 to env.learnts.Vec.sz - 1 do - (Vec.get env.learnts i).activity <- - (Vec.get env.learnts i).activity *. 1e-20; ---- alt-ergo-2.3.0-free/sources/lib/structures/expr.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/structures/expr.ml 2022-02-23 12:57:12.851376945 -0700 -@@ -1031,7 +1031,7 @@ let mk_builtin ~is_pos n l = - (** Substitutions *) - - let is_skolem_cst v = -- try Pervasives.(=) (String.sub (Sy.to_string v.f) 0 4) "_sko" -+ try Stdlib.(=) (String.sub (Sy.to_string v.f) 0 4) "_sko" - with Invalid_argument _ -> false - - let get_skolem = -@@ -1669,9 +1669,9 @@ module Triggers = struct - | { f = (Name _) as s1; xs=tl1; _ }, { f = (Name _) as s2; xs=tl2; _ } -> - let l1 = List.map score_term tl1 in - let l2 = List.map score_term tl2 in -- let l1 = List.fast_sort Pervasives.compare l1 in -- let l2 = List.fast_sort Pervasives.compare l2 in -- let c = Util.cmp_lists l1 l2 Pervasives.compare in -+ let l1 = List.fast_sort Stdlib.compare l1 in -+ let l2 = List.fast_sort Stdlib.compare l2 in -+ let c = Util.cmp_lists l1 l2 Stdlib.compare in - if c <> 0 then c - else - let c = Sy.compare s1 s2 in -@@ -1702,7 +1702,7 @@ module Triggers = struct - - | { f = Op (Access a1) ; xs=[t1]; _ }, - { f = Op (Access a2) ; xs=[t2]; _ } -> -- let c = Pervasives.compare a1 a2 in (* should be Hstring.compare *) -+ let c = Stdlib.compare a1 a2 in (* should be Hstring.compare *) - if c<>0 then c else cmp_trig_term t1 t2 - - | { f = Op (Access _); _ }, _ -> -1 -@@ -1710,7 +1710,7 @@ module Triggers = struct - - | { f = Op (Destruct (_,a1)) ; xs = [t1]; _ }, - { f = Op (Destruct (_,a2)) ; xs = [t2]; _ } -> -- let c = Pervasives.compare a1 a2 in (* should be Hstring.compare *) -+ let c = Stdlib.compare a1 a2 in (* should be Hstring.compare *) - if c<>0 then c else cmp_trig_term t1 t2 - - | { f = Op (Destruct _); _ }, _ -> -1 -@@ -1725,9 +1725,9 @@ module Triggers = struct - (* ops that are not infix or prefix *) - let l1 = List.map score_term tl1 in - let l2 = List.map score_term tl2 in -- let l1 = List.fast_sort Pervasives.compare l1 in -- let l2 = List.fast_sort Pervasives.compare l2 in -- let c = Util.cmp_lists l1 l2 Pervasives.compare in -+ let l1 = List.fast_sort Stdlib.compare l1 in -+ let l2 = List.fast_sort Stdlib.compare l2 in -+ let c = Util.cmp_lists l1 l2 Stdlib.compare in - if c <> 0 then c - else - let c = Sy.compare s1 s2 in -@@ -1741,9 +1741,9 @@ module Triggers = struct - let cmp_trig_term_list tl2 tl1 = - let l1 = List.map score_term tl1 in - let l2 = List.map score_term tl2 in -- let l1 = List.rev (List.fast_sort Pervasives.compare l1) in -- let l2 = List.rev (List.fast_sort Pervasives.compare l2) in -- let c = Util.cmp_lists l1 l2 Pervasives.compare in -+ let l1 = List.rev (List.fast_sort Stdlib.compare l1) in -+ let l2 = List.rev (List.fast_sort Stdlib.compare l2) in -+ let c = Util.cmp_lists l1 l2 Stdlib.compare in - if c <> 0 then c else Util.cmp_lists tl1 tl2 cmp_trig_term - - let unique_stable_sort = ---- alt-ergo-2.3.0-free/sources/lib/structures/profiling.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/structures/profiling.ml 2022-02-23 12:57:12.851376945 -0700 -@@ -85,7 +85,7 @@ let state = - let set_sigprof () = - let tm = - let v = Options.profiling_period () in -- if Pervasives.(>) v 0. then v else -. v -+ if Stdlib.(>) v 0. then v else -. v - in - ignore - (Unix.setitimer Unix.ITIMER_PROF -@@ -629,9 +629,9 @@ let switch () = - - - let float_print fmt v = -- if Pervasives.(=) v 0. then fprintf fmt "-- " -- else if Pervasives.(<) v 10. then fprintf fmt "%0.5f" v -- else if Pervasives.(<) v 100. then fprintf fmt "%0.4f" v -+ if Stdlib.(=) v 0. then fprintf fmt "-- " -+ else if Stdlib.(<) v 10. then fprintf fmt "%0.5f" v -+ else if Stdlib.(<) v 100. then fprintf fmt "%0.4f" v - else fprintf fmt "%0.3f" v - - let line_of_module arr f = ---- alt-ergo-2.3.0-free/sources/lib/structures/symbols.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/structures/symbols.ml 2022-02-23 12:57:12.851376945 -0700 -@@ -124,7 +124,7 @@ let compare_operators op1 op2 = - (function - | Access h1, Access h2 | Constr h1, Constr h2 -> Hstring.compare h1 h2 - | Destruct (h1, b1), Destruct(h2, b2) -> -- let c = Pervasives.compare b1 b2 in -+ let c = Stdlib.compare b1 b2 in - if c <> 0 then c else Hstring.compare h1 h2 - | _ , (Plus | Minus | Mult | Div | Modulo - | Concat | Extract | Get | Set | Fixed | Float | Reach -@@ -155,7 +155,7 @@ let compare_forms f1 f2 = - Util.compare_algebraic f1 f2 - (function - | F_Unit b1, F_Unit b2 -- | F_Clause b1, F_Clause b2 -> Pervasives.compare b1 b2 -+ | F_Clause b1, F_Clause b2 -> Stdlib.compare b1 b2 - | _, (F_Unit _ | F_Clause _ | F_Lemma | F_Skolem - | F_Iff | F_Xor) -> - assert false -@@ -173,10 +173,10 @@ let compare_bounds a b = - let c = Ty.compare a.sort b.sort in - if c <> 0 then c - else -- let c = Pervasives.compare a.is_open b.is_open in -+ let c = Stdlib.compare a.is_open b.is_open in - if c <> 0 then c - else -- let c = Pervasives.compare a.is_lower b.is_lower in -+ let c = Stdlib.compare a.is_lower b.is_lower in - if c <> 0 then c - else compare_bounds_kind a.kind b.kind - ---- alt-ergo-2.3.0-free/sources/lib/structures/ty.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/structures/ty.ml 2022-02-23 12:57:12.852376945 -0700 -@@ -201,7 +201,7 @@ and shorten_body _ _ = - - let rec compare t1 t2 = - match shorten t1 , shorten t2 with -- | Tvar{ v = v1; _ } , Tvar{ v = v2; _ } -> Pervasives.compare v1 v2 -+ | Tvar{ v = v1; _ } , Tvar{ v = v2; _ } -> Stdlib.compare v1 v2 - | Tvar _, _ -> -1 | _ , Tvar _ -> 1 - | Text(l1, s1) , Text(l2, s2) -> - let c = Hstring.compare s1 s2 in -@@ -234,7 +234,7 @@ let rec compare t1 t2 = - - | Tadt _, _ -> -1 | _ , Tadt _ -> 1 - -- | t1 , t2 -> Pervasives.compare t1 t2 -+ | t1 , t2 -> Stdlib.compare t1 t2 - - - and compare_list l1 l2 = match l1, l2 with -@@ -278,7 +278,7 @@ let rec equal t1 t2 = - | _ -> false - - (*** matching with a substitution mechanism ***) --module M = Map.Make(struct type t=int let compare = Pervasives.compare end) -+module M = Map.Make(struct type t=int let compare = Stdlib.compare end) - type subst = t M.t - - let esubst = M.empty -@@ -602,12 +602,12 @@ let instantiate lvar lty ty = - let union_subst s1 s2 = - M.fold (fun k x s2 -> M.add k x s2) (M.map (apply_subst s2) s1) s2 - --let compare_subst = M.compare Pervasives.compare -+let compare_subst = M.compare Stdlib.compare - --let equal_subst = M.equal Pervasives.(=) -+let equal_subst = M.equal Stdlib.(=) - - module Svty = -- Set.Make(struct type t = int let compare = Pervasives.compare end) -+ Set.Make(struct type t = int let compare = Stdlib.compare end) - - module Set = - Set.Make(struct ---- alt-ergo-2.3.0-free/sources/lib/structures/typed.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/structures/typed.ml 2022-02-23 12:57:12.852376945 -0700 -@@ -369,8 +369,8 @@ let fresh_hypothesis_name = - | _ -> "@L"^(string_of_int !cpt) - - let is_local_hyp s = -- try Pervasives.(=) (String.sub s 0 2) "@L" with Invalid_argument _ -> false -+ try Stdlib.(=) (String.sub s 0 2) "@L" with Invalid_argument _ -> false - - let is_global_hyp s = -- try Pervasives.(=) (String.sub s 0 2) "@H" with Invalid_argument _ -> false -+ try Stdlib.(=) (String.sub s 0 2) "@H" with Invalid_argument _ -> false - ---- alt-ergo-2.3.0-free/sources/lib/structures/xliteral.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/structures/xliteral.ml 2022-02-23 12:57:12.852376945 -0700 -@@ -103,7 +103,7 @@ module Make (X : OrderedType) : S with t - - type t = { at : atom; neg : bool; tpos : int; tneg : int } - -- let compare a1 a2 = Pervasives.compare a1.tpos a2.tpos -+ let compare a1 a2 = Stdlib.compare a1.tpos a2.tpos - let equal a1 a2 = a1.tpos = a2.tpos (* XXX == *) - let hash a1 = a1.tpos - let uid a1 = a1.tpos ---- alt-ergo-2.3.0-free/sources/lib/util/emap.mli.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/emap.mli 2022-02-23 12:57:12.852376945 -0700 -@@ -41,8 +41,8 @@ - struct - type t = int * int - let compare (x0,y0) (x1,y1) = -- match Pervasives.compare x0 x1 with -- 0 -> Pervasives.compare y0 y1 -+ match Stdlib.compare x0 x1 with -+ 0 -> Stdlib.compare y0 y1 - | c -> c - end - -@@ -68,7 +68,7 @@ sig - [f e1 e2] is strictly negative if [e1] is smaller than [e2], - and [f e1 e2] is strictly positive if [e1] is greater than [e2]. - Example: a suitable ordering function is the generic structural -- comparison function {!Pervasives.compare}. *) -+ comparison function {!Stdlib.compare}. *) - end - (** Input signature of the functor {!Map.Make}. *) - ---- alt-ergo-2.3.0-free/sources/lib/util/myUnix.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/myUnix.ml 2022-02-23 12:57:12.852376945 -0700 -@@ -18,7 +18,7 @@ module Default_Unix = struct - let cur_time () = (times()).tms_utime - - let set_timeout ~is_gui timelimit = -- if Pervasives.(<>) timelimit 0. then -+ if Stdlib.(<>) timelimit 0. then - let itimer = - if is_gui then Unix.ITIMER_REAL (* troubles with VIRTUAL *) - else Unix.ITIMER_VIRTUAL ---- alt-ergo-2.3.0-free/sources/lib/util/numbers.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/numbers.ml 2022-02-23 12:57:12.853376946 -0700 -@@ -48,8 +48,8 @@ module Q = struct - else - let v = to_float q in - let w = -- if Pervasives.(<) v min_float then min_float -- else if Pervasives.(>) v max_float then max_float -+ if Stdlib.(<) v min_float then min_float -+ else if Stdlib.(>) v max_float then max_float - else v - in - let flt = if n = 2 then sqrt w else w ** (1. /. float n) in ---- alt-ergo-2.3.0-free/sources/lib/util/options.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/options.ml 2022-02-23 12:57:12.853376946 -0700 -@@ -957,7 +957,7 @@ let (>) (a: int) (b: int) = a > b - let (<=) (a: int) (b: int) = a <= b - let (>=) (a: int) (b: int) = a >= b - --let compare (a: int) (b: int) = Pervasives.compare a b -+let compare (a: int) (b: int) = Stdlib.compare a b - - - (* extra **) ---- alt-ergo-2.3.0-free/sources/lib/util/util.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/util.ml 2022-02-23 12:57:12.853376946 -0700 -@@ -83,7 +83,7 @@ let [@inline always] compare_algebraic s - let r1 = Obj.repr s1 in - let r2 = Obj.repr s2 in - match Obj.is_int r1, Obj.is_int r2 with -- | true, true -> Pervasives.compare s1 s2 (* both constructors without args *) -+ | true, true -> Stdlib.compare s1 s2 (* both constructors without args *) - | true, false -> -1 - | false, true -> 1 - | false, false -> ---- alt-ergo-2.3.0-free/sources/lib/util/util.mli.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/util.mli 2022-02-23 12:57:12.853376946 -0700 -@@ -56,7 +56,7 @@ val string_of_th_ext : theories_extensio - (** - generic function for comparing algebraic data types. - [compare_algebraic a b f] -- - Pervasives.compare a b is used if -+ - Stdlib.compare a b is used if - - *) - val [@inline always] compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int ---- alt-ergo-2.3.0-free/sources/lib/util/zarithNumbers.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/zarithNumbers.ml 2022-02-23 12:57:12.853376946 -0700 -@@ -153,7 +153,7 @@ module Q : NumbersInterface.QSig with mo - let floor t = from_z (Z.fdiv (num t) (den t)) - let ceiling t = from_z (Z.cdiv (num t) (den t)) - let power t n = -- let abs_n = Pervasives.abs n in -+ let abs_n = Stdlib.abs n in - let num_pow = Z.power (num t) abs_n in - let den_pow = Z.power (den t) abs_n in - if n >= 0 then from_zz num_pow den_pow else from_zz den_pow num_pow ---- alt-ergo-2.3.0-free/sources/parsers/parsers.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/parsers/parsers.ml 2022-02-23 12:57:12.853376946 -0700 -@@ -124,7 +124,7 @@ let parse_input_file file = - stdin, Lexing.from_string file_content, false, ext - else - let ext = Filename.extension file in -- if Pervasives.(<>) file "" then -+ if Stdlib.(<>) file "" then - let cin = open_in file in - cin, Lexing.from_channel cin, true, ext - else ---- alt-ergo-2.3.0-free/sources/tools/gui/annoted_ast.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/tools/gui/annoted_ast.ml 2022-02-23 12:57:12.854376946 -0700 +--- alt-ergo-2.3.0-free/sources/tools/gui/annoted_ast.ml.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/tools/gui/annoted_ast.ml 2022-06-18 16:08:13.053310654 -0600 @@ -191,7 +191,7 @@ type annoted_node = module MDep = Map.Make ( struct @@ -508,8 +65,8 @@ )sl l in findtags_aform sl aaf.c acc ---- alt-ergo-2.3.0-free/sources/tools/gui/connected_ast.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/tools/gui/connected_ast.ml 2022-02-23 12:57:12.854376946 -0700 +--- alt-ergo-2.3.0-free/sources/tools/gui/connected_ast.ml.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/tools/gui/connected_ast.ml 2022-06-18 16:08:37.469375133 -0600 @@ -388,7 +388,7 @@ let rec unquantify_aform (buffer:sbuffer List.fold_left (fun (nbv, used, goal_used, ve, uplet, lets) v -> let ((s, _) as v'), e = List.hd ve in @@ -537,8 +94,8 @@ commit_tags_buffer sbuf | _ -> assert false end ---- alt-ergo-2.3.0-free/sources/tools/gui/main_gui.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/tools/gui/main_gui.ml 2022-02-23 12:57:12.854376946 -0700 +--- alt-ergo-2.3.0-free/sources/tools/gui/main_gui.ml.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/tools/gui/main_gui.ml 2022-06-18 16:09:14.324472461 -0600 @@ -151,7 +151,7 @@ let save_session envs = let save_dialog cancel envs () = diff --git a/alt-ergo-stdlib-shims.patch b/alt-ergo-stdlib-shims.patch new file mode 100644 index 0000000..5f266df --- /dev/null +++ b/alt-ergo-stdlib-shims.patch @@ -0,0 +1,42 @@ +--- alt-ergo-2.3.0-free/sources/alt-ergo-lib-free.opam.orig 2022-05-20 03:15:57.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/alt-ergo-lib-free.opam 2022-06-18 16:35:11.569523676 -0600 +@@ -16,7 +16,6 @@ depends: [ + "ocplib-simplex" {>= "0.4" } + "zarith" + "seq" +- "stdlib-shims" + ] + conflicts: [ + "alt-ergo" +--- alt-ergo-2.3.0-free/sources/alt-ergo-parsers-free.opam.orig 2022-05-20 03:16:01.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/alt-ergo-parsers-free.opam 2022-06-18 16:35:52.177624279 -0600 +@@ -16,7 +16,6 @@ depends: [ + "psmt2-frontend" { >= "0.2" & < "0.4" } + "camlzip" + "menhir" { < "20210310" } +- "stdlib-shims" + ] + conflicts: [ + "alt-ergo-parsers" +--- alt-ergo-2.3.0-free/sources/lib/dune.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/dune 2022-06-18 16:34:45.634456726 -0600 +@@ -9,7 +9,7 @@ + (public_name alt-ergo-lib) + + ; external dependencies +- (libraries seq unix num str zarith dynlink ocplib-simplex stdlib-shims) ++ (libraries seq unix num str zarith dynlink ocplib-simplex) + + ; .mli only modules *also* need to be in this field + (modules_without_implementation matching_types numbersInterface sig sig_rel) +--- alt-ergo-2.3.0-free/sources/parsers/dune.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/parsers/dune 2022-06-18 16:36:07.177661183 -0600 +@@ -14,7 +14,7 @@ + (library + (name AltErgoParsers) + (public_name alt-ergo-parsers) +- (libraries camlzip dynlink psmt2-frontend alt-ergo-lib stdlib-shims) ++ (libraries camlzip dynlink psmt2-frontend alt-ergo-lib) + (modules + ; common + Parsers Parsers_loader MyZip diff --git a/alt-ergo.spec b/alt-ergo.spec index 0c15271..ba5b1e4 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,22 +8,39 @@ %global debug_package %{nil} %endif +# The major and minor releases contain a full tarball. Patch releases, however, +# contain only the parts that have changed, typically just the sources +# directory. Use this to set up everything up appropriately. +%global minorver 2.3 +%global patchrel 3 + Name: alt-ergo -Version: 2.3.0 -Release: 4%{?dist} +Version: %{minorver}.%{patchrel} +Release: 1%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 URL: https://alt-ergo.ocamlpro.com/ -Source0: https://alt-ergo.ocamlpro.com/http/%{name}-free-%{version}/%{name}-free-%{version}.tar.gz +# The patch releases contain only the sources directory. The other files come +# from the minor releases. +Source0: https://alt-ergo.ocamlpro.com/http/%{name}-free-%{minorver}.0/%{name}-free-%{minorver}.0.tar.gz +%if 0%{?patchrel} > 0 +Source1: https://alt-ergo.ocamlpro.com/http/%{name}-free-%{version}/%{name}-free-%{version}.tar.gz +%endif # Created with gimp from official upstream icon -Source1: %{name}-icons.tar.xz -Source2: %{name}.desktop -Source3: %{name}.metainfo.xml +Source2: %{name}-icons.tar.xz +Source3: %{name}.desktop +Source4: %{name}.metainfo.xml # Do not use the deprecated Pervasives interface Patch0: %{name}-pervasives.patch # Adapt to recent changes in psmt2-frontend Patch1: %{name}-psmt2-frontend.patch +# Temporarily use the menhir table backend instead of the code backend for the +# AB plugin. Menhir is unable to infer types with the current code and layout. +# Check each new release to see if this is still necessary. +Patch2: %{name}-menhir.patch +# Fedora does not have or need the forward compatibility stdlib-shims package +Patch3: %{name}-stdlib-shims.patch BuildRequires: appstream BuildRequires: desktop-file-utils @@ -105,10 +122,17 @@ This package contains development files needed to build applications that use the Alt-Ergo library. %prep -%autosetup -n %{name}-%{version}-free -p1 -a 1 +%autosetup -n %{name}-%{minorver}.0-free -N -a 2 +%if 0%{?patchrel} > 0 +# See above. Replace the minor release sources with the patch release sources. +rm -rf sources +tar xf %{SOURCE1} +%endif + +%autopatch -p1 cd sources -cp -p %{SOURCE2} com.ocamlpro.%{name}.desktop +cp -p %{SOURCE3} com.ocamlpro.%{name}.desktop # Unzip an example cd examples/AB-Why3-plugin @@ -119,7 +143,7 @@ cd - %build # This is not an autoconf-generated script. Do NOT use %%configure. cd sources -./configure --prefix=%{_prefix} --libdir=%{_libdir}/ocaml --sharedir=%{_datadir} +./configure --prefix=%{_prefix} --libdir=%{_libdir}/ocaml --sharedir=%{_libdir}/ocaml %make_build %make_build doc @@ -140,11 +164,10 @@ rm -fr %{buildroot}%{_prefix}/doc mkdir -p %{buildroot}%{_mandir}/man1 cp -p doc/alt-ergo.1 %{buildroot}%{_mandir}/man1 -# Make the plugins directory -mkdir -p %{buildroot}%{_libdir}/ocaml/%{name}/plugins - -# Install the preludes -cp -a preludes %{buildroot}%{_libdir}/ocaml/%{name} +# The install target in the Makefile puts these in the wrong place +mv %{buildroot}%{_datadir}/alt-ergo/{plugins,preludes} \ + %{buildroot}%{_libdir}/ocaml/alt-ergo +rmdir %{buildroot}%{_datadir}/alt-ergo # Install the gtksourceview file mkdir -p %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs @@ -158,7 +181,7 @@ desktop-file-install --dir %{buildroot}%{_datadir}/applications \ # Install the AppData file mkdir -p %{buildroot}%{_metainfodir} -install -pm 644 %{SOURCE3} \ +install -pm 644 %{SOURCE4} \ %{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml appstreamcli validate --no-net \ %{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml @@ -178,6 +201,7 @@ dune runtest --release %{_bindir}/%{name} %{_mandir}/man1/alt-ergo.1.* %{_libdir}/ocaml/%{name}/ +%{_libdir}/ocaml/%{name}-free/ %files gui %{_bindir}/altgr-ergo @@ -195,6 +219,7 @@ dune runtest --release %ifarch %{ocaml_native_compiler} %{_libdir}/ocaml/%{name}-parsers/*.cmxs %endif +%{_libdir}/ocaml/%{name}-parsers-free/ %files -n ocaml-%{name}-parsers-devel %{_libdir}/ocaml/%{name}-parsers/dune-package @@ -216,6 +241,7 @@ dune runtest --release %ifarch %{ocaml_native_compiler} %{_libdir}/ocaml/%{name}-lib/*.cmxs %endif +%{_libdir}/ocaml/%{name}-lib-free/ %files -n ocaml-%{name}-lib-devel %doc sources/_build/default/_doc/* @@ -231,6 +257,11 @@ dune runtest --release %{_libdir}/ocaml/%{name}-lib/*.cmti %changelog +* Mon Jun 20 2022 Jerry James - 2.3.3-1 +- Version 2.3.3 +- Add -menhir patch to fix FTBFS +- Add -stdlib-shims patch since Fedora does not need stdlib-shims + * Mon Feb 28 2022 Jerry James - 2.3.0-4 - Switch to the correct tarball - Drop unneeded ocaml-findlib BR diff --git a/sources b/sources index 56b9730..2e808e5 100644 --- a/sources +++ b/sources @@ -1,2 +1,3 @@ SHA512 (alt-ergo-free-2.3.0.tar.gz) = e15efc6bbde59065c6ccaf1ef2f8158b8b9be4b00b2c2365e5eeb7d7114be72c47c813fc06880a6278edd7e288f24ef4588c88e0630d9bda9378a3eda3fd07ca +SHA512 (alt-ergo-free-2.3.3.tar.gz) = 0dc056c02c8ffdeb9eeaa127dd204d30a0ee95ffe38aa3f1a608b17019f377ea6520ccfc9cb09b109deac5f19e7e695b7e6ec18db969843312cfb17f3950c9ba SHA512 (alt-ergo-icons.tar.xz) = cb2e93bab3359f6f198e80e3e68840ed4b25a213b61f388a2de8abc299fd3c89240f64f610290ac89e6005088c484b2718a68ec18063076f73d7871a38ee038f