diff --git a/README.md b/README.md
deleted file mode 100644
index fa65fbb..0000000
--- a/README.md
+++ /dev/null
@@ -1,9 +0,0 @@
-# alt-ergo
-
-[Alt-Ergo](https://alt-ergo.ocamlpro.com/) 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.
diff --git a/alt-ergo-1.30-use-pic.patch b/alt-ergo-1.30-use-pic.patch
new file mode 100644
index 0000000..71d6ad0
--- /dev/null
+++ b/alt-ergo-1.30-use-pic.patch
@@ -0,0 +1,19 @@
+--- alt-ergo-1.30.old/Makefile.users 2017-11-09 09:55:47.337871409 +0000
++++ alt-ergo-1.30/Makefile.users 2017-11-09 10:00:52.374639872 +0000
+@@ -140,14 +140,14 @@
+ $(OCAMLC) $(BFLAGS) -o $@ $(BIBBYTE) $^
+
+ $(NAME).opt: $(MAINCMX)
+- $(OCAMLOPT) $(OFLAGS) -o $@ $(BIBOPT) $^
++ $(OCAMLOPT) $(OFLAGS) -runtime-variant _pic -o $@ $(BIBOPT) $^
+
+ ####
+ $(GUINAME).byte: $(GUICMO)
+ $(OCAMLC) $(BFLAGS) -o $(GUINAME).byte $(BIBBYTE) $(BIBGUIBYTE) $^
+
+ $(GUINAME).opt: $(GUICMX)
+- $(OCAMLOPT) $(OFLAGS) -o $(GUINAME).opt $(BIBOPT) $(BIBGUIOPT) $^
++ $(OCAMLOPT) $(OFLAGS) -runtime-variant _pic -o $(GUINAME).opt $(BIBOPT) $(BIBGUIOPT) $^
+
+ ifeq ($(ENABLEGUI),yes)
+ gui: $(GUINAME).$(OCAMLBEST)
diff --git a/alt-ergo-dune3.patch b/alt-ergo-dune3.patch
deleted file mode 100644
index cb875a4..0000000
--- a/alt-ergo-dune3.patch
+++ /dev/null
@@ -1,29 +0,0 @@
---- 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
deleted file mode 100644
index b3be679..0000000
--- a/alt-ergo-forward-compat.patch
+++ /dev/null
@@ -1,64 +0,0 @@
---- 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
deleted file mode 100644
index ccb8356..0000000
--- a/alt-ergo-inline-error.patch
+++ /dev/null
@@ -1,26 +0,0 @@
-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
deleted file mode 100644
index 4ab3e45..0000000
--- a/alt-ergo-menhir.patch
+++ /dev/null
@@ -1,18 +0,0 @@
---- 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 bd72f54..b782e21 100644
--- a/alt-ergo-pervasives.patch
+++ b/alt-ergo-pervasives.patch
@@ -1,22 +1,416 @@
---- alt-ergo-2.3.0-free/extra/ocpChecker.ml.orig 2021-06-29 06:08:30.000000000 -0600
-+++ alt-ergo-2.3.0-free/extra/ocpChecker.ml 2022-02-23 12:58:05.976390283 -0700
-@@ -45,10 +45,10 @@ let update_file file lines =
- exit 2
+--- alt-ergo-2.2.0/lib/frontend/parsers.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/frontend/parsers.ml 2021-01-29 16:42:13.025134465 -0700
+@@ -100,7 +100,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.2.0/lib/frontend/triggers.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/frontend/triggers.ml 2021-01-29 16:15:57.819513468 -0700
+@@ -33,7 +33,7 @@ module Sy = Symbols
+ type polarity = Pos | Neg
+
+ module Vterm = Sy.Set
+-module Vtype = Set.Make(struct type t=int let compare=Pervasives.compare end)
++module Vtype = Set.Make(struct type t=int let compare=Stdlib.compare end)
+
+ module STRS = Set.Make(
+ struct
+@@ -50,12 +50,12 @@ module STRS = Set.Make(
+ let c=compare_term a1 a2 in if c=0 then compare_term b1 b2 else c
+ else c
+ | TTconst (Treal r1) , TTconst (Treal r2) -> Num.compare_num r1 r2
+- | x , y -> Pervasives.compare x y
++ | x , y -> Stdlib.compare x y
+ and compare_list l1 l2 = match l1,l2 with
+ [] , _ -> -1
+ | _ , [] -> 1
+ | x::l1 , y::l2 ->
+- let c = Pervasives.compare x y in if c=0 then compare_list l1 l2 else c
++ let c = Stdlib.compare x y in if c=0 then compare_list l1 l2 else c
+
+ let compare (t1,_,_) (t2,_,_) = compare_term t1 t2
+ end)
+@@ -75,7 +75,7 @@ let compare_tconstant c1 c2 =
+ | Tbitv s1, Tbitv s2 -> String.compare s1 s2
+ | Tbitv s1, _ -> 1
+ | _, Tbitv s2 -> -1
+- | _ -> Pervasives.compare c1 c2
++ | _ -> Stdlib.compare c1 c2
+
+ let rec depth_tterm t =
+ match t.c.tt_desc with
+@@ -153,7 +153,7 @@ let rec compare_tterm t1 t2 =
+
+ | TTinInterval (e1, a1, b1, c1, d1), TTinInterval (e2, a2, b2, c2, d2) ->
+ let c = compare_tterm e1 e2 in
+- if c <> 0 then c else Pervasives.compare (a1, b1, c1, d1) (a2, b2, c2, d2)
++ if c <> 0 then c else Stdlib.compare (a1, b1, c1, d1) (a2, b2, c2, d2)
+
+ | TTinInterval _, _ -> -1
+ | _, TTinInterval _ -> 1
+@@ -191,7 +191,7 @@ let rec compare_tterm t1 t2 =
+ | TTconcat _, _ -> -1
+ | _, TTconcat _ -> 1
+ | TTdot(t1, a1), TTdot(t2,a2) ->
+- let c = Pervasives.compare a1 a2 in
++ let c = Stdlib.compare a1 a2 in
+ if c<>0 then c else
+ compare_tterm t1 t2
+ | TTdot _, _ -> -1
+--- alt-ergo-2.2.0/lib/frontend/typechecker.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/frontend/typechecker.ml 2021-01-29 16:43:14.235096310 -0700
+@@ -36,7 +36,7 @@ module S = Set.Make(String)
+ module Sy = Symbols.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
+
+@@ -78,7 +78,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
+@@ -97,7 +97,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
+@@ -108,7 +108,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
+@@ -769,7 +769,7 @@ and type_form ?(in_theory=false) env f =
+ try
+ List.iter2 Ty.unify lt lt_args;
+ let r =
+- if Pervasives.(=) p "<=" || Pervasives.(=) p "<" then
++ if Stdlib.(=) p "<=" || Stdlib.(=) p "<" then
+ TFatom { c = TAbuilt(Hstring.make p,te_args);
+ annot=new_id ()}
+ else
+@@ -1871,10 +1871,10 @@ let file ld =
+ exit 1
+
+ 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
+
+ let split_goals_aux f l =
+ let _, _, _, ret =
+--- alt-ergo-2.2.0/lib/reasoners/fun_sat.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/reasoners/fun_sat.ml 2021-01-29 16:44:04.915064713 -0700
+@@ -69,7 +69,7 @@ module Make (Th : Theory.S) : Sat_solver
+ SF.fold
+ (fun f mp ->
+ let w = var_inc +. try MF.find f mp with Not_found -> 0. in
+- stable := !stable && Pervasives.(<=) w 1e100;
++ stable := !stable && Stdlib.(<=) w 1e100;
+ MF.add f w mp
+ )(Ex.bj_formulas_of expl) mp
+ in
+@@ -95,9 +95,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
+ (*
+@@ -967,7 +967,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.2.0/lib/reasoners/ite.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/reasoners/ite.ml 2021-01-29 15:13:41.631062282 -0700
+@@ -72,7 +72,7 @@ module Relation (X : ALIEN) (Uf : Uf.S)
+ type t = T.t * bool
+ let compare (a1, b1) (a2, b2) =
+ let c = T.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.2.0/lib/reasoners/satml_frontend.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/reasoners/satml_frontend.ml 2021-01-29 16:16:47.003462456 -0700
+@@ -533,7 +533,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 *)
+@@ -922,7 +922,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 (F.max_term_depth f) in
++ let aux mx f = Stdlib.max mx (F.max_term_depth f) in
+ let max_t = MF.fold (fun f _ mx -> aux mx f) env.gamma 0 in
+ A.Map.fold (fun _ {F.f} mx -> aux mx f) env.ground_preds max_t
+
+--- alt-ergo-2.2.0/lib/reasoners/satml.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/reasoners/satml.ml 2021-01-29 16:44:54.595033743 -0700
+@@ -351,7 +351,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
+
+ let f_filter env i = (Vec.get env.vars i).level < 0
+
+@@ -365,7 +365,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;
+@@ -377,7 +377,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;
+@@ -861,7 +861,7 @@ let compute_facts_for_theory_propagate e
+ let f_sort_db c1 c2 =
+ let sz1 = Vec.size c1.atoms in
+ let sz2 = Vec.size c2.atoms in
+- let c = Pervasives.compare c1.activity c2.activity in
++ let c = Stdlib.compare c1.activity c2.activity in
+ if sz1 = sz2 && c = 0 then 0
+ else
+ if sz1 > 2 && (sz2 = 2 || c < 0) then -1
+--- alt-ergo-2.2.0/lib/structures/formula.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/structures/formula.ml 2021-01-29 16:34:03.946514585 -0700
+@@ -108,8 +108,8 @@ type gformula = {
+ let size (t,_) = t.size
+
+ let compare ((v1,_) as f1) ((v2,_) as f2) =
+- let c = Pervasives.compare (size f1) (size f2) in
+- if c=0 then Pervasives.compare v1.tag v2.tag else c
++ let c = Stdlib.compare (size f1) (size f2) in
++ if c=0 then Stdlib.compare v1.tag v2.tag else c
+
+ let equal (f1,_) (f2,_) =
+ assert ((f1 == f2) == (f1.tag == f2.tag));
+@@ -866,7 +866,7 @@ let label f =
+ | _ -> Hstring.empty
+
+ let label_model h =
+- try Pervasives.(=) (String.sub (Hstring.view h) 0 6) "model:"
++ try Stdlib.(=) (String.sub (Hstring.view h) 0 6) "model:"
+ with Invalid_argument _ -> false
+
+ let is_in_model f =
+--- alt-ergo-2.2.0/lib/structures/literal.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/structures/literal.ml 2021-01-29 15:11:35.935224734 -0700
+@@ -95,7 +95,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.2.0/lib/structures/profiling.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/structures/profiling.ml 2021-01-29 16:41:48.035150044 -0700
+@@ -86,7 +86,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
- Queue.iter (fun line ->
-- Pervasives.output_string cout line;
-- Pervasives.output_string cout "\n"
-+ Stdlib.output_string cout line;
-+ Stdlib.output_string cout "\n"
- )lines;
-- Pervasives.flush cout;
-+ Stdlib.flush cout;
- close_out cout
+ ignore
+ (Unix.setitimer Unix.ITIMER_PROF
+@@ -626,9 +626,9 @@ let switch () =
---- 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 =
+ 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.2.0/lib/structures/symbols.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/structures/symbols.ml 2021-01-29 15:10:23.775316438 -0700
+@@ -114,7 +114,7 @@ let compare s1 s2 = match s1, s2 with
+ | Op(Access s1), Op(Access s2) -> Hstring.compare s1 s2
+ | Op(Access _), _ -> -1
+ | _, Op(Access _) -> 1
+- | _ -> Pervasives.compare s1 s2
++ | _ -> Stdlib.compare s1 s2
+
+ let equal s1 s2 = compare s1 s2 = 0
+
+--- alt-ergo-2.2.0/lib/structures/term.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/structures/term.ml 2021-01-29 16:33:11.033560074 -0700
+@@ -270,7 +270,7 @@ let gen_sko ty = make (Sy.fresh "@sko")
+
+ let is_skolem_cst v =
+ try
+- Pervasives.(=) (String.sub (Sy.to_string v.f) 0 4) "_sko"
++ Stdlib.(=) (String.sub (Sy.to_string v.f) 0 4) "_sko"
+ with Invalid_argument _ -> false
+
+ let find_skolem =
+@@ -338,7 +338,7 @@ let label t = try Labels.find labels t w
+
+
+ let label_model h =
+- try Pervasives.(=) (String.sub (Hstring.view h) 0 6) "model:"
++ try Stdlib.(=) (String.sub (Hstring.view h) 0 6) "model:"
+ with Invalid_argument _ -> false
+
+ let rec is_in_model_rec depth { f = f; xs = xs } =
+--- alt-ergo-2.2.0/lib/structures/ty.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/structures/ty.ml 2021-01-29 16:18:15.746370389 -0700
+@@ -202,7 +202,7 @@ let rec equal t1 t2 =
+
+ 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
+@@ -225,7 +225,7 @@ let rec compare t1 t2 =
+ let l1, l2 = List.map snd l1, List.map snd l2 in
+ compare_list l1 l2
+ | Trecord _, _ -> -1 | _ , Trecord _ -> 1
+- | t1 , t2 -> Pervasives.compare t1 t2
++ | t1 , t2 -> Stdlib.compare t1 t2
+ and compare_list l1 l2 = match l1, l2 with
+ | [] , [] -> 0
+ | [] , _ -> -1
+@@ -268,7 +268,7 @@ let rec unify t1 t2 =
+
+
+ (*** 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
+@@ -340,9 +340,9 @@ 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.(=)
+
+ let rec fresh ty subst =
+ match ty with
+@@ -383,7 +383,7 @@ and fresh_list lty subst =
+ ty::lty, subst) lty ([], subst)
+
+ 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.2.0/lib/util/myUnix.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/util/myUnix.ml 2021-01-29 16:45:33.010009798 -0700
+@@ -16,7 +16,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.2.0/lib/util/numbers.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/util/numbers.ml 2021-01-29 16:46:06.130989159 -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.2.0/lib/util/options.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/util/options.ml 2021-01-29 16:11:53.387767103 -0700
+@@ -902,8 +902,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.2.0/lib/util/zarithNumbers.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/lib/util/zarithNumbers.ml 2021-01-29 16:08:45.571962041 -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.2.0/tools/gui/annoted_ast.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/tools/gui/annoted_ast.ml 2021-01-29 16:47:08.762950125 -0700
+@@ -188,7 +188,7 @@ type annoted_node =
module MDep = Map.Make (
struct
type t = atyped_decl annoted
@@ -25,58 +419,58 @@
end)
-@@ -880,9 +880,9 @@ let find_dep_by_string dep s =
- | None -> begin
- match d.c with
- | ALogic (_, ls, _, _) when List.mem s ls -> Some d
-- | ATypeDecl (_, _, s', _, _) when Pervasives.(=) s s'-> Some d
-- | APredicate_def (_, p, _, _) when Pervasives.(=) s p -> Some d
-- | AFunction_def (_, f, _, _, _, _) when Pervasives.(=) s f -> Some d
-+ | ATypeDecl (_, _, s', _, _) when Stdlib.(=) s s'-> Some d
-+ | APredicate_def (_, p, _, _) when Stdlib.(=) s p -> Some d
-+ | AFunction_def (_, f, _, _, _, _) when Stdlib.(=) s f -> Some d
- | _ -> None
- end
+@@ -862,9 +862,9 @@ let find_dep_by_string dep s =
+ | None -> begin
+ match d.c with
+ | ALogic (_, ls, ty) when List.mem s ls -> Some d
+- | ATypeDecl (_, _, s', _) when Pervasives.(=) s s'-> Some d
+- | APredicate_def (_, p, _, _) when Pervasives.(=) s p -> Some d
+- | AFunction_def (_, f, _, _, _) when Pervasives.(=) s f -> Some d
++ | ATypeDecl (_, _, s', _) when Stdlib.(=) s s'-> Some d
++ | APredicate_def (_, p, _, _) when Stdlib.(=) s p -> Some d
++ | AFunction_def (_, f, _, _, _) when Stdlib.(=) s f -> Some d
+ | _ -> None
+ end
) dep None
-@@ -892,7 +892,7 @@ let find_tag_deps dep tag =
+@@ -874,7 +874,7 @@ let find_tag_deps dep tag =
(fun d (deps,_) found ->
- match found with
- | Some _ -> found
-- | None -> if Pervasives.(=) d.tag tag then Some deps else None
-+ | None -> if Stdlib.(=) d.tag tag then Some deps else None
+ match found with
+ | Some _ -> found
+- | None -> if Pervasives.(=) d.tag tag then Some deps else None
++ | None -> if Stdlib.(=) d.tag tag then Some deps else None
) dep None
let find_tag_inversedeps dep tag =
-@@ -900,7 +900,7 @@ let find_tag_inversedeps dep tag =
+@@ -882,7 +882,7 @@ let find_tag_inversedeps dep tag =
(fun d (_,deps) found ->
- match found with
- | Some _ -> found
-- | None -> if Pervasives.(=) d.tag tag then Some deps else None
-+ | None -> if Stdlib.(=) d.tag tag then Some deps else None
+ match found with
+ | Some _ -> found
+- | None -> if Pervasives.(=) d.tag tag then Some deps else None
++ | None -> if Stdlib.(=) d.tag tag then Some deps else None
) dep None
let make_dep_string d ex dep s =
-@@ -2046,7 +2046,7 @@ and findtags_aform sl aform acc =
- (fun sl (sy, _) ->
- let s = Symbols.to_string_clean sy in
- List.fold_left
-- (fun l s' -> if Pervasives.(=) s' s then l else s'::l) [] sl
-+ (fun l s' -> if Stdlib.(=) s' s then l else s'::l) [] sl
- )sl l
- in
- findtags_aform sl aaf.c acc
---- 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
- let cdr_ve = List.tl ve in
-- assert (Pervasives.(=) v v');
-+ assert (Stdlib.(=) v v');
- if String.length e == 0 then
- (v'::nbv, used, goal_used, cdr_ve, v'::uplet, lets)
- else
-@@ -545,7 +545,7 @@ let rec add_instance_aux ?(register=true
+@@ -1965,7 +1965,7 @@ and findtags_aform sl aform acc =
+ (fun sl (sy, _) ->
+ let s = Symbols.to_string_clean sy in
+ List.fold_left
+- (fun l s' -> if Pervasives.(=) s' s then l else s'::l) [] sl
++ (fun l s' -> if Stdlib.(=) s' s then l else s'::l) [] sl
+ )sl l
+ in
+ findtags_aform sl aaf.c acc
+--- alt-ergo-2.2.0/tools/gui/connected_ast.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/tools/gui/connected_ast.ml 2021-01-29 16:47:43.226928651 -0700
+@@ -386,7 +386,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
+ let cdr_ve = List.tl ve in
+- assert (Pervasives.(=) v v');
++ assert (Stdlib.(=) v v');
+ if String.length e == 0 then
+ (v'::nbv, used, goal_used, cdr_ve, v'::uplet, lets)
+ else
+@@ -541,7 +541,7 @@ let rec add_instance_aux ?(register=true
make_instance env.inst_buffer vars entries af goal_form tyenv in
let ln_form = least_nested_form used_vars goal_form in
env.inst_buffer#place_cursor ~where:env.inst_buffer#end_iter;
@@ -85,18 +479,18 @@
let hy =
AAxiom (loc, (sprintf "%s%s" "_instance_" aname), ax_kd, instance.c) in
let ahy = new_annot env.inst_buffer hy instance.id ptag in
-@@ -739,7 +739,7 @@ and add_trigger ?(register=true) t qid e
- if register then
- save env.actions
- (AddTrigger (qf.id,
-- Pervasives.(=) sbuf env.inst_buffer, str));
-+ Stdlib.(=) sbuf env.inst_buffer, str));
- commit_tags_buffer sbuf
- | _ -> assert false
- end
---- 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 =
+@@ -735,7 +735,7 @@ and add_trigger ?(register=true) t qid e
+ if register then
+ save env.actions
+ (AddTrigger (qf.id,
+- Pervasives.(=) sbuf env.inst_buffer, str));
++ Stdlib.(=) sbuf env.inst_buffer, str));
+ commit_tags_buffer sbuf
+ | _ -> assert false
+ end
+--- alt-ergo-2.2.0/tools/gui/main_gui.ml.orig 2018-04-21 11:02:10.000000000 -0600
++++ alt-ergo-2.2.0/tools/gui/main_gui.ml 2021-01-29 16:49:56.218845792 -0700
+@@ -148,7 +148,7 @@ let save_session envs =
let save_dialog cancel envs () =
if List.exists
@@ -105,7 +499,7 @@
if List.exists
(fun env -> not (Gui_session.safe_session env.actions)) envs then
GToolbox.message_box
-@@ -250,7 +250,7 @@ let pop_model sat_env () =
+@@ -247,7 +247,7 @@ let pop_model sat_env () =
let compare_rows icol_number (model:#GTree.model) row1 row2 =
let t1 = model#get ~row:row1 ~column:icol_number in
let t2 = model#get ~row:row2 ~column:icol_number in
@@ -123,16 +517,16 @@
t.tl_sat#set_text (sprintf "%3.2f s" tsat);
t.tl_match#set_text (sprintf "%3.2f s" tmatch);
-@@ -455,7 +455,7 @@ let add_inst ({ h; _ } as inst_model) or
- let id = Expr.id orig in
+@@ -455,7 +455,7 @@ let add_inst ({h=h} as inst_model) orig
+ let id = Formula.id orig in
let name =
- match Expr.form_view orig with
-- | Expr.Lemma { Expr.name = n ; _ } when Pervasives.(<>) n "" -> n
-+ | Expr.Lemma { Expr.name = n ; _ } when Stdlib.(<>) n "" -> n
- | Expr.Lemma _ | Expr.Unit _ | Expr.Clause _ | Expr.Literal _
- | Expr.Skolem _ | Expr.Let _ | Expr.Iff _ | Expr.Xor _ ->
- string_of_int id
-@@ -607,7 +607,7 @@ let vt_signal =
+ match Formula.view orig with
+- | Formula.Lemma {Formula.name=n} when Pervasives.(<>) n "" -> n
++ | Formula.Lemma {Formula.name=n} when Stdlib.(<>) n "" -> n
+ | _ -> string_of_int id
+ in
+ let r, n, limit, to_add =
+@@ -604,7 +604,7 @@ let vt_signal =
let force_interrupt old_action_ref n =
(* This function is called just before the thread's timeslice ends *)
@@ -141,18 +535,18 @@
raise Abort_thread;
match !old_action_ref with
| Sys.Signal_handle f -> f n
-@@ -723,8 +723,8 @@ let remove_context env () =
- toggle_prune env td
+@@ -718,8 +718,8 @@ let remove_context env () =
+ toggle_prune env td
| AAxiom (_, s, _, _)
- when String.length s = 0 ||
+ when String.length s = 0 ||
- (Pervasives.(<>) s.[0] '_' &&
- Pervasives.(<>) s.[0] '@') ->
+ (Stdlib.(<>) s.[0] '_' &&
+ Stdlib.(<>) s.[0] '@') ->
- toggle_prune env td
+ toggle_prune env td
| _ -> ()
) env.ast
-@@ -951,7 +951,7 @@ let search_all entry (_sv:GSourceView2.s
+@@ -945,7 +945,7 @@ let search_all entry (sv:GSourceView2.so
buf#remove_tag found_all_tag ~start:buf#start_iter ~stop:buf#end_iter;
let str = entry#text in
let iter = ref buf#start_iter in
@@ -161,7 +555,7 @@
let result = ref None in
search_one buf str result iter found_all_tag;
while !result != None do
-@@ -1300,7 +1300,7 @@ let start_gui all_used_context =
+@@ -1286,7 +1286,7 @@ let start_gui () =
let set_wrap_lines _ =
List.iter (fun env ->
diff --git a/alt-ergo-psmt2-frontend.patch b/alt-ergo-psmt2-frontend.patch
deleted file mode 100644
index caa9af7..0000000
--- a/alt-ergo-psmt2-frontend.patch
+++ /dev/null
@@ -1,12 +0,0 @@
---- alt-ergo-2.3.0-free/sources/parsers/psmt2_to_alt_ergo.ml.orig 2021-06-29 06:08:30.000000000 -0600
-+++ alt-ergo-2.3.0-free/sources/parsers/psmt2_to_alt_ergo.ml 2022-02-23 12:59:13.497394356 -0700
-@@ -403,6 +403,9 @@ module Translate = struct
- | Cmd_Push _ -> not_supported "push"; assert false
- | Cmd_Pop _ -> not_supported "pop"; assert false
- | Cmd_Exit -> acc
-+ | Cmd_CheckAllSat _ -> not_supported "check-all-sat"; assert false
-+ | Cmd_Maximize _ -> not_supported "maximize"; assert false
-+ | Cmd_Minimize _ -> not_supported "minimize"; assert false
-
- let init () =
- if Psmt2Frontend.Options.get_is_int_real () then
diff --git a/alt-ergo.metainfo.xml b/alt-ergo.metainfo.xml
index cff34da..cdb417e 100644
--- a/alt-ergo.metainfo.xml
+++ b/alt-ergo.metainfo.xml
@@ -20,15 +20,15 @@
com.ocamlpro.alt-ergo.desktop
- https://jjames.fedorapeople.org/alt-ergo/altgr-ergo-screenshot.png
+ http://jjames.fedorapeople.org/alt-ergo/altgr-ergo-screenshot.png
Basic Alt-Ergo usage
- alt-ergo-maintainers@fedoraproject.org
+ loganjerry@gmail.com
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.rpmlintrc b/alt-ergo.rpmlintrc
new file mode 100644
index 0000000..7a6e1a4
--- /dev/null
+++ b/alt-ergo.rpmlintrc
@@ -0,0 +1,14 @@
+# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON
+# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors
+
+# The dictionary lacks some technical words
+addFilter(r'W: spelling-error .* (arithmetics|equational|instantiation|parameterized|prover)')
+
+# Caused by ocaml; this package cannot fix it
+addFilter(r'alt-ergo(-gui)?\.[^:]+: E: missing-call-to-chdir-with-chroot')
+
+# Documentation is in the main package
+addFilter(r'alt-ergo-gui\.[^:]+: W: no-documentation')
+
+# There is no man page for the graphical launcher
+addFilter(r'alt-ergo-gui\.[^:]+: W: no-manual-page-for-binary altgr-ergo')
diff --git a/alt-ergo.spec b/alt-ergo.spec
index 3adb6d8..b56a195 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -1,194 +1,117 @@
-# 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.
-# 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
+%ifnarch %{ocaml_native_compiler}
+%global debug_package %{nil}
+%endif
Name: alt-ergo
-Version: %{minorver}.%{patchrel}
-Release: 30%{?dist}
+Version: 2.2.0
+Release: 9%{?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/
-# 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
+Source0: https://alt-ergo.ocamlpro.com/http/%{name}-%{version}/%{name}-%{version}.tar.gz
# Created with gimp from official upstream icon
-Source2: %{name}-icons.tar.xz
-Source3: %{name}.desktop
-Source4: %{name}.metainfo.xml
+Source1: %{name}-icons.tar.xz
+Source2: %{name}.desktop
+Source3: %{name}.metainfo.xml
+
+# Use the asmrun_pic variant when linking the binary.
+Patch0: %{name}-1.30-use-pic.patch
# 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
+Patch1: %{name}-pervasives.patch
BuildRequires: desktop-file-utils
BuildRequires: gtksourceview2-devel
BuildRequires: libappstream-glib
BuildRequires: make
-BuildRequires: ocaml >= 4.04.0
-BuildRequires: ocaml-dune
+BuildRequires: ocaml
+BuildRequires: ocaml-findlib
BuildRequires: ocaml-lablgtk-devel
BuildRequires: ocaml-menhir
BuildRequires: ocaml-num-devel
-BuildRequires: ocaml-ocplib-simplex-devel >= 0.4
-BuildRequires: ocaml-psmt2-frontend-devel >= 0.2
+BuildRequires: ocaml-ocplib-simplex-devel
+BuildRequires: ocaml-psmt2-frontend-devel
BuildRequires: ocaml-zarith-devel
BuildRequires: ocaml-zip-devel
-Requires: ocaml-alt-ergo-parsers%{?_isa} = %{version}-%{release}
+Requires: ocaml-alt-ergo%{?_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.}
+# Do not Require private ocaml interfaces that we don't Provide
+%global __requires_exclude ocamlx?\\\((Commands|Ex(ception|planation)|Formula|Hstring|Inequalities|L(iteral|oc)|Matching_types|Numbers(Interface)?|Options|P(arsed|olynome)|S(atml_types|ig|ymbols)|T(erm|y(ped)?)|U(f|til)|Vec)\\\)
-%description
-%_desc
+%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
%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
-
-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
-
-This package contains development files needed to build applications that use
-the Alt-Ergo parser library.
-
-%package -n ocaml-alt-ergo-lib
+%package -n ocaml-alt-ergo
Summary: Automated theorem prover library
-License: CECILL-C
-%description -n ocaml-alt-ergo-lib
-%_desc
+%description -n ocaml-alt-ergo %_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-zarith-devel%{?_isa}
+%package -n ocaml-alt-ergo-devel
+Summary: Development files for ocaml-altergolib
+Requires: ocaml-alt-ergo%{?_isa} = %{version}-%{release}
-%description -n ocaml-alt-ergo-lib-devel
-%_desc
+%description -n ocaml-alt-ergo-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}-%{minorver}.0-free -N -a 2
+%autosetup -p1 -a 1
-%if 0%{?patchrel} > 0
-# See above. Replace the minor release sources with the patch release sources.
-rm -rf sources
-tar xf %{SOURCE1}
+cp -p %{SOURCE2} com.ocamlpro.%{name}.desktop
+
+# Look for zip instead of camlzip
+sed -i 's/camlzip/zip/g' configure opam
+
+%ifarch %{arm}
+# Work around for https://github.com/ocaml/ocaml/issues/7608
+# Remove this once a released ocaml version fixes that issue.
+sed -i "s|^LIGHT_OFLAGS =|& -fno-thumb|" Makefile.users
%endif
-%autopatch -p1
-
-%conf
-cd sources
-cp -p %{SOURCE3} com.ocamlpro.%{name}.desktop
-
-# Unzip an example
-cd examples/AB-Why3-plugin
-unzip p4_34.why.zip
-rm p4_34.why.zip
-cd -
-
-%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
-%make_build
+%configure --libdir=%{_libdir}/ocaml
+
+%ifnarch %{ocaml_native_compiler}
+%global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLLEX=ocamllex
+%else
+%global opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
+%endif
+
+make %{opt_option}
%install
-cd sources
-%make_install
+mkdir -p %{buildroot}%{_bindir}
+make %{opt_option} DESTDIR=%{buildroot} install
-# We do not want the ml files
-find %{buildroot}%{ocamldir} -name \*.ml -delete
-
-# We install the documentation with the doc macro
-rm -fr %{buildroot}%{_prefix}/doc
-
-# Install the man page
-mkdir -p %{buildroot}%{_mandir}/man1
-cp -p doc/alt-ergo.1 %{buildroot}%{_mandir}/man1
-
-# 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
-cp -p doc/gtk-lang/alt-ergo.lang \
- %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs
+# Move the gtksourceview file to the right place
+mv %{buildroot}%{_datadir}/%{name}/gtksourceview-2.0 %{buildroot}%{_datadir}
+rmdir %{buildroot}%{_datadir}/%{name}
# Install the desktop file
mkdir -p %{buildroot}%{_datadir}/applications
@@ -197,241 +120,71 @@ desktop-file-install --dir %{buildroot}%{_datadir}/applications \
# Install the AppData file
mkdir -p %{buildroot}%{_metainfodir}
-install -pm 644 %{SOURCE4} \
+install -pm 644 %{SOURCE3} \
%{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml
appstream-util validate-relax --nonet \
%{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml
# Install the icons
-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_check
+# Test alt-ergo on the examples.
+%define altergo %{buildroot}%{_bindir}/alt-ergo
+cd examples/valid
+for fil in *.why; do
+ if ! %{altergo} $fil | grep -Fq Valid; then
+ echo $fil was not found valid
+ exit 1
+ fi
+done
+cd ../invalid
+for fil in *.why; do
+ if %{altergo} $fil | grep -Fq Valid; then
+ echo $fil was erroneously found valid
+ exit 1
+ fi
+done
%files
-%doc README.md sources/CHANGES sources/examples publications/*.pdf
+%doc README.md CHANGES examples
+%license COPYING.md LICENSE.md
%{_bindir}/%{name}
%{_mandir}/man1/alt-ergo.1.*
-%{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
-%{ocamldir}/altgr-ergo/
%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml
-%files -n ocaml-%{name}-parsers
-%dir %{ocamldir}/%{name}-parsers/
-%{ocamldir}/%{name}-parsers/META
-%{ocamldir}/%{name}-parsers/*.cma
-%{ocamldir}/%{name}-parsers/*.cmi
+%files -n ocaml-alt-ergo
+%dir %{_libdir}/ocaml/%{name}/
+%{_libdir}/ocaml/%{name}/plugins/
+%{_libdir}/ocaml/%{name}/preludes/
+%{_libdir}/ocaml/%{name}/altErgoLib.cma
+%{_libdir}/ocaml/%{name}/altErgoLib.cmi
%ifarch %{ocaml_native_compiler}
-%{ocamldir}/%{name}-parsers/*.cmxs
+%{_libdir}/ocaml/%{name}/altErgoLib.cmxs
%endif
-%{ocamldir}/%{name}-parsers-free/
-%files -n ocaml-%{name}-parsers-devel
-%{ocamldir}/%{name}-parsers/dune-package
-%{ocamldir}/%{name}-parsers/opam
+%files -n ocaml-%{name}-devel
+%{_libdir}/ocaml/%{name}/META
%ifarch %{ocaml_native_compiler}
-%{ocamldir}/%{name}-parsers/*.a
-%{ocamldir}/%{name}-parsers/*.cmx
-%{ocamldir}/%{name}-parsers/*.cmxa
+%{_libdir}/ocaml/%{name}/altErgoLib.a
+%{_libdir}/ocaml/%{name}/altErgoLib.cmx
+%{_libdir}/ocaml/%{name}/altErgoLib.cmxa
%endif
-%{ocamldir}/%{name}-parsers/*.mli
-%{ocamldir}/%{name}-parsers/*.cmt
-%{ocamldir}/%{name}-parsers/*.cmti
-
-%files -n ocaml-%{name}-lib
-%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}
-%{ocamldir}/%{name}-lib/*.cmxs
-%endif
-%{ocamldir}/%{name}-lib-free/
-
-%files -n ocaml-%{name}-lib-devel
-%{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}
-%{ocamldir}/%{name}-lib/*.a
-%{ocamldir}/%{name}-lib/*.cmx
-%{ocamldir}/%{name}-lib/*.cmxa
-%endif
-%{ocamldir}/%{name}-lib/*.cmt
-%{ocamldir}/%{name}-lib/*.cmti
+%{_libdir}/ocaml/%{name}/altErgoLib.o
+%{_libdir}/ocaml/%{name}/altErgoLib.cmo
+%{_libdir}/ocaml/%{name}/altErgoLib.cmt
%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
-- Add dependency on ocaml-alt-ergo-parsers from ocaml-alt-ergo-parsers-devel
-
-* Fri Feb 04 2022 Richard W.M. Jones - 2.3.0-3
-- OCaml 4.13.1 rebuild to remove package notes
-
-* Wed Jan 19 2022 Fedora Release Engineering - 2.3.0-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
-
-* Mon Dec 27 2021 Jerry James - 2.3.0-1
-- Version 2.3.0
-- New ocaml-alt-ergo-lib and ocaml-alt-ergo-parsers subpackages
-
-* Tue Oct 05 2021 Richard W.M. Jones - 2.2.0-14
-- OCaml 4.13.1 build
-
-* Thu Jul 29 2021 Jerry James - 2.2.0-13
-- Rebuild for changed ocamlx(Dynlink)
-
-* Wed Jul 21 2021 Fedora Release Engineering - 2.2.0-12
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
-
-* Mon Jul 19 2021 Jerry James - 2.2.0-11
-- Move META to the main package
-
-* Tue Jun 22 2021 Jerry James - 2.2.0-11
-- Rebuild for ocaml-lablgtk without gnomeui
-
-* Wed Mar 3 2021 Jerry James - 2.2.0-10
+* Wed Mar 3 2021 Jerry James - 2.2.0-9
- Rebuild for ocaml-zarith 1.12
-* Tue Mar 2 11:26:14 GMT 2021 Richard W.M. Jones - 2.2.0-9
-- OCaml 4.12.0 build
-
* Thu Feb 4 2021 Jerry James - 2.2.0-8
- Updates to the desktop and metainfo files
- Add -pervasives patch
diff --git a/sources b/sources
index 2e808e5..8679a4d 100644
--- a/sources
+++ b/sources
@@ -1,3 +1,2 @@
-SHA512 (alt-ergo-free-2.3.0.tar.gz) = e15efc6bbde59065c6ccaf1ef2f8158b8b9be4b00b2c2365e5eeb7d7114be72c47c813fc06880a6278edd7e288f24ef4588c88e0630d9bda9378a3eda3fd07ca
-SHA512 (alt-ergo-free-2.3.3.tar.gz) = 0dc056c02c8ffdeb9eeaa127dd204d30a0ee95ffe38aa3f1a608b17019f377ea6520ccfc9cb09b109deac5f19e7e695b7e6ec18db969843312cfb17f3950c9ba
+SHA512 (alt-ergo-2.2.0.tar.gz) = 08ac8250ef2b853edc4885038ffbc8a5b4bbbedd170812fda3a4c4e59609f9642ae995d3a75ed637fbabb1163c6e84afa61c41204d41ba4b1377b3b84cc01eb8
SHA512 (alt-ergo-icons.tar.xz) = cb2e93bab3359f6f198e80e3e68840ed4b25a213b61f388a2de8abc299fd3c89240f64f610290ac89e6005088c484b2718a68ec18063076f73d7871a38ee038f