diff --git a/alt-ergo-dune3.patch b/alt-ergo-dune3.patch
new file mode 100644
index 0000000..cb875a4
--- /dev/null
+++ b/alt-ergo-dune3.patch
@@ -0,0 +1,29 @@
+--- alt-ergo-2.3.0-free/sources/configure.ml.orig 2022-05-20 01:34:55.000000000 -0600
++++ alt-ergo-2.3.0-free/sources/configure.ml 2022-07-05 16:42:35.856375154 -0600
+@@ -139,26 +139,6 @@ let () =
+ Format.eprintf "ERROR: Couldn't find dune in env@.";
+ exit 1
+
+-(* run dune to check that dependencies are installed *)
+-let () =
+- let p_opt = match !pkg with
+- | "" -> ""
+- | s -> Format.asprintf "-p %s" s
+- in
+- let cmd = Format.asprintf
+- "dune external-lib-deps --display=quiet --missing %s @install"
+- p_opt
+- in
+- let ch = Unix.open_process_in cmd in
+- let _ = read_all ch in
+- let res = Unix.close_process_in ch in
+- match res with
+- | Unix.WEXITED 0 ->
+- Format.printf "All deps are installed.@."
+- | _ ->
+- (* dune already prints the missing libs on stderr *)
+- exit 2
+-
+ let () =
+ Format.printf "Good to go !@."
+
diff --git a/alt-ergo-forward-compat.patch b/alt-ergo-forward-compat.patch
new file mode 100644
index 0000000..b3be679
--- /dev/null
+++ b/alt-ergo-forward-compat.patch
@@ -0,0 +1,64 @@
+--- 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-07-05 16:40:03.983955825 -0600
+@@ -15,8 +15,6 @@ depends: [
+ "num"
+ "ocplib-simplex" {>= "0.4" }
+ "zarith"
+- "seq"
+- "stdlib-shims"
+ ]
+ conflicts: [
+ "alt-ergo"
+--- alt-ergo-2.3.0-free/sources/alt-ergo-lib.opam.orig 2022-05-20 01:34:55.000000000 -0600
++++ alt-ergo-2.3.0-free/sources/alt-ergo-lib.opam 2022-07-05 16:47:56.113259397 -0600
+@@ -15,8 +15,6 @@ depends: [
+ "num"
+ "ocplib-simplex" {>= "0.4" }
+ "zarith"
+- "seq"
+- "stdlib-shims"
+ ]
+ conflicts: [
+ "alt-ergo-free"
+--- 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/alt-ergo-parsers.opam.orig 2022-05-20 01:34:55.000000000 -0600
++++ alt-ergo-2.3.0-free/sources/alt-ergo-parsers.opam 2022-07-05 16:39:33.254870985 -0600
+@@ -16,7 +16,6 @@ depends: [
+ "psmt2-frontend" { >= "0.2" }
+ "camlzip"
+ "menhir"
+- "stdlib-shims"
+ ]
+ homepage: "http://alt-ergo.ocamlpro.com/"
+ dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
+--- 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-07-05 16:50:35.778700249 -0600
+@@ -9,7 +9,7 @@
+ (public_name alt-ergo-lib)
+
+ ; external dependencies
+- (libraries seq unix num str zarith dynlink ocplib-simplex stdlib-shims)
++ (libraries 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-inline-error.patch b/alt-ergo-inline-error.patch
new file mode 100644
index 0000000..ccb8356
--- /dev/null
+++ b/alt-ergo-inline-error.patch
@@ -0,0 +1,26 @@
+Fixes these errors:
+
+File "lib/util/util.mli", line 62, characters 6-12:
+62 | val [@inline always] compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int
+ ^^^^^^
+Error (warning 53 [misplaced-attribute]): the "inline" attribute cannot appear in this context
+
+File "lib/util/util.mli", line 64, characters 6-12:
+64 | val [@inline always] cmp_lists: 'a list -> 'a list -> ('a -> 'a -> int) -> int
+ ^^^^^^
+Error (warning 53 [misplaced-attribute]): the "inline" attribute cannot appear in this context
+
+--- alt-ergo-2.3.0-free/sources/lib/util/util.mli.orig 2022-05-20 01:34:55.000000000 -0600
++++ alt-ergo-2.3.0-free/sources/lib/util/util.mli 2024-05-05 11:41:32.415674847 -0600
+@@ -59,9 +59,9 @@ val string_of_th_ext : theories_extensio
+ - Pervasives.compare a b is used if
+
+ *)
+-val [@inline always] compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int
++val compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int
+
+-val [@inline always] cmp_lists: 'a list -> 'a list -> ('a -> 'a -> int) -> int
++val cmp_lists: 'a list -> 'a list -> ('a -> 'a -> int) -> int
+
+ type matching_env =
+ {
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.metainfo.xml b/alt-ergo.metainfo.xml
index cdb417e..cff34da 100644
--- a/alt-ergo.metainfo.xml
+++ b/alt-ergo.metainfo.xml
@@ -20,15 +20,15 @@
com.ocamlpro.alt-ergo.desktop
- http://jjames.fedorapeople.org/alt-ergo/altgr-ergo-screenshot.png
+ https://jjames.fedorapeople.org/alt-ergo/altgr-ergo-screenshot.png
Basic Alt-Ergo usage
- loganjerry@gmail.com
+ alt-ergo-maintainers@fedoraproject.org
https://alt-ergo.ocamlpro.com/
https://github.com/OCamlPro/alt-ergo/issues
https://alt-ergo.ocamlpro.com/#services
-
+
altgr-ergo
diff --git a/alt-ergo.spec b/alt-ergo.spec
index 0c15271..3adb6d8 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -1,33 +1,56 @@
+# OCaml packages not built on i686 since OCaml 5 / Fedora 39.
+ExcludeArch: %{ix86}
+
# rpmlint "no-binary" error is not really an error - see:
# https://www.redhat.com/archives/fedora-packaging/2008-August/msg00017.html
# and ocaml-ocamlgraph spec file for a discussion of this issue.
-%undefine _package_note_flags
-
-%ifnarch %{ocaml_native_compiler}
-%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 appropriately.
+%global minorver 2.3
+%global patchrel 3
Name: alt-ergo
-Version: 2.3.0
-Release: 4%{?dist}
+Version: %{minorver}.%{patchrel}
+Release: 30%{?dist}
Summary: Automated theorem prover including linear arithmetic
-License: ASL 2.0
+# The top-level license files apply to the non-free main distribution of
+# alt-ergo. The alt-ergo-free distribution, which we package, is distributed
+# with the CeCILL-C license, as noted on the website and also in
+# sources/tools/gui/main_gui.ml.
+# The AB-Why3 plugin is LGPL-2.1-only WITH OCaml-LGPL-linking-exception
+License: CECILL-C AND LGPL-2.1-only WITH OCaml-LGPL-linking-exception
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 need the forward compatibility seq and stdlib-shims packages
+Patch3: %{name}-forward-compat.patch
+# Dune 3 eliminated the external-lib-deps command
+Patch4: %{name}-dune3.patch
+# Avoid errors due to misplaced inline attributes
+Patch5: %{name}-inline-error.patch
-BuildRequires: appstream
BuildRequires: desktop-file-utils
BuildRequires: gtksourceview2-devel
+BuildRequires: libappstream-glib
BuildRequires: make
BuildRequires: ocaml >= 4.04.0
BuildRequires: ocaml-dune
@@ -35,80 +58,95 @@ BuildRequires: ocaml-lablgtk-devel
BuildRequires: ocaml-menhir
BuildRequires: ocaml-num-devel
BuildRequires: ocaml-ocplib-simplex-devel >= 0.4
-BuildRequires: ocaml-odoc
BuildRequires: ocaml-psmt2-frontend-devel >= 0.2
-BuildRequires: ocaml-seq-devel
BuildRequires: ocaml-zarith-devel
BuildRequires: ocaml-zip-devel
Requires: ocaml-alt-ergo-parsers%{?_isa} = %{version}-%{release}
-%global _desc %{expand:
-Alt-Ergo is an automated theorem prover implemented in OCaml. It is
-based on CC(X) - a congruence closure algorithm parameterized by an
-equational theory X. This algorithm is reminiscent of the Shostak
-algorithm. Currently CC(X) is instantiated by the theory of linear
-arithmetics. Alt-Ergo also contains a home made SAT-solver and an
-instantiation mechanism by which it fully supports quantifiers.}
+%global _desc %{expand:Alt-Ergo is an automated theorem prover implemented in OCaml. It is based on
+CC(X) - a congruence closure algorithm parameterized by an equational theory
+X. This algorithm is reminiscent of the Shostak algorithm. Currently CC(X)
+is instantiated by the theory of linear arithmetics. Alt-Ergo also contains a
+home made SAT-solver and an instantiation mechanism by which it fully supports
+quantifiers.}
-%description %_desc
+%description
+%_desc
%package gui
Summary: Graphical front end for Alt-Ergo
+License: CECILL-C
Requires: %{name}%{?_isa} = %{version}-%{release}
Requires: gtksourceview2
Requires: hicolor-icon-theme
-%description gui %_desc
+%description gui
+%_desc
-This package contains a graphical front end for the Alt-Ergo theorem
-prover.
+This package contains a graphical front end for the Alt-Ergo theorem prover.
%package -n ocaml-alt-ergo-parsers
Summary: Parser library used by the Alt-Ergo SMT solver
+License: CECILL-C
Requires: ocaml-alt-ergo-lib%{?_isa} = %{version}-%{release}
-%description -n ocaml-alt-ergo-parsers %_desc
+%description -n ocaml-alt-ergo-parsers
+%_desc
This package contains the parser library used by the Alt-Ergo SMT solver.
%package -n ocaml-alt-ergo-parsers-devel
Summary: Development files for ocaml-alt-ergo-parsers
+License: CECILL-C
Requires: ocaml-alt-ergo-parsers%{?_isa} = %{version}-%{release}
Requires: ocaml-alt-ergo-lib-devel%{?_isa} = %{version}-%{release}
Requires: ocaml-psmt2-frontend-devel%{?_isa}
Requires: ocaml-zip-devel%{?_isa}
-%description -n ocaml-alt-ergo-parsers-devel %_desc
+%description -n ocaml-alt-ergo-parsers-devel
+%_desc
-This package contains development files needed to build applications
-that use the Alt-Ergo parser library.
+This package contains development files needed to build applications that use
+the Alt-Ergo parser library.
%package -n ocaml-alt-ergo-lib
Summary: Automated theorem prover library
+License: CECILL-C
-%description -n ocaml-alt-ergo-lib %_desc
+%description -n ocaml-alt-ergo-lib
+%_desc
This package is the core of Alt-Ergo as an OCaml library.
%package -n ocaml-alt-ergo-lib-devel
Summary: Development files for ocaml-alt-ergo-lib
+License: CECILL-C
Requires: ocaml-alt-ergo-lib%{?_isa} = %{version}-%{release}
Requires: ocaml-num-devel%{?_isa}
Requires: ocaml-ocplib-simplex-devel%{?_isa}
-Requires: ocaml-seq-devel%{?_isa}
Requires: ocaml-zarith-devel%{?_isa}
-%description -n ocaml-alt-ergo-lib-devel %_desc
+%description -n ocaml-alt-ergo-lib-devel
+%_desc
-This package contains development files needed to build applications
-that use the Alt-Ergo library.
+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
+
+%conf
cd sources
-cp -p %{SOURCE2} com.ocamlpro.%{name}.desktop
+cp -p %{SOURCE3} com.ocamlpro.%{name}.desktop
# Unzip an example
cd examples/AB-Why3-plugin
@@ -116,22 +154,24 @@ unzip p4_34.why.zip
rm p4_34.why.zip
cd -
-%build
+%ifnarch %{ocaml_native_compiler}
+# Do not require native plugins
+sed -i '/cmxs/d' plugins/{AB-Why3,fm-simplex}/dune
+%endif
+
# This is not an autoconf-generated script. Do NOT use %%configure.
+./configure --prefix=%{_prefix} --libdir=%{ocamldir} --sharedir=%{ocamldir}
+
+%build
cd sources
-./configure --prefix=%{_prefix} --libdir=%{_libdir}/ocaml --sharedir=%{_datadir}
%make_build
-%make_build doc
%install
cd sources
%make_install
-# We do not want the dune markers
-find _build/default/_doc/_html -name .dune-keep -delete
-
# We do not want the ml files
-find %{buildroot}%{_libdir}/ocaml -name \*.ml -delete
+find %{buildroot}%{ocamldir} -name \*.ml -delete
# We install the documentation with the doc macro
rm -fr %{buildroot}%{_prefix}/doc
@@ -140,11 +180,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}%{ocamldir}/alt-ergo
+rmdir %{buildroot}%{_datadir}/alt-ergo
# Install the gtksourceview file
mkdir -p %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs
@@ -158,9 +197,9 @@ 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 \
+appstream-util validate-relax --nonet \
%{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml
# Install the icons
@@ -168,69 +207,195 @@ cd -
mkdir -p %{buildroot}%{_datadir}/icons
cp -a icons %{buildroot}%{_datadir}/icons/hicolor
+# Put something interesting into the META files
+cat > %{buildroot}%{ocamldir}/alt-ergo/META << EOF
+version = "%{version}"
+description = "Automated theorem prover including linear arithmetic"
+requires = ""
+EOF
+rm %{buildroot}%{ocamldir}/{alt-ergo-free,altgr-ergo}/META
+ln %{buildroot}%{ocamldir}/alt-ergo/META \
+ %{buildroot}%{ocamldir}/alt-ergo-free/META
+ln %{buildroot}%{ocamldir}/alt-ergo/META \
+ %{buildroot}%{ocamldir}/altgr-ergo/META
+
%check
cd sources
-dune runtest --release
+%dune_check
%files
%doc README.md sources/CHANGES sources/examples publications/*.pdf
-%license COPYING.md LICENSE.md License.OCamlPro
%{_bindir}/%{name}
%{_mandir}/man1/alt-ergo.1.*
-%{_libdir}/ocaml/%{name}/
+%{ocamldir}/%{name}/
+%{ocamldir}/%{name}-free/
%files gui
%{_bindir}/altgr-ergo
%{_datadir}/applications/com.ocamlpro.%{name}.desktop
%{_datadir}/gtksourceview-2.0/language-specs/%{name}.lang
%{_datadir}/icons/hicolor/*/apps/%{name}.png
-%{_libdir}/ocaml/altgr-ergo/
+%{ocamldir}/altgr-ergo/
%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml
%files -n ocaml-%{name}-parsers
-%dir %{_libdir}/ocaml/%{name}-parsers/
-%{_libdir}/ocaml/%{name}-parsers/META
-%{_libdir}/ocaml/%{name}-parsers/*.cma
-%{_libdir}/ocaml/%{name}-parsers/*.cmi
+%dir %{ocamldir}/%{name}-parsers/
+%{ocamldir}/%{name}-parsers/META
+%{ocamldir}/%{name}-parsers/*.cma
+%{ocamldir}/%{name}-parsers/*.cmi
%ifarch %{ocaml_native_compiler}
-%{_libdir}/ocaml/%{name}-parsers/*.cmxs
+%{ocamldir}/%{name}-parsers/*.cmxs
%endif
+%{ocamldir}/%{name}-parsers-free/
%files -n ocaml-%{name}-parsers-devel
-%{_libdir}/ocaml/%{name}-parsers/dune-package
-%{_libdir}/ocaml/%{name}-parsers/opam
+%{ocamldir}/%{name}-parsers/dune-package
+%{ocamldir}/%{name}-parsers/opam
%ifarch %{ocaml_native_compiler}
-%{_libdir}/ocaml/%{name}-parsers/*.a
-%{_libdir}/ocaml/%{name}-parsers/*.cmx
-%{_libdir}/ocaml/%{name}-parsers/*.cmxa
+%{ocamldir}/%{name}-parsers/*.a
+%{ocamldir}/%{name}-parsers/*.cmx
+%{ocamldir}/%{name}-parsers/*.cmxa
%endif
-%{_libdir}/ocaml/%{name}-parsers/*.mli
-%{_libdir}/ocaml/%{name}-parsers/*.cmt
-%{_libdir}/ocaml/%{name}-parsers/*.cmti
+%{ocamldir}/%{name}-parsers/*.mli
+%{ocamldir}/%{name}-parsers/*.cmt
+%{ocamldir}/%{name}-parsers/*.cmti
%files -n ocaml-%{name}-lib
-%dir %{_libdir}/ocaml/%{name}-lib/
-%{_libdir}/ocaml/%{name}-lib/META
-%{_libdir}/ocaml/%{name}-lib/*.cma
-%{_libdir}/ocaml/%{name}-lib/*.cmi
+%dir %{ocamldir}/%{name}-lib/
+%license LGPL-License.txt LICENSE.md License.OCamlPro
+%{ocamldir}/%{name}-lib/META
+%{ocamldir}/%{name}-lib/*.cma
+%{ocamldir}/%{name}-lib/*.cmi
%ifarch %{ocaml_native_compiler}
-%{_libdir}/ocaml/%{name}-lib/*.cmxs
+%{ocamldir}/%{name}-lib/*.cmxs
%endif
+%{ocamldir}/%{name}-lib-free/
%files -n ocaml-%{name}-lib-devel
-%doc sources/_build/default/_doc/*
-%{_libdir}/ocaml/%{name}-lib/dune-package
-%{_libdir}/ocaml/%{name}-lib/opam
+%{ocamldir}/%{name}-lib/dune-package
+%{ocamldir}/%{name}-lib/opam
+%{ocamldir}/%{name}-lib/frontend/
+%{ocamldir}/%{name}-lib/reasoners/
+%{ocamldir}/%{name}-lib/structures/
+%{ocamldir}/%{name}-lib/util/
%ifarch %{ocaml_native_compiler}
-%{_libdir}/ocaml/%{name}-lib/*.a
-%{_libdir}/ocaml/%{name}-lib/*.cmx
-%{_libdir}/ocaml/%{name}-lib/*.cmxa
+%{ocamldir}/%{name}-lib/*.a
+%{ocamldir}/%{name}-lib/*.cmx
+%{ocamldir}/%{name}-lib/*.cmxa
%endif
-%{_libdir}/ocaml/%{name}-lib/*.mli
-%{_libdir}/ocaml/%{name}-lib/*.cmt
-%{_libdir}/ocaml/%{name}-lib/*.cmti
+%{ocamldir}/%{name}-lib/*.cmt
+%{ocamldir}/%{name}-lib/*.cmti
%changelog
+* Fri Jan 16 2026 Fedora Release Engineering - 2.3.3-30
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild
+
+* Tue Oct 14 2025 Richard W.M. Jones - 2.3.3-29
+- OCaml 5.4.0 rebuild
+
+* Tue Sep 16 2025 Jerry James - 2.3.3-28
+- Rebuild for ocaml-menhir 20250912
+
+* Fri Sep 05 2025 Jerry James - 2.3.3-27
+- Rebuild for ocaml-menhir 20250903
+
+* Wed Jul 23 2025 Fedora Release Engineering - 2.3.3-26
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild
+
+* Fri Jul 11 2025 Jerry James - 2.3.3-25
+- Rebuild to fix OCaml dependencies
+
+* Thu Jan 16 2025 Fedora Release Engineering - 2.3.3-24
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild
+
+* Thu Jan 9 2025 Jerry James - 2.3.3-23
+- OCaml 5.3.0 rebuild for Fedora 42
+- Correct License fields from Apache-2.0 to CECILL-C
+- Do configuration steps in %%conf
+
+* Mon Aug 5 2024 Jerry James - 2.3.3-22
+- Rebuild for ocaml-menhir 20240715 and ocaml-zip 1.12
+
+* Wed Jul 17 2024 Fedora Release Engineering - 2.3.3-21
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild
+
+* Tue Jul 16 2024 Jerry James - 2.3.3-20
+- Rebuild for ocaml-zarith 1.14
+
+* Wed Jun 19 2024 Richard W.M. Jones - 2.3.3-19
+- OCaml 5.2.0 ppc64le fix
+
+* Wed May 29 2024 Richard W.M. Jones - 2.3.3-18
+- OCaml 5.2.0 for Fedora 41
+
+* Thu May 23 2024 Jerry James - 2.3.3-17
+- Add patch to fix misplaced inline attributes
+
+* Fri Feb 2 2024 Jerry James - 2.3.3-17
+- Rebuild for changed ocamlx(Dynlink) hash
+
+* Mon Jan 22 2024 Fedora Release Engineering - 2.3.3-16
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
+
+* Fri Jan 19 2024 Fedora Release Engineering - 2.3.3-15
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
+
+* Tue Jan 2 2024 Jerry James - 2.3.3-14
+- Rebuild for ocaml-num and ocaml-menhir 20231231
+
+* Mon Dec 18 2023 Richard W.M. Jones - 2.3.3-13
+- OCaml 5.1.1 + s390x code gen fix for Fedora 40
+
+* Tue Dec 12 2023 Richard W.M. Jones - 2.3.3-12
+- OCaml 5.1.1 rebuild for Fedora 40
+
+* Thu Oct 05 2023 Richard W.M. Jones - 2.3.3-11
+- OCaml 5.1 rebuild for Fedora 40
+
+* Thu Jul 27 2023 Jerry James - 2.3.3-10
+- Rebuild for ocaml-zarith 1.13
+
+* Wed Jul 19 2023 Fedora Release Engineering - 2.3.3-9
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
+
+* Tue Jul 18 2023 Jerry James - 2.3.3-8
+- Validate appdata with appstream-util
+
+* Wed Jul 12 2023 Richard W.M. Jones - 2.3.3-8
+- OCaml 5.0 rebuild for Fedora 39
+
+* Mon Jul 10 2023 Jerry James - 2.3.3-7
+- OCaml 5.0.0 rebuild
+
+* Fri Mar 24 2023 Jerry James - 2.3.3-6
+- Dune 3.7.0 changed the install location of mli files
+
+* Tue Jan 24 2023 Richard W.M. Jones - 2.3.3-5
+- Rebuild OCaml packages for F38
+
+* Wed Jan 18 2023 Fedora Release Engineering - 2.3.3-4
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
+
+* Thu Aug 11 2022 Jerry James - 2.3.3-3
+- Convert License tag to SPDX
+- Note that the AB plugin has a different license
+
+* Wed Jul 20 2022 Fedora Release Engineering - 2.3.3-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
+
+* Tue Jul 5 2022 Jerry James - 2.3.3-2
+- Patch out uses of the dune external-lib-deps command
+- Patch out references to the seq forward compatibility module
+- Use new OCaml macros
+
+* 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
+
+* Sun Jun 19 2022 Richard W.M. Jones - 2.3.0-5
+- OCaml 4.14.0 rebuild
+
* 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