diff --git a/alt-ergo-inline-error.patch b/alt-ergo-inline-error.patch deleted file mode 100644 index ccb8356..0000000 --- a/alt-ergo-inline-error.patch +++ /dev/null @@ -1,26 +0,0 @@ -Fixes these errors: - -File "lib/util/util.mli", line 62, characters 6-12: -62 | val [@inline always] compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int - ^^^^^^ -Error (warning 53 [misplaced-attribute]): the "inline" attribute cannot appear in this context - -File "lib/util/util.mli", line 64, characters 6-12: -64 | val [@inline always] cmp_lists: 'a list -> 'a list -> ('a -> 'a -> int) -> int - ^^^^^^ -Error (warning 53 [misplaced-attribute]): the "inline" attribute cannot appear in this context - ---- alt-ergo-2.3.0-free/sources/lib/util/util.mli.orig 2022-05-20 01:34:55.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/util.mli 2024-05-05 11:41:32.415674847 -0600 -@@ -59,9 +59,9 @@ val string_of_th_ext : theories_extensio - - Pervasives.compare a b is used if - - *) --val [@inline always] compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int -+val compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int - --val [@inline always] cmp_lists: 'a list -> 'a list -> ('a -> 'a -> int) -> int -+val cmp_lists: 'a list -> 'a list -> ('a -> 'a -> int) -> int - - type matching_env = - { diff --git a/alt-ergo.spec b/alt-ergo.spec index 3adb6d8..c490048 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -13,15 +13,12 @@ ExcludeArch: %{ix86} Name: alt-ergo Version: %{minorver}.%{patchrel} -Release: 30%{?dist} +Release: 17%{?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 website and also in -# sources/tools/gui/main_gui.ml. +# The project as a whole is Apache-2.0. # 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 +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. @@ -45,8 +42,6 @@ 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 @@ -64,74 +59,70 @@ BuildRequires: ocaml-zip-devel Requires: ocaml-alt-ergo-parsers%{?_isa} = %{version}-%{release} -%global _desc %{expand:Alt-Ergo is an automated theorem prover implemented in OCaml. It is based on -CC(X) - a congruence closure algorithm parameterized by an equational theory -X. This algorithm is reminiscent of the Shostak algorithm. Currently CC(X) -is instantiated by the theory of linear arithmetics. Alt-Ergo also contains a -home made SAT-solver and an instantiation mechanism by which it fully supports -quantifiers.} +%global _desc %{expand: +Alt-Ergo is an automated theorem prover implemented in OCaml. It is +based on CC(X) - a congruence closure algorithm parameterized by an +equational theory X. This algorithm is reminiscent of the Shostak +algorithm. Currently CC(X) is instantiated by the theory of linear +arithmetics. Alt-Ergo also contains a home made SAT-solver and an +instantiation mechanism by which it fully supports quantifiers.} -%description -%_desc +%description %_desc %package gui Summary: Graphical front end for Alt-Ergo -License: CECILL-C +License: Apache-2.0 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 +License: Apache-2.0 Requires: ocaml-alt-ergo-lib%{?_isa} = %{version}-%{release} -%description -n ocaml-alt-ergo-parsers -%_desc +%description -n ocaml-alt-ergo-parsers %_desc This package contains the parser library used by the Alt-Ergo SMT solver. %package -n ocaml-alt-ergo-parsers-devel Summary: Development files for ocaml-alt-ergo-parsers -License: CECILL-C +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} 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 +License: Apache-2.0 -%description -n ocaml-alt-ergo-lib -%_desc +%description -n ocaml-alt-ergo-lib %_desc This package is the core of Alt-Ergo as an OCaml library. %package -n ocaml-alt-ergo-lib-devel Summary: Development files for ocaml-alt-ergo-lib -License: CECILL-C +License: Apache-2.0 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 @@ -143,8 +134,6 @@ tar xf %{SOURCE1} %endif %autopatch -p1 - -%conf cd sources cp -p %{SOURCE3} com.ocamlpro.%{name}.desktop @@ -159,11 +148,10 @@ cd - sed -i '/cmxs/d' plugins/{AB-Why3,fm-simplex}/dune %endif -# This is not an autoconf-generated script. Do NOT use %%configure. -./configure --prefix=%{_prefix} --libdir=%{ocamldir} --sharedir=%{ocamldir} - %build +# This is not an autoconf-generated script. Do NOT use %%configure. cd sources +./configure --prefix=%{_prefix} --libdir=%{ocamldir} --sharedir=%{ocamldir} %make_build %install @@ -207,18 +195,6 @@ 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 @@ -287,50 +263,6 @@ 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 - -* Tue Sep 16 2025 Jerry James - 2.3.3-28 -- Rebuild for ocaml-menhir 20250912 - -* Fri Sep 05 2025 Jerry James - 2.3.3-27 -- Rebuild for ocaml-menhir 20250903 - -* Wed Jul 23 2025 Fedora Release Engineering - 2.3.3-26 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild - -* Fri Jul 11 2025 Jerry James - 2.3.3-25 -- Rebuild to fix OCaml dependencies - -* Thu Jan 16 2025 Fedora Release Engineering - 2.3.3-24 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild - -* Thu Jan 9 2025 Jerry James - 2.3.3-23 -- OCaml 5.3.0 rebuild for Fedora 42 -- Correct License fields from Apache-2.0 to CECILL-C -- Do configuration steps in %%conf - -* Mon Aug 5 2024 Jerry James - 2.3.3-22 -- Rebuild for ocaml-menhir 20240715 and ocaml-zip 1.12 - -* Wed Jul 17 2024 Fedora Release Engineering - 2.3.3-21 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild - -* Tue Jul 16 2024 Jerry James - 2.3.3-20 -- Rebuild for ocaml-zarith 1.14 - -* Wed Jun 19 2024 Richard W.M. Jones - 2.3.3-19 -- OCaml 5.2.0 ppc64le fix - -* Wed May 29 2024 Richard W.M. Jones - 2.3.3-18 -- OCaml 5.2.0 for Fedora 41 - -* Thu May 23 2024 Jerry James - 2.3.3-17 -- Add patch to fix misplaced inline attributes - * Fri Feb 2 2024 Jerry James - 2.3.3-17 - Rebuild for changed ocamlx(Dynlink) hash