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.metainfo.xml b/alt-ergo.metainfo.xml index cdb417e..cff34da 100644 --- a/alt-ergo.metainfo.xml +++ b/alt-ergo.metainfo.xml @@ -20,15 +20,15 @@ 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 - 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 - + altgr-ergo diff --git a/alt-ergo.spec b/alt-ergo.spec index 2f4e937..3adb6d8 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -1,25 +1,27 @@ +# 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. -%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 up appropriately. +# directory. Use this to set up everything appropriately. %global minorver 2.3 %global patchrel 3 Name: alt-ergo Version: %{minorver}.%{patchrel} -Release: 3%{?dist} +Release: 30%{?dist} Summary: Automated theorem prover including linear arithmetic -License: ASL 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: 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. @@ -43,10 +45,12 @@ 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: appstream BuildRequires: desktop-file-utils BuildRequires: gtksourceview2-devel +BuildRequires: libappstream-glib BuildRequires: make BuildRequires: ocaml >= 4.04.0 BuildRequires: ocaml-dune @@ -60,65 +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: 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: 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: 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: 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: 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 @@ -130,6 +143,8 @@ tar xf %{SOURCE1} %endif %autopatch -p1 + +%conf cd sources cp -p %{SOURCE3} com.ocamlpro.%{name}.desktop @@ -139,10 +154,16 @@ unzip p4_34.why.zip rm p4_34.why.zip cd - -%build +%ifnarch %{ocaml_native_compiler} +# Do not require native plugins +sed -i '/cmxs/d' plugins/{AB-Why3,fm-simplex}/dune +%endif + # 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 @@ -178,7 +199,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 @@ -186,13 +207,24 @@ 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 %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 +262,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 @@ -241,16 +274,112 @@ 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 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 + +* 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 + +* 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 + +* 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 + +* 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 + +* 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 + +* 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 + +* 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 + +* 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