Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild

- Do configuration steps in %conf

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 =
+   {

alt-ergo.spec

@@ -13,12 +13,15 @@ ExcludeArch: %{ix86}
 
 Name:		alt-ergo
 Version:	%{minorver}.%{patchrel}
-Release:	17%{?dist}
+Release:	30%{?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 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:	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.
@@ -42,6 +45,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
@@ -59,70 +64,74 @@ BuildRequires:	ocaml-zip-devel
 
 Requires:	ocaml-alt-ergo-parsers%{?_isa} = %{version}-%{release}
 
-%global _desc %{expand:
-Alt-Ergo is an automated theorem prover implemented in OCaml. It is
-based on CC(X) - a congruence closure algorithm parameterized by an
-equational theory X. This algorithm is reminiscent of the Shostak
-algorithm. Currently CC(X) is instantiated by the theory of linear
-arithmetics. Alt-Ergo also contains a home made SAT-solver and an
-instantiation mechanism by which it fully supports quantifiers.}
+%global _desc %{expand:Alt-Ergo is an automated theorem prover implemented in OCaml.  It is based on
+CC(X) - a congruence closure algorithm parameterized by an equational theory
+X.  This algorithm is reminiscent of the Shostak algorithm.  Currently CC(X)
+is instantiated by the theory of linear arithmetics.  Alt-Ergo also contains a
+home made SAT-solver and an instantiation mechanism by which it fully supports
+quantifiers.}
 
-%description %_desc
+%description
+%_desc
 
 %package gui
 Summary:	Graphical front end for Alt-Ergo
-License:	Apache-2.0
+License:	CECILL-C
 Requires:	%{name}%{?_isa} = %{version}-%{release}
 Requires:	gtksourceview2
 Requires:	hicolor-icon-theme
 
-%description gui %_desc
+%description gui
+%_desc
 
-This package contains a graphical front end for the Alt-Ergo theorem
-prover.
+This package contains a graphical front end for the Alt-Ergo theorem prover.
 
 %package -n ocaml-alt-ergo-parsers
 Summary:	Parser library used by the Alt-Ergo SMT solver
-License:	Apache-2.0
+License:	CECILL-C
 Requires:	ocaml-alt-ergo-lib%{?_isa} = %{version}-%{release}
 
-%description -n ocaml-alt-ergo-parsers %_desc
+%description -n ocaml-alt-ergo-parsers
+%_desc
 
 This package contains the parser library used by the Alt-Ergo SMT solver.
 
 %package -n ocaml-alt-ergo-parsers-devel
 Summary:	Development files for ocaml-alt-ergo-parsers
-License:	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}
 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:	Apache-2.0
+License:	CECILL-C
 
-%description -n ocaml-alt-ergo-lib %_desc
+%description -n ocaml-alt-ergo-lib
+%_desc
 
 This package is the core of Alt-Ergo as an OCaml library.
 
 %package -n ocaml-alt-ergo-lib-devel
 Summary:	Development files for ocaml-alt-ergo-lib
-License:	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}
 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
@@ -134,6 +143,8 @@ tar xf %{SOURCE1}
 %endif
 
 %autopatch -p1
+
+%conf
 cd sources
 cp -p %{SOURCE3} com.ocamlpro.%{name}.desktop
 
@@ -148,10 +159,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
@@ -195,6 +207,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
@@ -263,6 +287,50 @@ 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
+
+* 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
+
+* 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
+
+* 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
+- 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
+
+* 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
+
+* 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.3-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