diff --git a/alt-ergo.spec b/alt-ergo.spec index 46ce45a..3adb6d8 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: 30%{?dist} Summary: Automated theorem prover including linear arithmetic # The top-level license files apply to the non-free main distribution of @@ -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 @@ -139,6 +143,8 @@ tar xf %{SOURCE1} %endif %autopatch -p1 + +%conf cd sources cp -p %{SOURCE3} com.ocamlpro.%{name}.desktop @@ -153,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 @@ -200,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 @@ -268,9 +287,31 @@ cd sources %{ocamldir}/%{name}-lib/*.cmti %changelog -* Wed Jan 29 2025 Jerry James - 2.3.%{patchrel}-23 -- OCaml 5.2.1 rebuild for Fedora 41 +* 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