From 3a917b3309e26ce4047ab1b540b53d0567ca32fc Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Tue, 2 Mar 2021 11:26:15 +0000
Subject: [PATCH 01/51] OCaml 4.12.0 build

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index c5ff404..0d261ed 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -8,7 +8,7 @@
 
 Name:		alt-ergo
 Version:	2.2.0
-Release:	8%{?dist}
+Release:	9%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 License:	ASL 2.0
 
@@ -182,6 +182,9 @@ done
 %{_libdir}/ocaml/%{name}/altErgoLib.cmt
 
 %changelog
+* Tue Mar  2 11:26:14 GMT 2021 Richard W.M. Jones <rjones@redhat.com> - 2.2.0-9
+- OCaml 4.12.0 build
+
 * Thu Feb  4 2021 Jerry James <loganjerry@gmail.com> - 2.2.0-8
 - Updates to the desktop and metainfo files
 - Add -pervasives patch

From 335accbed6e4aa4db24e07e8ca1d95f23f0e8062 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Wed, 3 Mar 2021 12:07:12 -0700
Subject: [PATCH 02/51] Rebuild for ocaml-zarith 1.12.

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 0d261ed..f1d22c9 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -8,7 +8,7 @@
 
 Name:		alt-ergo
 Version:	2.2.0
-Release:	9%{?dist}
+Release:	10%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 License:	ASL 2.0
 
@@ -182,6 +182,9 @@ done
 %{_libdir}/ocaml/%{name}/altErgoLib.cmt
 
 %changelog
+* Wed Mar  3 2021 Jerry James <loganjerry@gmail.com> - 2.2.0-10
+- Rebuild for ocaml-zarith 1.12
+
 * Tue Mar  2 11:26:14 GMT 2021 Richard W.M. Jones <rjones@redhat.com> - 2.2.0-9
 - OCaml 4.12.0 build
 

From 2cab6d39e0ec8065bdfa44cbb825f06e86599579 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Wed, 3 Mar 2021 12:07:12 -0700
Subject: [PATCH 03/51] Rebuild for ocaml-zarith 1.12.

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index c5ff404..b56a195 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -8,7 +8,7 @@
 
 Name:		alt-ergo
 Version:	2.2.0
-Release:	8%{?dist}
+Release:	9%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 License:	ASL 2.0
 
@@ -182,6 +182,9 @@ done
 %{_libdir}/ocaml/%{name}/altErgoLib.cmt
 
 %changelog
+* Wed Mar  3 2021 Jerry James <loganjerry@gmail.com> - 2.2.0-9
+- Rebuild for ocaml-zarith 1.12
+
 * Thu Feb  4 2021 Jerry James <loganjerry@gmail.com> - 2.2.0-8
 - Updates to the desktop and metainfo files
 - Add -pervasives patch

From a0af6956e8d953280625f8517b3cf8a628a1a4bc Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Thu, 24 Jun 2021 14:53:02 -0600
Subject: [PATCH 04/51] Rebuild for ocaml-lablgtk without gnomeui.

---
 alt-ergo.spec | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index f1d22c9..ca6cf7b 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -8,7 +8,7 @@
 
 Name:		alt-ergo
 Version:	2.2.0
-Release:	10%{?dist}
+Release:	11%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 License:	ASL 2.0
 
@@ -24,9 +24,9 @@ Patch0:		%{name}-1.30-use-pic.patch
 # Do not use the deprecated Pervasives interface
 Patch1:		%{name}-pervasives.patch
 
+BuildRequires:	appstream
 BuildRequires:	desktop-file-utils
 BuildRequires:	gtksourceview2-devel
-BuildRequires:	libappstream-glib
 BuildRequires:	make
 BuildRequires:	ocaml
 BuildRequires:	ocaml-findlib
