From 61ce442efc897a263eb05d38a594e189056e5ca0 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 11 Aug 2022 09:24:41 -0600 Subject: [PATCH 01/34] 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 - 2.3.3-3 +- Convert License tag to SPDX +- Note that the AB plugin has a different license + * Wed Jul 20 2022 Fedora Release Engineering - 2.3.3-3 - Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild From 3901efd195b280f907eb901a9466331f81a6bd8a Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Wed, 18 Jan 2023 21:38:44 +0000 Subject: [PATCH 02/34] Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- 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 - 2.3.3-4 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild + * Thu Aug 11 2022 Jerry James - 2.3.3-3 - Convert License tag to SPDX - Note that the AB plugin has a different license From 11fc19a34cfcf1ec30b85826acb7dec363367fae Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 24 Jan 2023 19:30:31 +0000 Subject: [PATCH 03/34] 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 - 2.3.3-5 +- Rebuild OCaml packages for F38 + * Wed Jan 18 2023 Fedora Release Engineering - 2.3.3-4 - Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild From 04eaf57e3a54133ed8291fe7604ae3e96321bbff Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 24 Mar 2023 10:04:51 -0600 Subject: [PATCH 04/34] 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 @@ com.ocamlpro.alt-ergo.desktop - http://jjames.fedorapeople.org/alt-ergo/altgr-ergo-screenshot.png + https://jjames.fedorapeople.org/alt-ergo/altgr-ergo-screenshot.png Basic Alt-Ergo usage @@ -28,7 +28,7 @@ https://alt-ergo.ocamlpro.com/ https://github.com/OCamlPro/alt-ergo/issues https://alt-ergo.ocamlpro.com/#services - + altgr-ergo diff --git a/alt-ergo.spec b/alt-ergo.spec index 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 - 2.3.3-6 +- Dune 3.7.0 changed the install location of mli files + * Tue Jan 24 2023 Richard W.M. Jones - 2.3.3-5 - Rebuild OCaml packages for F38 From f2cbc74c5e4c2f37a3c9d0863af4df287d9ebd7c Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 10 Jul 2023 16:57:48 -0600 Subject: [PATCH 05/34] 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 - 2.3.3-7 +- OCaml 5.0.0 rebuild + * Fri Mar 24 2023 Jerry James - 2.3.3-6 - Dune 3.7.0 changed the install location of mli files From 5ec9dcf52b9add353269928daa426320844dbe04 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 11 Jul 2023 11:36:25 +0100 Subject: [PATCH 06/34] 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" Date: Wed, 12 Jul 2023 01:39:34 +0100 Subject: [PATCH 07/34] 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 - 2.3.3-8 +- OCaml 5.0 rebuild for Fedora 39 + * Mon Jul 10 2023 Jerry James - 2.3.3-7 - OCaml 5.0.0 rebuild From 961a793aa4bb4160a553bf4be613376afa67db9e Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 18 Jul 2023 11:35:04 -0600 Subject: [PATCH 08/34] 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 - 2.3.3-8 +- Validate appdata with appstream-util + * Wed Jul 12 2023 Richard W.M. Jones - 2.3.3-8 - OCaml 5.0 rebuild for Fedora 39 From dcf60c5f1e5fce4586fcc17c3d839665efe9065b Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Wed, 19 Jul 2023 13:10:45 +0000 Subject: [PATCH 09/34] Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- 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 - 2.3.3-9 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild + * Tue Jul 18 2023 Jerry James - 2.3.3-8 - Validate appdata with appstream-util From 17e8a91f5087c14bd5ce2be2af1b5ca82b7c86ed Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 27 Jul 2023 10:22:59 -0600 Subject: [PATCH 10/34] 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 - 2.3.3-10 +- Rebuild for ocaml-zarith 1.13 + * Wed Jul 19 2023 Fedora Release Engineering - 2.3.3-9 - Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild From 95ebe8b78e5aeb4a41cc8f5bd76c4e163287f3db Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Thu, 5 Oct 2023 21:27:10 +0100 Subject: [PATCH 11/34] 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 - 2.3.3-11 +- OCaml 5.1 rebuild for Fedora 40 + * Thu Jul 27 2023 Jerry James - 2.3.3-10 - Rebuild for ocaml-zarith 1.13 From 03925961950310a6b50a6f9344c3a25cb3a171cb Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 12 Dec 2023 18:19:33 +0000 Subject: [PATCH 12/34] 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 - 2.3.3-12 +- OCaml 5.1.1 rebuild for Fedora 40 + * Thu Oct 05 2023 Richard W.M. Jones - 2.3.3-11 - OCaml 5.1 rebuild for Fedora 40 From f83c022bb375f52677563d9b14e0a14dd55f539c Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 18 Dec 2023 20:42:39 +0000 Subject: [PATCH 13/34] 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 - 2.3.3-13 +- OCaml 5.1.1 + s390x code gen fix for Fedora 40 + * Tue Dec 12 2023 Richard W.M. Jones - 2.3.3-12 - OCaml 5.1.1 rebuild for Fedora 40 From d55e3db9b2f86f547ee1fa44d2569c776650367d Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 18 Dec 2023 20:31:53 -0700 Subject: [PATCH 14/34] 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 @@ Basic Alt-Ergo usage - loganjerry@gmail.com + alt-ergo-maintainers@fedoraproject.org https://alt-ergo.ocamlpro.com/ https://github.com/OCamlPro/alt-ergo/issues https://alt-ergo.ocamlpro.com/#services From 2d515533aeafb538abc92fca4fbd324a57ea4b7f Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 2 Jan 2024 11:28:58 -0700 Subject: [PATCH 15/34] 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 - 2.3.3-14 +- Rebuild for ocaml-num and ocaml-menhir 20231231 + * Mon Dec 18 2023 Richard W.M. Jones - 2.3.3-13 - OCaml 5.1.1 + s390x code gen fix for Fedora 40 From ba198bf5cf00926f98692aba297f09a1d10c2e8f Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 19 Jan 2024 12:46:18 +0000 Subject: [PATCH 16/34] 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 - 2.3.3-15 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild + * Tue Jan 2 2024 Jerry James - 2.3.3-14 - Rebuild for ocaml-num and ocaml-menhir 20231231 From 89e6861d48bb9d9a10b3e1174ec747ae2e0954ed Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Mon, 22 Jan 2024 22:57:19 +0000 Subject: [PATCH 17/34] 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 - 2.3.3-16 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild + * Fri Jan 19 2024 Fedora Release Engineering - 2.3.3-15 - Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild From bd0a00952534e977b2063fa4b8604bd363d96541 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 2 Feb 2024 10:09:48 -0700 Subject: [PATCH 18/34] 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 - 2.3.3-17 +- Rebuild for changed ocamlx(Dynlink) hash + * Mon Jan 22 2024 Fedora Release Engineering - 2.3.3-16 - Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild From ce64caea9cd1161c27605f9414443ed7d632a5e5 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 23 May 2024 10:57:15 -0600 Subject: [PATCH 19/34] 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 - 2.3.%{patchrel}-17 +- Add patch to fix misplaced inline attributes + * Fri Feb 2 2024 Jerry James - 2.3.3-17 - Rebuild for changed ocamlx(Dynlink) hash From 8d4dec6e83e7c845f311c787f4f077609a1d835c Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 29 May 2024 23:50:30 +0100 Subject: [PATCH 20/34] 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 - 2.3.3-18 +- OCaml 5.2.0 for Fedora 41 + * Thu May 23 2024 Jerry James - 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" Date: Wed, 19 Jun 2024 14:26:21 +0100 Subject: [PATCH 21/34] 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 - 2.3.3-19 +- OCaml 5.2.0 ppc64le fix + * Wed May 29 2024 Richard W.M. Jones - 2.3.3-18 - OCaml 5.2.0 for Fedora 41 From fa4007b53c733a341532d3b5b401b91900a9ed1a Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 16 Jul 2024 10:39:18 -0600 Subject: [PATCH 22/34] 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 - 2.3.3-20 +- Rebuild for ocaml-zarith 1.14 + * Wed Jun 19 2024 Richard W.M. Jones - 2.3.3-19 - OCaml 5.2.0 ppc64le fix * Wed May 29 2024 Richard W.M. Jones - 2.3.3-18 - OCaml 5.2.0 for Fedora 41 -* Thu May 23 2024 Jerry James - 2.3.%{patchrel}-17 +* Thu May 23 2024 Jerry James - 2.3.3-17 - Add patch to fix misplaced inline attributes * Fri Feb 2 2024 Jerry James - 2.3.3-17 From d49408568a28b9a414e38f1bb29522c6f17b238a Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Wed, 17 Jul 2024 16:53:51 +0000 Subject: [PATCH 23/34] 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 - 2.3.3-21 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild + * Tue Jul 16 2024 Jerry James - 2.3.3-20 - Rebuild for ocaml-zarith 1.14 From 51625d920756664142ce0d95e359579fcd68313b Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 5 Aug 2024 10:32:00 -0600 Subject: [PATCH 24/34] 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 - 2.3.3-22 +- Rebuild for ocaml-menhir 20240715 and ocaml-zip 1.12 + * Wed Jul 17 2024 Fedora Release Engineering - 2.3.3-21 - Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild From 75bbe3f8fc8409a54c479a5fa476d3261bb4d8ad Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 27 Dec 2024 11:45:43 -0700 Subject: [PATCH 25/34] 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 - 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 - 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 Date: Thu, 9 Jan 2025 16:33:00 -0700 Subject: [PATCH 26/34] 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 - 2.3.3-22 +* Thu Jan 9 2025 Jerry James - 2.3.3-23 +- OCaml 5.3.0 rebuild for Fedora 42 - Correct License fields from Apache-2.0 to CECILL-C - Do configuration steps in %%conf From 360d6af7b6a2338004212f863a4954c4a0c60ba8 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Thu, 16 Jan 2025 10:55:33 +0000 Subject: [PATCH 27/34] 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 - 2.3.3-24 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild + * Thu Jan 9 2025 Jerry James - 2.3.3-23 - OCaml 5.3.0 rebuild for Fedora 42 - Correct License fields from Apache-2.0 to CECILL-C From 0ecba542d3ae5f15455070f806d1e8719d0ab793 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 11 Jul 2025 21:31:19 -0600 Subject: [PATCH 28/34] 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 - 2.3.3-25 +- Rebuild to fix OCaml dependencies + * Thu Jan 16 2025 Fedora Release Engineering - 2.3.3-24 - Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild From 0f343f3118a455ee41665fcb4d7054bad45bcb17 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Wed, 23 Jul 2025 16:55:43 +0000 Subject: [PATCH 29/34] 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 - 2.3.3-26 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild + * Fri Jul 11 2025 Jerry James - 2.3.3-25 - Rebuild to fix OCaml dependencies From 7497db4a079aaf57a946d8117f2551370b707285 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 5 Sep 2025 11:47:45 -0600 Subject: [PATCH 30/34] 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 - 2.3.3-27 +- Rebuild for ocaml-menhir 20250903 + * Wed Jul 23 2025 Fedora Release Engineering - 2.3.3-26 - Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild -* Fri Jul 11 2025 Jerry James - 2.3.3-25 +* Fri Jul 11 2025 Jerry James - 2.3.3-25 - Rebuild to fix OCaml dependencies * Thu Jan 16 2025 Fedora Release Engineering - 2.3.3-24 From 6544e1b439fec5a80666ac1b501f86bca57a69f9 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 16 Sep 2025 15:08:42 -0600 Subject: [PATCH 31/34] 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 - 2.3.3-28 +- Rebuild for ocaml-menhir 20250912 + * Fri Sep 05 2025 Jerry James - 2.3.3-27 - Rebuild for ocaml-menhir 20250903 From c9954a5c37134980826e6a234d43bfa93d43815c Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 14 Oct 2025 08:57:01 +0100 Subject: [PATCH 32/34] 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 - 2.3.3-29 +- OCaml 5.4.0 rebuild + * Tue Sep 16 2025 Jerry James - 2.3.3-28 - Rebuild for ocaml-menhir 20250912 From 94bbf330c30cb16e3da66b53c59d7c49d097edfd Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 9 Jan 2026 11:59:52 -0700 Subject: [PATCH 33/34] 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 Date: Fri, 16 Jan 2026 03:37:12 +0000 Subject: [PATCH 34/34] 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 - 2.3.3-30 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild + * Tue Oct 14 2025 Richard W.M. Jones - 2.3.3-29 - OCaml 5.4.0 rebuild