Compare commits

...
Sign in to create a new pull request.

10 commits

Author SHA1 Message Date
Fedora Release Engineering
259c21b750 Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild 2026-01-16 03:37:12 +00:00
Jerry James
94bbf330c3 Reflow the description text 2026-01-09 12:01:03 -07:00
Richard W.M. Jones
c9954a5c37 OCaml 5.4.0 rebuild 2025-10-14 08:57:01 +01:00
Jerry James
6544e1b439 Rebuild for ocaml-menhir 20250912 2025-09-16 15:08:42 -06:00
Jerry James
7497db4a07 Rebuild for ocaml-menhir 20250903 2025-09-05 11:47:45 -06:00
Fedora Release Engineering
0f343f3118 Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild 2025-07-23 16:55:43 +00:00
Jerry James
0ecba542d3 Rebuild to fix OCaml dependencies 2025-07-11 21:31:19 -06:00
Fedora Release Engineering
360d6af7b6 Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild 2025-01-16 10:55:33 +00:00
Jerry James
f53232f95d OCaml 5.3.0 rebuild for Fedora 42 2025-01-09 16:33:00 -07:00
Jerry James
75bbe3f8fc Correct License fields from Apache-2.0 to CECILL-C
- Do configuration steps in %conf
2024-12-27 11:45:43 -07:00

View file

@ -13,12 +13,15 @@ ExcludeArch: %{ix86}
Name: alt-ergo
Version: %{minorver}.%{patchrel}
Release: 22%{?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.
@ -61,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
@ -136,6 +143,8 @@ tar xf %{SOURCE1}
%endif
%autopatch -p1
%conf
cd sources
cp -p %{SOURCE3} com.ocamlpro.%{name}.desktop
@ -150,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
@ -197,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
@ -265,6 +287,32 @@ 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