@@ -122,7 +122,7 @@ desktop-file-install --dir %{buildroot}%{_datadir}/applications \
 mkdir -p %{buildroot}%{_metainfodir}
 install -pm 644 %{SOURCE3} \
   %{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml
-appstream-util validate-relax --nonet \
+appstreamcli validate --no-net \
   %{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml
 
 # Install the icons
@@ -182,6 +182,9 @@ done
 %{_libdir}/ocaml/%{name}/altErgoLib.cmt
 
 %changelog
+* Tue Jun 22 2021 Jerry James <loganjerry@gmail.com> - 2.2.0-11
+- Rebuild for ocaml-lablgtk without gnomeui
+
 * Wed Mar  3 2021 Jerry James <loganjerry@gmail.com> - 2.2.0-10
 - Rebuild for ocaml-zarith 1.12
 

From 3480332c8e8a4bbc809373a7c7cdeb7e4a89d031 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Mon, 19 Jul 2021 13:19:50 -0600
Subject: [PATCH 05/51] Move META to the main package.

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index ca6cf7b..1b3abd2 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -162,6 +162,7 @@ done
 
 %files -n ocaml-alt-ergo
 %dir %{_libdir}/ocaml/%{name}/
+%{_libdir}/ocaml/%{name}/META
 %{_libdir}/ocaml/%{name}/plugins/
 %{_libdir}/ocaml/%{name}/preludes/
 %{_libdir}/ocaml/%{name}/altErgoLib.cma
@@ -171,7 +172,6 @@ done
 %endif
 
 %files -n ocaml-%{name}-devel
-%{_libdir}/ocaml/%{name}/META
 %ifarch %{ocaml_native_compiler}
 %{_libdir}/ocaml/%{name}/altErgoLib.a
 %{_libdir}/ocaml/%{name}/altErgoLib.cmx
@@ -182,6 +182,9 @@ done
 %{_libdir}/ocaml/%{name}/altErgoLib.cmt
 
 %changelog
+* Mon Jul 19 2021 Jerry James <loganjerry@gmail.com> - 2.2.0-11
+- Move META to the main package
+
 * Tue Jun 22 2021 Jerry James <loganjerry@gmail.com> - 2.2.0-11
 - Rebuild for ocaml-lablgtk without gnomeui
 

From 154f03ab069c55237e63011a69914064eeb467be Mon Sep 17 00:00:00 2001
From: Fedora Release Engineering <releng@fedoraproject.org>
Date: Wed, 21 Jul 2021 12:33:38 +0000
Subject: [PATCH 06/51] - Rebuilt for
 https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild

Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>

From d4fa98b0182fc2c9fa0571120bdf7878977896e5 Mon Sep 17 00:00:00 2001
From: Fedora Release Engineering <releng@fedoraproject.org>
Date: Wed, 21 Jul 2021 17:29:03 +0000
Subject: [PATCH 07/51] - Rebuilt for
 https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild

Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 1b3abd2..6818f2c 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -8,7 +8,7 @@
 
 Name:		alt-ergo
 Version:	2.2.0
-Release:	11%{?dist}
+Release:	12%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 License:	ASL 2.0
 
@@ -182,6 +182,9 @@ done
 %{_libdir}/ocaml/%{name}/altErgoLib.cmt
 
 %changelog
+* Wed Jul 21 2021 Fedora Release Engineering <releng@fedoraproject.org> - 2.2.0-12
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
+
 * Mon Jul 19 2021 Jerry James <loganjerry@gmail.com> - 2.2.0-11
 - Move META to the main package
 

From 9a10ab3b2a47cf684f402c404e1adc7ee15b70d9 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Thu, 29 Jul 2021 12:57:23 -0600
Subject: [PATCH 08/51] Rebuild for changed ocamlx(Dynlink).

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 6818f2c..9fedc78 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -8,7 +8,7 @@
 
 Name:		alt-ergo
 Version:	2.2.0
-Release:	12%{?dist}
+Release:	13%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 License:	ASL 2.0
 
@@ -182,6 +182,9 @@ done
 %{_libdir}/ocaml/%{name}/altErgoLib.cmt
 
 %changelog
+* Thu Jul 29 2021 Jerry James <loganjerry@gmail.com> - 2.2.0-13
+- Rebuild for changed ocamlx(Dynlink)
+
 * Wed Jul 21 2021 Fedora Release Engineering <releng@fedoraproject.org> - 2.2.0-12
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
 

From ed81837150d45206a2b06d7cf3e0077422c095c1 Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Tue, 5 Oct 2021 12:54:42 +0100
Subject: [PATCH 09/51] OCaml 4.13.1 build

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 9fedc78..81eca7a 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -8,7 +8,7 @@
 
 Name:		alt-ergo
 Version:	2.2.0
-Release:	13%{?dist}
+Release:	14%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 License:	ASL 2.0
 
@@ -182,6 +182,9 @@ done
 %{_libdir}/ocaml/%{name}/altErgoLib.cmt
 
 %changelog
+* Tue Oct 05 2021 Richard W.M. Jones <rjones@redhat.com> - 2.2.0-14
+- OCaml 4.13.1 build
+
 * Thu Jul 29 2021 Jerry James <loganjerry@gmail.com> - 2.2.0-13
 - Rebuild for changed ocamlx(Dynlink)
 

From 4b29dc3ccc4cabd7aba6c4e8651049e6f616963b Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Thu, 30 Dec 2021 17:12:44 -0700
Subject: [PATCH 10/51] Version 2.3.0.

New ocaml-alt-ergo-lib and ocaml-alt-ergo-parsers subpackages.
---
 README.md                     |   9 +
 alt-ergo-1.30-use-pic.patch   |  19 -
 alt-ergo-pervasives.patch     | 687 ++++++++++++++++++----------------
 alt-ergo-psmt2-frontend.patch |  12 +
 alt-ergo.spec                 | 190 ++++++----
 sources                       |   2 +-
 6 files changed, 500 insertions(+), 419 deletions(-)
 create mode 100644 README.md
 delete mode 100644 alt-ergo-1.30-use-pic.patch
 create mode 100644 alt-ergo-psmt2-frontend.patch

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..fa65fbb
--- /dev/null
+++ b/README.md
@@ -0,0 +1,9 @@
+# alt-ergo
+
+[Alt-Ergo](https://alt-ergo.ocamlpro.com/) is an automated theorem prover
+implemented in OCaml.  It is based on `CC(X)` &mdash; 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
deleted file mode 100644
index 71d6ad0..0000000
--- a/alt-ergo-1.30-use-pic.patch
+++ /dev/null
@@ -1,19 +0,0 @@
---- 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-pervasives.patch b/alt-ergo-pervasives.patch
index b782e21..23ad048 100644
--- a/alt-ergo-pervasives.patch
+++ b/alt-ergo-pervasives.patch
@@ -1,71 +1,7 @@
---- 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
+--- alt-ergo-2.3.0/lib/frontend/typechecker.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/frontend/typechecker.ml	2021-12-13 11:22:42.669959468 -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)
@@ -73,17 +9,17 @@
  
  module Types = struct
  
-@@ -78,7 +78,7 @@ 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
+         (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;
+@@ -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" ->
@@ -91,49 +27,27 @@
        let t1,t2 = match l with
          | [t2] -> PPTint,t2
          | [t1;t2] -> t1,t2
-@@ -108,7 +108,7 @@ module Types = struct
+@@ -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
-@@ -769,7 +769,7 @@ and type_form ?(in_theory=false) env f =
+         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
-             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
+--- alt-ergo-2.3.0/lib/reasoners/fun_sat.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/reasoners/fun_sat.ml	2021-12-13 11:17:14.158193751 -0700
+@@ -75,7 +75,7 @@ module Make (Th : Theory.S) : Sat_solver
+         SE.fold
            (fun f mp ->
-              let w = var_inc +. try MF.find f mp with Not_found -> 0. in
+              let w = var_inc +. try ME.find f mp with Not_found -> 0. in
 -             stable := !stable && Pervasives.(<=) w 1e100;
 +             stable := !stable && Stdlib.(<=) w 1e100;
-              MF.add f w mp
+              ME.add f w mp
            )(Ex.bj_formulas_of expl) mp
        in
-@@ -95,9 +95,9 @@ module Make (Th : Theory.S) : Sat_solver
+@@ -118,9 +118,9 @@ module Make (Th : Theory.S) : Sat_solver
        let dec =
          List.fast_sort
            (fun (_, x1, b1) (_, x2, b2) ->
@@ -145,7 +59,7 @@
            )dec
        in
        (*
-@@ -967,7 +967,7 @@ module Make (Th : Theory.S) : Sat_solver
+@@ -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) &&
@@ -154,20 +68,20 @@
        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)
+--- alt-ergo-2.3.0/lib/reasoners/ite_rel.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/reasoners/ite_rel.ml	2021-12-13 11:18:06.781156246 -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.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
+ type t =
+--- alt-ergo-2.3.0/lib/reasoners/satml_frontend.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/reasoners/satml_frontend.ml	2021-12-13 11:17:48.709169125 -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 *)
@@ -176,27 +90,45 @@
        if res <> 0 then res
        else
          (* lower index is better *)
-@@ -922,7 +922,7 @@ module Make (Th : Theory.S) : Sat_solver
+@@ -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 (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
+-    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.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
+--- alt-ergo-2.3.0/lib/reasoners/satml.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/reasoners/satml.ml	2021-12-13 11:18:53.173123173 -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
  
-   let f_filter env i = (Vec.get env.vars i).level < 0
+   (* unused -- let f_filter env i = (Vec.get env.vars i).level < 0 *)
  
-@@ -365,7 +365,7 @@ module Make (Th : Theory.S) : SAT_ML wit
+@@ -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;
@@ -205,7 +137,7 @@
        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
+@@ -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;
@@ -214,51 +146,77 @@
        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
+--- alt-ergo-2.3.0/lib/structures/expr.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/structures/expr.ml	2021-12-13 11:27:30.381754212 -0700
+@@ -1031,7 +1031,7 @@ let mk_builtin ~is_pos n l =
+ (** Substitutions *)
  
- 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:"
+ 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 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
+ 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
  
-   type t = { at : atom; neg : bool; tpos : int; tneg : int }
+     | { 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
  
--  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 =
+     | { 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/lib/structures/profiling.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/structures/profiling.ml	2021-12-13 11:28:14.180722957 -0700
+@@ -85,7 +85,7 @@ let state =
  let set_sigprof () =
    let tm =
      let v = Options.profiling_period () in
@@ -267,7 +225,7 @@
    in
    ignore
      (Unix.setitimer Unix.ITIMER_PROF
-@@ -626,9 +626,9 @@ let switch () =
+@@ -629,9 +629,9 @@ let switch () =
  
  
  let float_print fmt v =
@@ -280,59 +238,61 @@
    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
+--- alt-ergo-2.3.0/lib/structures/symbols.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/structures/symbols.ml	2021-12-13 11:23:17.604934542 -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
  
- 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 =
+--- alt-ergo-2.3.0/lib/structures/ty.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/structures/ty.ml	2021-12-13 11:23:47.596913146 -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
-@@ -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 =
+-  | 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)
@@ -340,7 +300,7 @@
  type subst = t M.t
  
  let esubst = M.empty
-@@ -340,9 +340,9 @@ let instantiate lvar lty ty =
+@@ -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
  
@@ -350,20 +310,61 @@
 -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
+--- alt-ergo-2.3.0/lib/structures/typed.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/structures/typed.ml	2021-12-13 11:28:32.876709614 -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/lib/structures/xliteral.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/structures/xliteral.ml	2021-12-13 11:27:49.604740495 -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/lib/util/emap.mli.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/util/emap.mli	2021-12-13 11:20:53.277037515 -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/lib/util/myUnix.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/util/myUnix.ml	2021-12-13 11:19:46.141085403 -0700
+@@ -18,7 +18,7 @@ module Default_Unix = struct
    let cur_time () = (times()).tms_utime
  
    let set_timeout ~is_gui timelimit =
@@ -372,33 +373,54 @@
        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
+--- alt-ergo-2.3.0/lib/util/numbers.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/util/numbers.ml	2021-12-13 11:22:11.316981841 -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
+     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/lib/util/options.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/util/options.ml	2021-12-13 11:21:27.477013115 -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.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
+ (* extra **)
+--- alt-ergo-2.3.0/lib/util/util.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/util/util.ml	2021-12-13 11:20:25.717057175 -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/lib/util/util.mli.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/util/util.mli	2021-12-13 11:20:10.341068143 -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/lib/util/zarithNumbers.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/lib/util/zarithNumbers.ml	2021-12-13 11:19:11.821109879 -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))
@@ -408,9 +430,20 @@
      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 =
+--- alt-ergo-2.3.0/parsers/parsers.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/parsers/parsers.ml	2021-12-13 11:16:42.461216342 -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/tools/gui/annoted_ast.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/tools/gui/annoted_ast.ml	2021-12-13 11:15:02.334287694 -0700
+@@ -191,7 +191,7 @@ type annoted_node =
  module MDep = Map.Make (
    struct
      type t = atyped_decl annoted
@@ -419,58 +452,58 @@
    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
+@@ -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
      ) dep None
-@@ -874,7 +874,7 @@ let find_tag_deps dep tag =
+@@ -892,7 +892,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 =
-@@ -882,7 +882,7 @@ let find_tag_inversedeps dep tag =
+@@ -900,7 +900,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 =
-@@ -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
+@@ -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/tools/gui/connected_ast.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/tools/gui/connected_ast.ml	2021-12-13 11:16:16.069235150 -0700
+@@ -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
      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;
@@ -479,18 +512,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
-@@ -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 =
+@@ -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/tools/gui/main_gui.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/tools/gui/main_gui.ml	2021-12-13 11:15:49.445254125 -0700
+@@ -151,7 +151,7 @@ let save_session envs =
  
  let save_dialog cancel envs () =
    if List.exists
@@ -499,7 +532,7 @@
      if List.exists
          (fun env -> not (Gui_session.safe_session env.actions)) envs then
        GToolbox.message_box
-@@ -247,7 +247,7 @@ let pop_model sat_env () =
+@@ -250,7 +250,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
@@ -517,16 +550,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=h} as inst_model) orig
-   let id = Formula.id orig in
+@@ -455,7 +455,7 @@ let add_inst ({ h; _ } as inst_model) or
+   let id = Expr.id orig in
    let name =
