Version 2.3.3.

- Add -menhir patch to fix FTBFS. - Add -stdlib-shims patch since Fedora does not need stdlib-shims.
2022-06-21 09:17:10 -06:00
5 changed files with 113 additions and 464 deletions
--- a/alt-ergo-menhir.patch
+++ 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)
+ )
+ 
--- 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 () =
--- a/alt-ergo-stdlib-shims.patch
+++ 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
--- 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 <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 2.3.0-4
 - Switch to the correct tarball
 - Drop unneeded ocaml-findlib BR
--- a/1
+++ b/1
@ -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