-     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 =
+     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 =
  
  let force_interrupt old_action_ref n =
    (* This function is called just before the thread's timeslice ends *)
@@ -535,18 +568,18 @@
      raise Abort_thread;
    match !old_action_ref with
    | Sys.Signal_handle f -> f n
-@@ -718,8 +718,8 @@ let remove_context env () =
- 	 toggle_prune env td
+@@ -723,8 +723,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
-@@ -945,7 +945,7 @@ let search_all entry (sv:GSourceView2.so
+@@ -951,7 +951,7 @@ let search_all entry (_sv:GSourceView2.s
    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
@@ -555,7 +588,7 @@
      let result = ref None in
      search_one buf str result iter found_all_tag;
      while !result != None do
-@@ -1286,7 +1286,7 @@ let start_gui () =
+@@ -1300,7 +1300,7 @@ let start_gui all_used_context =
  
    let set_wrap_lines _ =
      List.iter (fun env ->
diff --git a/alt-ergo-psmt2-frontend.patch b/alt-ergo-psmt2-frontend.patch
new file mode 100644
index 0000000..1c58d9e
--- /dev/null
+++ b/alt-ergo-psmt2-frontend.patch
@@ -0,0 +1,12 @@
+--- alt-ergo-2.3.0/parsers/psmt2_to_alt_ergo.ml.orig	2019-02-11 09:43:50.000000000 -0700
++++ alt-ergo-2.3.0/parsers/psmt2_to_alt_ergo.ml	2021-12-13 13:45:45.216802816 -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.spec b/alt-ergo.spec
index 81eca7a..b1b8edf 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -7,8 +7,8 @@
 %endif
 
 Name:		alt-ergo
-Version:	2.2.0
-Release:	14%{?dist}
+Version:	2.3.0
+Release:	1%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 License:	ASL 2.0
 
@@ -18,30 +18,29 @@ Source0:	https://alt-ergo.ocamlpro.com/http/%{name}-%{version}/%{name}-%{version
 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
-Patch1:		%{name}-pervasives.patch
+Patch0:		%{name}-pervasives.patch
+# Adapt to recent changes in psmt2-frontend
+Patch1:		%{name}-psmt2-frontend.patch
 
 BuildRequires:	appstream
 BuildRequires:	desktop-file-utils
 BuildRequires:	gtksourceview2-devel
 BuildRequires:	make
-BuildRequires:	ocaml
+BuildRequires:	ocaml >= 4.04.0
+BuildRequires:	ocaml-dune
 BuildRequires:	ocaml-findlib
 BuildRequires:	ocaml-lablgtk-devel
 BuildRequires:	ocaml-menhir
 BuildRequires:	ocaml-num-devel
-BuildRequires:	ocaml-ocplib-simplex-devel
-BuildRequires:	ocaml-psmt2-frontend-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%{?_isa} = %{version}-%{release}
-
-# 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)\\\)
+Requires:	ocaml-alt-ergo-parsers%{?_isa} = %{version}-%{release}
 
 %global _desc %{expand:
 Alt-Ergo is an automated theorem prover implemented in OCaml. It is
@@ -64,18 +63,41 @@ Requires:	hicolor-icon-theme
 This package contains a graphical front end for the Alt-Ergo theorem
 prover.
 
-%package -n ocaml-alt-ergo
+%package -n ocaml-alt-ergo-parsers
+Summary:	Parser library used by the Alt-Ergo SMT solver
+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
+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
 Summary:	Automated theorem prover library
 
-%description -n ocaml-alt-ergo %_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-devel
-Summary:	Development files for ocaml-altergolib
-Requires:	ocaml-alt-ergo%{?_isa} = %{version}-%{release}
+%package -n ocaml-alt-ergo-lib-devel
+Summary:	Development files for ocaml-alt-ergo-lib
+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-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.
@@ -85,33 +107,44 @@ that use the Alt-Ergo library.
 
 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
+# Unzip an example
+cd examples/AB-Why3-plugin
+unzip p4_34.why.zip
+rm p4_34.why.zip
+cd -
 
 %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}
+# This is not an autoconf-generated script.  Do NOT use %%configure.
+./configure --prefix=%{_prefix} --libdir=%{_libdir}/ocaml --sharedir=%{_datadir}
+%make_build
+%make_build doc
 
 %install
-mkdir -p %{buildroot}%{_bindir}
-make %{opt_option} DESTDIR=%{buildroot} install
+%make_install
 
-# Move the gtksourceview file to the right place
-mv %{buildroot}%{_datadir}/%{name}/gtksourceview-2.0 %{buildroot}%{_datadir}
-rmdir %{buildroot}%{_datadir}/%{name}
+# 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
+
+# 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
+
+# Make the plugins directory
+mkdir -p %{buildroot}%{_libdir}/ocaml/%{name}/plugins
+
+# Install the preludes
+cp -a preludes %{buildroot}%{_libdir}/ocaml/%{name}
+
+# 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
 
 # Install the desktop file
 mkdir -p %{buildroot}%{_datadir}/applications
@@ -130,58 +163,71 @@ mkdir -p %{buildroot}%{_datadir}/icons
 cp -a icons %{buildroot}%{_datadir}/icons/hicolor
 
 %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
+dune runtest --profile release
 
 %files
 %doc README.md CHANGES examples
 %license COPYING.md LICENSE.md
 %{_bindir}/%{name}
 %{_mandir}/man1/alt-ergo.1.*
+%{_libdir}/ocaml/%{name}/
 
 %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/
 %{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml
 
-%files -n ocaml-alt-ergo
-%dir %{_libdir}/ocaml/%{name}/
-%{_libdir}/ocaml/%{name}/META
-%{_libdir}/ocaml/%{name}/plugins/
-%{_libdir}/ocaml/%{name}/preludes/
-%{_libdir}/ocaml/%{name}/altErgoLib.cma
-%{_libdir}/ocaml/%{name}/altErgoLib.cmi
+%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
 %ifarch %{ocaml_native_compiler}
-%{_libdir}/ocaml/%{name}/altErgoLib.cmxs
+%{_libdir}/ocaml/%{name}-parsers/*.cmxs
 %endif
 
-%files -n ocaml-%{name}-devel
+%files -n ocaml-%{name}-parsers-devel
+%{_libdir}/ocaml/%{name}-parsers/dune-package
+%{_libdir}/ocaml/%{name}-parsers/opam
 %ifarch %{ocaml_native_compiler}
-%{_libdir}/ocaml/%{name}/altErgoLib.a
-%{_libdir}/ocaml/%{name}/altErgoLib.cmx
-%{_libdir}/ocaml/%{name}/altErgoLib.cmxa
+%{_libdir}/ocaml/%{name}-parsers/*.a
+%{_libdir}/ocaml/%{name}-parsers/*.cmx
+%{_libdir}/ocaml/%{name}-parsers/*.cmxa
 %endif
-%{_libdir}/ocaml/%{name}/altErgoLib.o
-%{_libdir}/ocaml/%{name}/altErgoLib.cmo
-%{_libdir}/ocaml/%{name}/altErgoLib.cmt
+%{_libdir}/ocaml/%{name}-parsers/*.mli
+%{_libdir}/ocaml/%{name}-parsers/*.cmt
+%{_libdir}/ocaml/%{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
+%ifarch %{ocaml_native_compiler}
+%{_libdir}/ocaml/%{name}-lib/*.cmxs
+%endif
+
+%files -n ocaml-%{name}-lib-devel
+%doc _build/default/_doc/*
+%{_libdir}/ocaml/%{name}-lib/dune-package
+%{_libdir}/ocaml/%{name}-lib/opam
+%ifarch %{ocaml_native_compiler}
+%{_libdir}/ocaml/%{name}-lib/*.a
+%{_libdir}/ocaml/%{name}-lib/*.cmx
+%{_libdir}/ocaml/%{name}-lib/*.cmxa
+%endif
+%{_libdir}/ocaml/%{name}-lib/*.mli
+%{_libdir}/ocaml/%{name}-lib/*.cmt
+%{_libdir}/ocaml/%{name}-lib/*.cmti
 
 %changelog
+* Mon Dec 27 2021 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 2.2.0-14
 - OCaml 4.13.1 build
 
diff --git a/sources b/sources
index 8679a4d..f5aec05 100644
--- a/sources
+++ b/sources
@@ -1,2 +1,2 @@
-SHA512 (alt-ergo-2.2.0.tar.gz) = 08ac8250ef2b853edc4885038ffbc8a5b4bbbedd170812fda3a4c4e59609f9642ae995d3a75ed637fbabb1163c6e84afa61c41204d41ba4b1377b3b84cc01eb8
+SHA512 (alt-ergo-2.3.0.tar.gz) = a2f209b62b8494bfefe84328cdc786185e0534c5e224e212b83045b078352a51d2ab02622f72c22c74c7de95c7a554cbdae2a9a8a0c41f3f26c841f8c72f6b21
 SHA512 (alt-ergo-icons.tar.xz) = cb2e93bab3359f6f198e80e3e68840ed4b25a213b61f388a2de8abc299fd3c89240f64f610290ac89e6005088c484b2718a68ec18063076f73d7871a38ee038f

From 9cf9f87095d23cc63b2bca2622aab7997657d789 Mon Sep 17 00:00:00 2001
From: Fedora Release Engineering <releng@fedoraproject.org>
Date: Wed, 19 Jan 2022 21:10:09 +0000
Subject: [PATCH 11/51] - Rebuilt for
 https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild

Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index b1b8edf..b968115 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -8,7 +8,7 @@
 
 Name:		alt-ergo
 Version:	2.3.0
-Release:	1%{?dist}
+Release:	2%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 License:	ASL 2.0
 
@@ -224,6 +224,9 @@ dune runtest --profile release
 %{_libdir}/ocaml/%{name}-lib/*.cmti
 
 %changelog
+* Wed Jan 19 2022 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.0-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
+
 * Mon Dec 27 2021 Jerry James <loganjerry@gmail.com> - 2.3.0-1
 - Version 2.3.0
 - New ocaml-alt-ergo-lib and ocaml-alt-ergo-parsers subpackages

From 4817f805f6023dcf39594ff9f683aa851ffa5f77 Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Fri, 4 Feb 2022 20:19:28 +0000
Subject: [PATCH 12/51] OCaml 4.13.1 rebuild to remove package notes

---
 alt-ergo.spec | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index b968115..5cecc07 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -1,3 +1,4 @@
+%undefine _package_note_flags
 # 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.
@@ -8,7 +9,7 @@
 
 Name:		alt-ergo
 Version:	2.3.0
-Release:	2%{?dist}
+Release:	3%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 License:	ASL 2.0
 
@@ -224,6 +225,9 @@ dune runtest --profile release
 %{_libdir}/ocaml/%{name}-lib/*.cmti
 
 %changelog
+* Fri Feb 04 2022 Richard W.M. Jones <rjones@redhat.com> - 2.3.0-3
+- OCaml 4.13.1 rebuild to remove package notes
+
 * Wed Jan 19 2022 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.0-2
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
 

From 20c71462b63c4a182e78e2f69bc076f4f83c53e3 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Mon, 28 Feb 2022 12:02:56 -0700
Subject: [PATCH 13/51] Switch to the correct tarball.

- Drop unneeded ocaml-findlib BR.
- Add dependency on ocaml-alt-ergo-parsers from ocaml-alt-ergo-parsers-devel.
---
 alt-ergo-pervasives.patch     | 104 ++++++++++++++++++++--------------
 alt-ergo-psmt2-frontend.patch |   4 +-
 alt-ergo.rpmlintrc            |  14 -----
 alt-ergo.spec                 |  29 +++++++---
 sources                       |   2 +-
 5 files changed, 83 insertions(+), 70 deletions(-)
 delete mode 100644 alt-ergo.rpmlintrc

diff --git a/alt-ergo-pervasives.patch b/alt-ergo-pervasives.patch
index 23ad048..4c0a255 100644
--- a/alt-ergo-pervasives.patch
+++ b/alt-ergo-pervasives.patch
@@ -1,5 +1,21 @@
---- alt-ergo-2.3.0/lib/frontend/typechecker.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/frontend/typechecker.ml	2021-12-13 11:22:42.669959468 -0700
+--- 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
+   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
+ 
+ 
+--- 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
  
@@ -36,8 +52,8 @@
                                     equal_pp_vars l vars -> ty
          | _ ->
            try
---- alt-ergo-2.3.0/lib/reasoners/fun_sat.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/reasoners/fun_sat.ml	2021-12-13 11:17:14.158193751 -0700
+--- 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 ->
@@ -68,8 +84,8 @@
        begin
          Options.Time.unset_timeout ~is_gui:(Options.get_is_gui());
          Options.Time.set_timeout
---- alt-ergo-2.3.0/lib/reasoners/ite_rel.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/reasoners/ite_rel.ml	2021-12-13 11:18:06.781156246 -0700
+--- 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) =
@@ -79,8 +95,8 @@
      end)
  
  type t =
---- alt-ergo-2.3.0/lib/reasoners/satml_frontend.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/reasoners/satml_frontend.ml	2021-12-13 11:17:48.709169125 -0700
+--- 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
@@ -117,8 +133,8 @@
      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/lib/reasoners/satml.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/reasoners/satml.ml	2021-12-13 11:18:53.173123173 -0700
+--- 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
  *)
  
@@ -146,8 +162,8 @@
        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/lib/structures/expr.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/structures/expr.ml	2021-12-13 11:27:30.381754212 -0700
+--- 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 *)
  
@@ -214,8 +230,8 @@
      if c <> 0 then c else Util.cmp_lists tl1 tl2 cmp_trig_term
  
    let unique_stable_sort =
---- alt-ergo-2.3.0/lib/structures/profiling.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/structures/profiling.ml	2021-12-13 11:28:14.180722957 -0700
+--- 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 =
@@ -238,8 +254,8 @@
    else fprintf fmt "%0.3f" v
  
  let line_of_module arr f =
---- alt-ergo-2.3.0/lib/structures/symbols.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/structures/symbols.ml	2021-12-13 11:23:17.604934542 -0700
+--- 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
@@ -271,8 +287,8 @@
        if c <> 0 then c
        else compare_bounds_kind a.kind b.kind
  
---- alt-ergo-2.3.0/lib/structures/ty.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/structures/ty.ml	2021-12-13 11:23:47.596913146 -0700
+--- 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 =
@@ -316,8 +332,8 @@
  
  module Set =
    Set.Make(struct
---- alt-ergo-2.3.0/lib/structures/typed.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/structures/typed.ml	2021-12-13 11:28:32.876709614 -0700
+--- 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)
  
@@ -329,8 +345,8 @@
 -  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/lib/structures/xliteral.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/structures/xliteral.ml	2021-12-13 11:27:49.604740495 -0700
+--- 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 }
@@ -340,8 +356,8 @@
    let equal a1 a2 = a1.tpos = a2.tpos (* XXX == *)
    let hash a1 = a1.tpos
    let uid a1 = a1.tpos
---- alt-ergo-2.3.0/lib/util/emap.mli.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/util/emap.mli	2021-12-13 11:20:53.277037515 -0700
+--- 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
@@ -362,8 +378,8 @@
  end
  (** Input signature of the functor {!Map.Make}. *)
  
---- alt-ergo-2.3.0/lib/util/myUnix.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/util/myUnix.ml	2021-12-13 11:19:46.141085403 -0700
+--- 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
  
@@ -373,8 +389,8 @@
        let itimer =
          if is_gui then Unix.ITIMER_REAL (* troubles with VIRTUAL *)
          else Unix.ITIMER_VIRTUAL
---- alt-ergo-2.3.0/lib/util/numbers.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/util/numbers.ml	2021-12-13 11:22:11.316981841 -0700
+--- 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
@@ -386,8 +402,8 @@
          else v
        in
        let flt = if n = 2 then sqrt w else w ** (1. /. float n) in
---- alt-ergo-2.3.0/lib/util/options.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/util/options.ml	2021-12-13 11:21:27.477013115 -0700
+--- 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
@@ -397,8 +413,8 @@
  
  
  (* extra **)
---- alt-ergo-2.3.0/lib/util/util.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/util/util.ml	2021-12-13 11:20:25.717057175 -0700
+--- 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
@@ -408,8 +424,8 @@
    | true, false -> -1
    | false, true -> 1
    | false, false ->
---- alt-ergo-2.3.0/lib/util/util.mli.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/util/util.mli	2021-12-13 11:20:10.341068143 -0700
+--- 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.
@@ -419,8 +435,8 @@
  
  *)
  val [@inline always] compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int
---- alt-ergo-2.3.0/lib/util/zarithNumbers.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/lib/util/zarithNumbers.ml	2021-12-13 11:19:11.821109879 -0700
+--- 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))
@@ -430,8 +446,8 @@
      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/parsers/parsers.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/parsers/parsers.ml	2021-12-13 11:16:42.461216342 -0700
+--- 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
@@ -441,8 +457,8 @@
          let cin = open_in file in
          cin, Lexing.from_channel cin, true, ext
        else
---- alt-ergo-2.3.0/tools/gui/annoted_ast.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/tools/gui/annoted_ast.ml	2021-12-13 11:15:02.334287694 -0700
+--- 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
 @@ -191,7 +191,7 @@ type annoted_node =
  module MDep = Map.Make (
    struct
@@ -492,8 +508,8 @@
          )sl l
      in
      findtags_aform sl aaf.c acc
---- alt-ergo-2.3.0/tools/gui/connected_ast.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/tools/gui/connected_ast.ml	2021-12-13 11:16:16.069235150 -0700
+--- 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
 @@ -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
@@ -521,8 +537,8 @@
          commit_tags_buffer sbuf
        | _ -> assert false
      end
---- alt-ergo-2.3.0/tools/gui/main_gui.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/tools/gui/main_gui.ml	2021-12-13 11:15:49.445254125 -0700
+--- 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
 @@ -151,7 +151,7 @@ let save_session envs =
  
  let save_dialog cancel envs () =
diff --git a/alt-ergo-psmt2-frontend.patch b/alt-ergo-psmt2-frontend.patch
index 1c58d9e..caa9af7 100644
--- a/alt-ergo-psmt2-frontend.patch
+++ b/alt-ergo-psmt2-frontend.patch
@@ -1,5 +1,5 @@
---- alt-ergo-2.3.0/parsers/psmt2_to_alt_ergo.ml.orig	2019-02-11 09:43:50.000000000 -0700
-+++ alt-ergo-2.3.0/parsers/psmt2_to_alt_ergo.ml	2021-12-13 13:45:45.216802816 -0700
+--- 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
diff --git a/alt-ergo.rpmlintrc b/alt-ergo.rpmlintrc
deleted file mode 100644
index 7a6e1a4..0000000
--- a/alt-ergo.rpmlintrc
+++ /dev/null
@@ -1,14 +0,0 @@
-# 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 5cecc07..0c15271 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -1,20 +1,21 @@
-%undefine _package_note_flags
 # 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
 
 Name:		alt-ergo
 Version:	2.3.0
-Release:	3%{?dist}
+Release:	4%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 License:	ASL 2.0
 
 URL:		https://alt-ergo.ocamlpro.com/
-Source0:	https://alt-ergo.ocamlpro.com/http/%{name}-%{version}/%{name}-%{version}.tar.gz
+Source0:	https://alt-ergo.ocamlpro.com/http/%{name}-free-%{version}/%{name}-free-%{version}.tar.gz
 # Created with gimp from official upstream icon
 Source1:	%{name}-icons.tar.xz
 Source2:	%{name}.desktop
@@ -30,7 +31,6 @@ BuildRequires:	gtksourceview2-devel
 BuildRequires:	make
 BuildRequires:	ocaml >= 4.04.0
 BuildRequires:	ocaml-dune
-BuildRequires:	ocaml-findlib
 BuildRequires:	ocaml-lablgtk-devel
 BuildRequires:	ocaml-menhir
 BuildRequires:	ocaml-num-devel
@@ -74,6 +74,7 @@ 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
+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}
@@ -104,8 +105,9 @@ This package contains development files needed to build applications
 that use the Alt-Ergo library.
 
 %prep
-%autosetup -p1 -a 1
+%autosetup -n %{name}-%{version}-free -p1 -a 1
 
+cd sources
 cp -p %{SOURCE2} com.ocamlpro.%{name}.desktop
 
 # Unzip an example
@@ -116,11 +118,13 @@ cd -
 
 %build
 # This is not an autoconf-generated script.  Do NOT use %%configure.
+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
@@ -160,15 +164,17 @@ appstreamcli validate --no-net \
   %{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml
 
 # Install the icons
+cd -
 mkdir -p %{buildroot}%{_datadir}/icons
 cp -a icons %{buildroot}%{_datadir}/icons/hicolor
 
 %check
-dune runtest --profile release
+cd sources
+dune runtest --release
 
 %files
-%doc README.md CHANGES examples
-%license COPYING.md LICENSE.md
+%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}/
@@ -212,7 +218,7 @@ dune runtest --profile release
 %endif
 
 %files -n ocaml-%{name}-lib-devel
-%doc _build/default/_doc/*
+%doc sources/_build/default/_doc/*
 %{_libdir}/ocaml/%{name}-lib/dune-package
 %{_libdir}/ocaml/%{name}-lib/opam
 %ifarch %{ocaml_native_compiler}
@@ -225,6 +231,11 @@ dune runtest --profile release
 %{_libdir}/ocaml/%{name}-lib/*.cmti
 
 %changelog
+* Mon Feb 28 2022 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 2.3.0-3
 - OCaml 4.13.1 rebuild to remove package notes
 
diff --git a/sources b/sources
index f5aec05..56b9730 100644
--- a/sources
+++ b/sources
@@ -1,2 +1,2 @@
-SHA512 (alt-ergo-2.3.0.tar.gz) = a2f209b62b8494bfefe84328cdc786185e0534c5e224e212b83045b078352a51d2ab02622f72c22c74c7de95c7a554cbdae2a9a8a0c41f3f26c841f8c72f6b21
+SHA512 (alt-ergo-free-2.3.0.tar.gz) = e15efc6bbde59065c6ccaf1ef2f8158b8b9be4b00b2c2365e5eeb7d7114be72c47c813fc06880a6278edd7e288f24ef4588c88e0630d9bda9378a3eda3fd07ca
 SHA512 (alt-ergo-icons.tar.xz) = cb2e93bab3359f6f198e80e3e68840ed4b25a213b61f388a2de8abc299fd3c89240f64f610290ac89e6005088c484b2718a68ec18063076f73d7871a38ee038f

From 5f6eee8592100c36eee8bbde19b5db0950ea3992 Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Sun, 19 Jun 2022 13:28:13 +0100
Subject: [PATCH 14/51] OCaml 4.14.0 rebuild

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 0c15271..c1413a7 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -10,7 +10,7 @@
 
 Name:		alt-ergo
 Version:	2.3.0
-Release:	4%{?dist}
+Release:	5%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 License:	ASL 2.0
 
@@ -231,6 +231,9 @@ dune runtest --release
 %{_libdir}/ocaml/%{name}-lib/*.cmti
 
 %changelog
+* Sun Jun 19 2022 Richard W.M. Jones <rjones@redhat.com> - 2.3.0-5
+- OCaml 4.14.0 rebuild
+
 * Mon Feb 28 2022 Jerry James <loganjerry@gmail.com> - 2.3.0-4
 - Switch to the correct tarball
 - Drop unneeded ocaml-findlib BR

From cf26b7fc7efef5894e9e3b2814589a49147e7883 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Tue, 21 Jun 2022 09:01:13 -0600
Subject: [PATCH 15/51] Version 2.3.3.

- Add -menhir patch to fix FTBFS.
- Add -stdlib-shims patch since Fedora does not need stdlib-shims.
---
 alt-ergo-menhir.patch       |  18 ++
 alt-ergo-pervasives.patch   | 455 +-----------------------------------
 alt-ergo-stdlib-shims.patch |  42 ++++
 alt-ergo.spec               |  61 +++--
 sources                     |   1 +
 5 files changed, 113 insertions(+), 464 deletions(-)
 create mode 100644 alt-ergo-menhir.patch
 create mode 100644 alt-ergo-stdlib-shims.patch

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

From cf1a6b7780edc8d55a1f7bf68a927c1efd1eab4d Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Tue, 5 Jul 2022 17:03:29 -0600
Subject: [PATCH 16/51] Patch out uses of the dune external-lib-deps command.

- Patch out references to the seq forward compatibility module.
- Use new OCaml macros.
---
 alt-ergo-dune3.patch                          | 29 ++++++
 ...ims.patch => alt-ergo-forward-compat.patch | 32 ++++++-
 alt-ergo.spec                                 | 91 +++++++++----------
 3 files changed, 101 insertions(+), 51 deletions(-)
 create mode 100644 alt-ergo-dune3.patch
 rename alt-ergo-stdlib-shims.patch => alt-ergo-forward-compat.patch (60%)

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-stdlib-shims.patch b/alt-ergo-forward-compat.patch
similarity index 60%
rename from alt-ergo-stdlib-shims.patch
rename to alt-ergo-forward-compat.patch
index 5f266df..b3be679 100644
--- a/alt-ergo-stdlib-shims.patch
+++ b/alt-ergo-forward-compat.patch
@@ -1,13 +1,25 @@
 --- alt-ergo-2.3.0-free/sources/alt-ergo-lib-free.opam.orig	2022-05-20 03:15:57.000000000 -0600
-+++ alt-ergo-2.3.0-free/sources/alt-ergo-lib-free.opam	2022-06-18 16:35:11.569523676 -0600
-@@ -16,7 +16,6 @@ depends: [
++++ 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"
+-  "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: [
@@ -18,14 +30,24 @@
  ]
  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-06-18 16:34:45.634456726 -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        seq unix num str zarith dynlink ocplib-simplex)
++  (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)
diff --git a/alt-ergo.spec b/alt-ergo.spec
index 79fa381..ecfba1b 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -16,7 +16,7 @@
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	1%{?dist}
+Release:	2%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 License:	ASL 2.0
 
@@ -39,8 +39,10 @@ Patch1:		%{name}-psmt2-frontend.patch
 # AB plugin.  Menhir is unable to infer types with the current code and layout.
 # Check each new release to see if this is still necessary.
 Patch2:         %{name}-menhir.patch
-# Fedora does not have or need the forward compatibility stdlib-shims package
-Patch3:         %{name}-stdlib-shims.patch
+# 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
 
 BuildRequires:	appstream
 BuildRequires:	desktop-file-utils
@@ -52,9 +54,7 @@ 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
 
@@ -113,7 +113,6 @@ Summary:	Development files for ocaml-alt-ergo-lib
 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
@@ -143,19 +142,15 @@ cd -
 %build
 # This is not an autoconf-generated script.  Do NOT use %%configure.
 cd sources
-./configure --prefix=%{_prefix} --libdir=%{_libdir}/ocaml --sharedir=%{_libdir}/ocaml
+./configure --prefix=%{_prefix} --libdir=%{ocamldir} --sharedir=%{ocamldir}
 %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
@@ -166,7 +161,7 @@ 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}%{_libdir}/ocaml/alt-ergo
+   %{buildroot}%{ocamldir}/alt-ergo
 rmdir %{buildroot}%{_datadir}/alt-ergo
 
 # Install the gtksourceview file
@@ -193,70 +188,74 @@ cp -a icons %{buildroot}%{_datadir}/icons/hicolor
 
 %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}/
-%{_libdir}/ocaml/%{name}-free/
+%{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
-%{_libdir}/ocaml/%{name}-parsers-free/
+%{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/
+%{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
-%{_libdir}/ocaml/%{name}-lib-free/
+%{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
 %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/*.mli
+%{ocamldir}/%{name}-lib/*.cmt
+%{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Tue Jul  5 2022 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 2.3.3-1
 - Version 2.3.3
 - Add -menhir patch to fix FTBFS

From 43489678cad85bc82bbe1d3cec64e28fa9b6fbf4 Mon Sep 17 00:00:00 2001
From: Fedora Release Engineering <releng@fedoraproject.org>
Date: Wed, 20 Jul 2022 20:41:54 +0000
Subject: [PATCH 17/51] Rebuilt for
 https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild

Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index ecfba1b..2f4e937 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -16,7 +16,7 @@
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	2%{?dist}
+Release:	3%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 License:	ASL 2.0
 
@@ -251,6 +251,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Wed Jul 20 2022 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
+
 * Tue Jul  5 2022 Jerry James <loganjerry@gmail.com> - 2.3.3-2
 - Patch out uses of the dune external-lib-deps command
 - Patch out references to the seq forward compatibility module

From 61ce442efc897a263eb05d38a594e189056e5ca0 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Thu, 11 Aug 2022 09:24:41 -0600
Subject: [PATCH 18/51] Convert License tag to SPDX.

Note that the AB plugin has a different license.
---
 alt-ergo.spec | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 2f4e937..affd66d 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -10,7 +10,7 @@
 
 # The major and minor releases contain a full tarball.  Patch releases, however,
 # contain only the parts that have changed, typically just the sources
-# directory.  Use this to set up everything up appropriately.
+# directory.  Use this to set up everything appropriately.
 %global minorver 2.3
 %global patchrel 3
 
@@ -18,8 +18,10 @@ Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
 Release:	3%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
-License:	ASL 2.0
 
+# The project as a whole is Apache-2.0.
+# The AB-Why3 plugin is LGPL-2.1-only WITH OCaml-LGPL-linking-exception
+License:	Apache-2.0 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.
@@ -72,6 +74,7 @@ instantiation mechanism by which it fully supports quantifiers.}
 
 %package gui
 Summary:	Graphical front end for Alt-Ergo
+License:	Apache-2.0
 Requires:	%{name}%{?_isa} = %{version}-%{release}
 Requires:	gtksourceview2
 Requires:	hicolor-icon-theme
@@ -83,6 +86,7 @@ prover.
 
 %package -n ocaml-alt-ergo-parsers
 Summary:	Parser library used by the Alt-Ergo SMT solver
+License:	Apache-2.0
 Requires:	ocaml-alt-ergo-lib%{?_isa} = %{version}-%{release}
 
 %description -n ocaml-alt-ergo-parsers %_desc
@@ -91,6 +95,7 @@ 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:	Apache-2.0
 Requires:	ocaml-alt-ergo-parsers%{?_isa} = %{version}-%{release}
 Requires:	ocaml-alt-ergo-lib-devel%{?_isa} = %{version}-%{release}
 Requires:	ocaml-psmt2-frontend-devel%{?_isa}
@@ -103,6 +108,7 @@ that use the Alt-Ergo parser library.
 
 %package -n ocaml-alt-ergo-lib
 Summary:	Automated theorem prover library
+License:	Apache-2.0
 
 %description -n ocaml-alt-ergo-lib %_desc
 
@@ -110,6 +116,7 @@ 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:	Apache-2.0
 Requires:	ocaml-alt-ergo-lib%{?_isa} = %{version}-%{release}
 Requires:	ocaml-num-devel%{?_isa}
 Requires:	ocaml-ocplib-simplex-devel%{?_isa}
@@ -192,7 +199,6 @@ cd sources
 
 %files
 %doc README.md sources/CHANGES sources/examples publications/*.pdf
-%license COPYING.md LICENSE.md License.OCamlPro
 %{_bindir}/%{name}
 %{_mandir}/man1/alt-ergo.1.*
 %{ocamldir}/%{name}/
@@ -230,6 +236,7 @@ cd sources
 
 %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
@@ -251,6 +258,10 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Thu Aug 11 2022 Jerry James <loganjerry@gmail.com> - 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 <releng@fedoraproject.org> - 2.3.3-3
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
 

From 3901efd195b280f907eb901a9466331f81a6bd8a Mon Sep 17 00:00:00 2001
From: Fedora Release Engineering <releng@fedoraproject.org>
Date: Wed, 18 Jan 2023 21:38:44 +0000
Subject: [PATCH 19/51] Rebuilt for
 https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild

Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index affd66d..4ffb323 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -16,7 +16,7 @@
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	3%{?dist}
+Release:	4%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -258,6 +258,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Wed Jan 18 2023 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-4
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
+
 * Thu Aug 11 2022 Jerry James <loganjerry@gmail.com> - 2.3.3-3
 - Convert License tag to SPDX
 - Note that the AB plugin has a different license

From 11fc19a34cfcf1ec30b85826acb7dec363367fae Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Tue, 24 Jan 2023 19:30:31 +0000
Subject: [PATCH 20/51] Rebuild OCaml packages for F38

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 4ffb323..3420b36 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -16,7 +16,7 @@
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	4%{?dist}
+Release:	5%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -258,6 +258,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-5
+- Rebuild OCaml packages for F38
+
 * Wed Jan 18 2023 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-4
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
 

From 04eaf57e3a54133ed8291fe7604ae3e96321bbff Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Fri, 24 Mar 2023 10:04:51 -0600
Subject: [PATCH 21/51] Dune 3.7.0 changed the install location of mli files

---
 alt-ergo.metainfo.xml |  4 ++--
 alt-ergo.spec         | 10 ++++++++--
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/alt-ergo.metainfo.xml b/alt-ergo.metainfo.xml
index cdb417e..5bf59c9 100644
--- a/alt-ergo.metainfo.xml
+++ b/alt-ergo.metainfo.xml
@@ -20,7 +20,7 @@
  <launchable type="desktop-id">com.ocamlpro.alt-ergo.desktop</launchable>
  <screenshots>
   <screenshot type="default">
-   <image>http://jjames.fedorapeople.org/alt-ergo/altgr-ergo-screenshot.png</image>
+   <image>https://jjames.fedorapeople.org/alt-ergo/altgr-ergo-screenshot.png</image>
    <caption>Basic Alt-Ergo usage</caption>
   </screenshot>
  </screenshots>
@@ -28,7 +28,7 @@
  <url type="homepage">https://alt-ergo.ocamlpro.com/</url>
  <url type="bugtracker">https://github.com/OCamlPro/alt-ergo/issues</url>
  <url type="contact">https://alt-ergo.ocamlpro.com/#services</url>
- <content_rating type="oars-1.0"></content_rating>
+ <content_rating type="oars-1.1"></content_rating>
  <provides>
   <binary>altgr-ergo</binary>
  </provides>
diff --git a/alt-ergo.spec b/alt-ergo.spec
index 3420b36..2e48222 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -16,7 +16,7 @@
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	5%{?dist}
+Release:	6%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -248,16 +248,22 @@ cd sources
 %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/*.mli
 %{ocamldir}/%{name}-lib/*.cmt
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Fri Mar 24 2023 Jerry James <loganjerry@gmail.com> - 2.3.3-6
+- Dune 3.7.0 changed the install location of mli files
+
 * Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-5
 - Rebuild OCaml packages for F38
 

From f2cbc74c5e4c2f37a3c9d0863af4df287d9ebd7c Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Mon, 10 Jul 2023 16:57:48 -0600
Subject: [PATCH 22/51] OCaml 5.0.0 rebuild

---
 alt-ergo.spec | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 2e48222..46d4279 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -2,12 +2,6 @@
 # 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.
@@ -16,7 +10,7 @@
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	6%{?dist}
+Release:	7%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -146,6 +140,11 @@ 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
+
 %build
 # This is not an autoconf-generated script.  Do NOT use %%configure.
 cd sources
@@ -261,6 +260,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Mon Jul 10 2023 Jerry James <loganjerry@gmail.com> - 2.3.3-7
+- OCaml 5.0.0 rebuild
+
 * Fri Mar 24 2023 Jerry James <loganjerry@gmail.com> - 2.3.3-6
 - Dune 3.7.0 changed the install location of mli files
 

From 5ec9dcf52b9add353269928daa426320844dbe04 Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Tue, 11 Jul 2023 11:36:25 +0100
Subject: [PATCH 23/51] ExcludeArch i686
 (https://lists.fedoraproject.org/archives/list/devel@lists.fedoraproject.org/message/SPML7CUBSZNI36NLXGVHEG7DNHU3EWOJ/)

---
 alt-ergo.spec | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 46d4279..138bd95 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -1,3 +1,6 @@
+# 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.

From 4aadcff56bbd242bf84e7e57862dda8443f38885 Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Wed, 12 Jul 2023 01:39:34 +0100
Subject: [PATCH 24/51] OCaml 5.0 rebuild for Fedora 39

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 138bd95..cb17057 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	7%{?dist}
+Release:	8%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -263,6 +263,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Wed Jul 12 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-8
+- OCaml 5.0 rebuild for Fedora 39
+
 * Mon Jul 10 2023 Jerry James <loganjerry@gmail.com> - 2.3.3-7
 - OCaml 5.0.0 rebuild
 

From 961a793aa4bb4160a553bf4be613376afa67db9e Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Tue, 18 Jul 2023 11:35:04 -0600
Subject: [PATCH 25/51] Validate appdata with appstream-util

---
 alt-ergo.spec | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index cb17057..2bc3f83 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -43,9 +43,9 @@ Patch3:         %{name}-forward-compat.patch
 # Dune 3 eliminated the external-lib-deps command
 Patch4:         %{name}-dune3.patch
 
-BuildRequires:	appstream
 BuildRequires:	desktop-file-utils
 BuildRequires:	gtksourceview2-devel
+BuildRequires:	libappstream-glib
 BuildRequires:	make
 BuildRequires:	ocaml >= 4.04.0
 BuildRequires:	ocaml-dune
@@ -187,7 +187,7 @@ desktop-file-install --dir %{buildroot}%{_datadir}/applications \
 mkdir -p %{buildroot}%{_metainfodir}
 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
@@ -263,6 +263,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Tue Jul 18 2023 Jerry James <loganjerry@gmail.com> - 2.3.3-8
+- Validate appdata with appstream-util
+
 * Wed Jul 12 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-8
 - OCaml 5.0 rebuild for Fedora 39
 

From dcf60c5f1e5fce4586fcc17c3d839665efe9065b Mon Sep 17 00:00:00 2001
From: Fedora Release Engineering <releng@fedoraproject.org>
Date: Wed, 19 Jul 2023 13:10:45 +0000
Subject: [PATCH 26/51] Rebuilt for
 https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild

Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 2bc3f83..201b9ce 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	8%{?dist}
+Release:	9%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -263,6 +263,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Wed Jul 19 2023 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-9
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
+
 * Tue Jul 18 2023 Jerry James <loganjerry@gmail.com> - 2.3.3-8
 - Validate appdata with appstream-util
 

From 17e8a91f5087c14bd5ce2be2af1b5ca82b7c86ed Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Thu, 27 Jul 2023 10:22:59 -0600
Subject: [PATCH 27/51] Rebuild for ocaml-zarith 1.13

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 201b9ce..8bd6571 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	9%{?dist}
+Release:	10%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -263,6 +263,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Thu Jul 27 2023 Jerry James <loganjerry@gmail.com> - 2.3.3-10
+- Rebuild for ocaml-zarith 1.13
+
 * Wed Jul 19 2023 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-9
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
 

From 95ebe8b78e5aeb4a41cc8f5bd76c4e163287f3db Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Thu, 5 Oct 2023 21:27:10 +0100
Subject: [PATCH 28/51] OCaml 5.1 rebuild for Fedora 40

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 8bd6571..fabc4c1 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	10%{?dist}
+Release:	11%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -263,6 +263,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Thu Oct 05 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-11
+- OCaml 5.1 rebuild for Fedora 40
+
 * Thu Jul 27 2023 Jerry James <loganjerry@gmail.com> - 2.3.3-10
 - Rebuild for ocaml-zarith 1.13
 

From 03925961950310a6b50a6f9344c3a25cb3a171cb Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Tue, 12 Dec 2023 18:19:33 +0000
Subject: [PATCH 29/51] OCaml 5.1.1 rebuild for Fedora 40

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index fabc4c1..74da93d 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	11%{?dist}
+Release:	12%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -263,6 +263,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Tue Dec 12 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-12
+- OCaml 5.1.1 rebuild for Fedora 40
+
 * Thu Oct 05 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-11
 - OCaml 5.1 rebuild for Fedora 40
 

From f83c022bb375f52677563d9b14e0a14dd55f539c Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Mon, 18 Dec 2023 20:42:39 +0000
Subject: [PATCH 30/51] OCaml 5.1.1 + s390x code gen fix for Fedora 40

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 74da93d..a9032d3 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	12%{?dist}
+Release:	13%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -263,6 +263,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Mon Dec 18 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-13
+- OCaml 5.1.1 + s390x code gen fix for Fedora 40
+
 * Tue Dec 12 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-12
 - OCaml 5.1.1 rebuild for Fedora 40
 

From d55e3db9b2f86f547ee1fa44d2569c776650367d Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Mon, 18 Dec 2023 20:31:53 -0700
Subject: [PATCH 31/51] Update metainfo contact address

---
 alt-ergo.metainfo.xml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/alt-ergo.metainfo.xml b/alt-ergo.metainfo.xml
index 5bf59c9..cff34da 100644
--- a/alt-ergo.metainfo.xml
+++ b/alt-ergo.metainfo.xml
@@ -24,7 +24,7 @@
    <caption>Basic Alt-Ergo usage</caption>
   </screenshot>
  </screenshots>
- <update_contact>loganjerry@gmail.com</update_contact>
+ <update_contact>alt-ergo-maintainers@fedoraproject.org</update_contact>
  <url type="homepage">https://alt-ergo.ocamlpro.com/</url>
  <url type="bugtracker">https://github.com/OCamlPro/alt-ergo/issues</url>
  <url type="contact">https://alt-ergo.ocamlpro.com/#services</url>

From 2d515533aeafb538abc92fca4fbd324a57ea4b7f Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Tue, 2 Jan 2024 11:28:58 -0700
Subject: [PATCH 32/51] Rebuild for ocaml-num

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index a9032d3..a07e6cb 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	13%{?dist}
+Release:	14%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -263,6 +263,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Tue Jan  2 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-14
+- Rebuild for ocaml-num and ocaml-menhir 20231231
+
 * Mon Dec 18 2023 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-13
 - OCaml 5.1.1 + s390x code gen fix for Fedora 40
 

From ba198bf5cf00926f98692aba297f09a1d10c2e8f Mon Sep 17 00:00:00 2001
From: Fedora Release Engineering <releng@fedoraproject.org>
Date: Fri, 19 Jan 2024 12:46:18 +0000
Subject: [PATCH 33/51] Rebuilt for
 https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index a07e6cb..3053df7 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	14%{?dist}
+Release:	15%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -263,6 +263,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Fri Jan 19 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-15
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
+
 * Tue Jan  2 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-14
 - Rebuild for ocaml-num and ocaml-menhir 20231231
 

From 89e6861d48bb9d9a10b3e1174ec747ae2e0954ed Mon Sep 17 00:00:00 2001
From: Fedora Release Engineering <releng@fedoraproject.org>
Date: Mon, 22 Jan 2024 22:57:19 +0000
Subject: [PATCH 34/51] Rebuilt for
 https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 3053df7..7df67ce 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	15%{?dist}
+Release:	16%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -263,6 +263,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Mon Jan 22 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-16
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
+
 * Fri Jan 19 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-15
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
 

From bd0a00952534e977b2063fa4b8604bd363d96541 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Fri, 2 Feb 2024 10:09:48 -0700
Subject: [PATCH 35/51] Rebuild for changed ocamlx(Dynlink) hash

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 7df67ce..c490048 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	16%{?dist}
+Release:	17%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -263,6 +263,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Fri Feb  2 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-17
+- Rebuild for changed ocamlx(Dynlink) hash
+
 * Mon Jan 22 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-16
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
 

From ce64caea9cd1161c27605f9414443ed7d632a5e5 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Thu, 23 May 2024 10:57:15 -0600
Subject: [PATCH 36/51] Add patch to fix misplaced inline attributes

---
 alt-ergo-inline-error.patch | 26 ++++++++++++++++++++++++++
 alt-ergo.spec               |  5 +++++
 2 files changed, 31 insertions(+)
 create mode 100644 alt-ergo-inline-error.patch

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.spec b/alt-ergo.spec
index c490048..a62f7c7 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -42,6 +42,8 @@ Patch2:         %{name}-menhir.patch
 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:	desktop-file-utils
 BuildRequires:	gtksourceview2-devel
@@ -263,6 +265,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Thu May 23 2024 Jerry James <loganjerry@gmail.com> - 2.3.%{patchrel}-17
+- Add patch to fix misplaced inline attributes
+
 * Fri Feb  2 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-17
 - Rebuild for changed ocamlx(Dynlink) hash
 

From 8d4dec6e83e7c845f311c787f4f077609a1d835c Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Wed, 29 May 2024 23:50:30 +0100
Subject: [PATCH 37/51] OCaml 5.2.0 for Fedora 41

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index a62f7c7..43b7bcd 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	17%{?dist}
+Release:	18%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -265,6 +265,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Wed May 29 2024 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-18
+- OCaml 5.2.0 for Fedora 41
+
 * Thu May 23 2024 Jerry James <loganjerry@gmail.com> - 2.3.%{patchrel}-17
 - Add patch to fix misplaced inline attributes
 

From ffa1a2579918e6546fa992e813067edc5be0032e Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Wed, 19 Jun 2024 14:26:21 +0100
Subject: [PATCH 38/51] OCaml 5.2.0 ppc64le fix

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 43b7bcd..efe6fe8 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	18%{?dist}
+Release:	19%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -265,6 +265,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Wed Jun 19 2024 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-19
+- OCaml 5.2.0 ppc64le fix
+
 * Wed May 29 2024 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-18
 - OCaml 5.2.0 for Fedora 41
 

From fa4007b53c733a341532d3b5b401b91900a9ed1a Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Tue, 16 Jul 2024 10:39:18 -0600
Subject: [PATCH 39/51] Rebuild for ocaml-zarith 1.14

---
 alt-ergo.spec | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index efe6fe8..50d9743 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	19%{?dist}
+Release:	20%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -265,13 +265,16 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Tue Jul 16 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-20
+- Rebuild for ocaml-zarith 1.14
+
 * Wed Jun 19 2024 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-19
 - OCaml 5.2.0 ppc64le fix
 
 * Wed May 29 2024 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-18
 - OCaml 5.2.0 for Fedora 41
 
-* Thu May 23 2024 Jerry James <loganjerry@gmail.com> - 2.3.%{patchrel}-17
+* Thu May 23 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-17
 - Add patch to fix misplaced inline attributes
 
 * Fri Feb  2 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-17

From d49408568a28b9a414e38f1bb29522c6f17b238a Mon Sep 17 00:00:00 2001
From: Fedora Release Engineering <releng@fedoraproject.org>
Date: Wed, 17 Jul 2024 16:53:51 +0000
Subject: [PATCH 40/51] Rebuilt for
 https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 50d9743..655c5ce 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	20%{?dist}
+Release:	21%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -265,6 +265,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Wed Jul 17 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-21
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild
+
 * Tue Jul 16 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-20
 - Rebuild for ocaml-zarith 1.14
 

From 51625d920756664142ce0d95e359579fcd68313b Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Mon, 5 Aug 2024 10:32:00 -0600
Subject: [PATCH 41/51] Rebuild for ocaml-menhir 20240715 and ocaml-zip 1.12

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 655c5ce..a31ff01 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	21%{?dist}
+Release:	22%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The project as a whole is Apache-2.0.
@@ -265,6 +265,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Mon Aug  5 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-22
+- Rebuild for ocaml-menhir 20240715 and ocaml-zip 1.12
+
 * Wed Jul 17 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-21
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild
 

From 75bbe3f8fc8409a54c479a5fa476d3261bb4d8ad Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Fri, 27 Dec 2024 11:45:43 -0700
Subject: [PATCH 42/51] Correct License fields from Apache-2.0 to CECILL-C

- Do configuration steps in %conf
---
 alt-ergo.spec | 28 +++++++++++++++++++---------
 1 file changed, 19 insertions(+), 9 deletions(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index a31ff01..0086789 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -16,9 +16,12 @@ Version:	%{minorver}.%{patchrel}
 Release:	22%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
-# The project as a whole is Apache-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 webiste and also in
+# sources/tools/gui/main_gui.ml.
 # The AB-Why3 plugin is LGPL-2.1-only WITH OCaml-LGPL-linking-exception
-License:	Apache-2.0 AND 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.
@@ -73,7 +76,7 @@ instantiation mechanism by which it fully supports quantifiers.}
 
 %package gui
 Summary:	Graphical front end for Alt-Ergo
-License:	Apache-2.0
+License:	CECILL-C
 Requires:	%{name}%{?_isa} = %{version}-%{release}
 Requires:	gtksourceview2
 Requires:	hicolor-icon-theme
@@ -85,7 +88,7 @@ prover.
 
 %package -n ocaml-alt-ergo-parsers
 Summary:	Parser library used by the Alt-Ergo SMT solver
-License:	Apache-2.0
+License:	CECILL-C
 Requires:	ocaml-alt-ergo-lib%{?_isa} = %{version}-%{release}
 
 %description -n ocaml-alt-ergo-parsers %_desc
@@ -94,7 +97,7 @@ 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:	Apache-2.0
+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}
@@ -107,7 +110,7 @@ that use the Alt-Ergo parser library.
 
 %package -n ocaml-alt-ergo-lib
 Summary:	Automated theorem prover library
-License:	Apache-2.0
+License:	CECILL-C
 
 %description -n ocaml-alt-ergo-lib %_desc
 
@@ -115,7 +118,7 @@ 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:	Apache-2.0
+License:	CECILL-C
 Requires:	ocaml-alt-ergo-lib%{?_isa} = %{version}-%{release}
 Requires:	ocaml-num-devel%{?_isa}
 Requires:	ocaml-ocplib-simplex-devel%{?_isa}
@@ -136,6 +139,8 @@ tar xf %{SOURCE1}
 %endif
 
 %autopatch -p1
+
+%conf
 cd sources
 cp -p %{SOURCE3} com.ocamlpro.%{name}.desktop
 
@@ -150,10 +155,11 @@ cd -
 sed -i '/cmxs/d' plugins/{AB-Why3,fm-simplex}/dune
 %endif
 
-%build
 # This is not an autoconf-generated script.  Do NOT use %%configure.
-cd sources
 ./configure --prefix=%{_prefix} --libdir=%{ocamldir} --sharedir=%{ocamldir}
+
+%build
+cd sources
 %make_build
 
 %install
@@ -265,6 +271,10 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Mon Dec 23 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-22
+- Correct License fields from Apache-2.0 to CECILL-C
+- Do configuration steps in %%conf
+
 * Mon Aug  5 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-22
 - Rebuild for ocaml-menhir 20240715 and ocaml-zip 1.12
 

From f53232f95d99ff503768ea412a19d39bda7efc68 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Thu, 9 Jan 2025 16:33:00 -0700
Subject: [PATCH 43/51] OCaml 5.3.0 rebuild for Fedora 42

---
 alt-ergo.spec | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 0086789..32bbaf1 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	22%{?dist}
+Release:	23%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The top-level license files apply to the non-free main distribution of
@@ -271,7 +271,8 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
-* Mon Dec 23 2024 Jerry James <loganjerry@gmail.com> - 2.3.3-22
+* Thu Jan  9 2025 Jerry James <loganjerry@gmail.com> - 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
 

From 360d6af7b6a2338004212f863a4954c4a0c60ba8 Mon Sep 17 00:00:00 2001
From: Fedora Release Engineering <releng@fedoraproject.org>
Date: Thu, 16 Jan 2025 10:55:33 +0000
Subject: [PATCH 44/51] Rebuilt for
 https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 32bbaf1..42ae7d0 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	23%{?dist}
+Release:	24%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The top-level license files apply to the non-free main distribution of
@@ -271,6 +271,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Thu Jan 16 2025 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-24
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild
+
 * Thu Jan  9 2025 Jerry James <loganjerry@gmail.com> - 2.3.3-23
 - OCaml 5.3.0 rebuild for Fedora 42
 - Correct License fields from Apache-2.0 to CECILL-C

From 0ecba542d3ae5f15455070f806d1e8719d0ab793 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Fri, 11 Jul 2025 21:31:19 -0600
Subject: [PATCH 45/51] Rebuild to fix OCaml dependencies

---
 alt-ergo.spec | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 42ae7d0..a6a0b9b 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,12 +13,12 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	24%{?dist}
+Release:	25%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # 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 webiste and also in
+# 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
@@ -271,6 +271,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Fri Jul 11 2025 Jerry James  <loganjerry@gmail.com> - 2.3.3-25
+- Rebuild to fix OCaml dependencies
+
 * Thu Jan 16 2025 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-24
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild
 

From 0f343f3118a455ee41665fcb4d7054bad45bcb17 Mon Sep 17 00:00:00 2001
From: Fedora Release Engineering <releng@fedoraproject.org>
Date: Wed, 23 Jul 2025 16:55:43 +0000
Subject: [PATCH 46/51] Rebuilt for
 https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index a6a0b9b..286ebd7 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	25%{?dist}
+Release:	26%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The top-level license files apply to the non-free main distribution of
@@ -271,6 +271,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Wed Jul 23 2025 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-26
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild
+
 * Fri Jul 11 2025 Jerry James  <loganjerry@gmail.com> - 2.3.3-25
 - Rebuild to fix OCaml dependencies
 

From 7497db4a079aaf57a946d8117f2551370b707285 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Fri, 5 Sep 2025 11:47:45 -0600
Subject: [PATCH 47/51] Rebuild for ocaml-menhir 20250903

---
 alt-ergo.spec | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 286ebd7..9cd6d51 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	26%{?dist}
+Release:	27%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The top-level license files apply to the non-free main distribution of
@@ -203,6 +203,18 @@ 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
@@ -271,10 +283,13 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Fri Sep 05 2025 Jerry James <loganjerry@gmail.com> - 2.3.3-27
+- Rebuild for ocaml-menhir 20250903
+
 * Wed Jul 23 2025 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-26
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild
 
-* Fri Jul 11 2025 Jerry James  <loganjerry@gmail.com> - 2.3.3-25
+* Fri Jul 11 2025 Jerry James <loganjerry@gmail.com> - 2.3.3-25
 - Rebuild to fix OCaml dependencies
 
 * Thu Jan 16 2025 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-24

From 6544e1b439fec5a80666ac1b501f86bca57a69f9 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Tue, 16 Sep 2025 15:08:42 -0600
Subject: [PATCH 48/51] Rebuild for ocaml-menhir 20250912

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 9cd6d51..07ead7c 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	27%{?dist}
+Release:	28%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The top-level license files apply to the non-free main distribution of
@@ -283,6 +283,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Tue Sep 16 2025 Jerry James <loganjerry@gmail.com> - 2.3.3-28
+- Rebuild for ocaml-menhir 20250912
+
 * Fri Sep 05 2025 Jerry James <loganjerry@gmail.com> - 2.3.3-27
 - Rebuild for ocaml-menhir 20250903
 

From c9954a5c37134980826e6a234d43bfa93d43815c Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Tue, 14 Oct 2025 08:57:01 +0100
Subject: [PATCH 49/51] OCaml 5.4.0 rebuild

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 07ead7c..3dea37f 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	28%{?dist}
+Release:	29%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The top-level license files apply to the non-free main distribution of
@@ -283,6 +283,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Tue Oct 14 2025 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-29
+- OCaml 5.4.0 rebuild
+
 * Tue Sep 16 2025 Jerry James <loganjerry@gmail.com> - 2.3.3-28
 - Rebuild for ocaml-menhir 20250912
 

From 94bbf330c30cb16e3da66b53c59d7c49d097edfd Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Fri, 9 Jan 2026 11:59:52 -0700
Subject: [PATCH 50/51] Reflow the description text

---
 alt-ergo.spec | 42 +++++++++++++++++++++++-------------------
 1 file changed, 23 insertions(+), 19 deletions(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 3dea37f..2b2d934 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -64,15 +64,15 @@ 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
@@ -81,17 +81,18 @@ 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.
 
@@ -103,16 +104,18 @@ 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.
 
@@ -124,10 +127,11 @@ Requires:	ocaml-num-devel%{?_isa}
 Requires:	ocaml-ocplib-simplex-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}-%{minorver}.0-free -N -a 2

From 259c21b7500fd47ad98da229be11dbfb664af486 Mon Sep 17 00:00:00 2001
From: Fedora Release Engineering <releng@fedoraproject.org>
Date: Fri, 16 Jan 2026 03:37:12 +0000
Subject: [PATCH 51/51] Rebuilt for
 https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild

---
 alt-ergo.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/alt-ergo.spec b/alt-ergo.spec
index 2b2d934..3adb6d8 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -13,7 +13,7 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	29%{?dist}
+Release:	30%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 # The top-level license files apply to the non-free main distribution of
@@ -287,6 +287,9 @@ cd sources
 %{ocamldir}/%{name}-lib/*.cmti
 
 %changelog
+* Fri Jan 16 2026 Fedora Release Engineering <releng@fedoraproject.org> - 2.3.3-30
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild
+
 * Tue Oct 14 2025 Richard W.M. Jones <rjones@redhat.com> - 2.3.3-29
 - OCaml 5.4.0 rebuild