From ec408a198fd117b21cd387201d47f94ad5e22e4b Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Thu, 31 Jan 2019 13:13:44 +0000 Subject: [PATCH 01/77] - Rebuilt for https://fedoraproject.org/wiki/Fedora_30_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 9df0f9f..a4c5a33 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -9,7 +9,7 @@ Name: alt-ergo Version: 1.30 -Release: 15%{?dist} +Release: 16%{?dist} Summary: Automated theorem prover including linear arithmetic License: CeCILL-C @@ -137,6 +137,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Thu Jan 31 2019 Fedora Release Engineering - 1.30-16 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild + * Thu Jul 12 2018 Fedora Release Engineering - 1.30-15 - Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild From aa097b342b5124e871618848830bd3df6f529868 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 5 Jun 2019 19:55:51 -0600 Subject: [PATCH 02/77] Update to version 2.0.0. Also: - Add -newline patch to fix FTBFS. - Add a 256x256 icon. --- .gitignore | 4 +--- alt-ergo-2.0.0-newline.patch | 18 ++++++++++++++++++ alt-ergo.spec | 28 ++++++++++++++++------------ sources | 4 ++-- 4 files changed, 37 insertions(+), 17 deletions(-) create mode 100644 alt-ergo-2.0.0-newline.patch diff --git a/.gitignore b/.gitignore index e139737..7da3b50 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,2 @@ /alt-ergo-icons.tar.xz -/alt-ergo-0.99.1.tar.gz -/alt-ergo-1.01.tar.gz -/alt-ergo-1.30.tar.gz +/alt-ergo-*.tar.gz diff --git a/alt-ergo-2.0.0-newline.patch b/alt-ergo-2.0.0-newline.patch new file mode 100644 index 0000000..ed46c53 --- /dev/null +++ b/alt-ergo-2.0.0-newline.patch @@ -0,0 +1,18 @@ +--- alt-ergo-2.0.0/Makefile.users.orig 2017-11-14 10:01:38.000000000 -0700 ++++ alt-ergo-2.0.0/Makefile.users 2019-05-31 10:27:59.204322901 -0600 +@@ -180,12 +180,12 @@ lib/util/cmdline_parser.ml: config.statu + @echo "(* parse_args () should be called as soon as possible (put earlier" > lib/util/cmdline_parser.ml + @echo " when linking) because some choices during compilation depend on" >> lib/util/cmdline_parser.ml + @echo " given options (e.g. dfs-sat)" >> lib/util/cmdline_parser.ml +- @echo "\n -> The following call:" >> lib/util/cmdline_parser.ml ++ @echo -e "\n -> The following call:" >> lib/util/cmdline_parser.ml + @echo " 1 - should be kept when builtind Alt-Ergo tools" >> lib/util/cmdline_parser.ml + @echo " 2 - should be removed to build and use only the library." >> lib/util/cmdline_parser.ml +- @echo "\n Alternatively to 2, one can just remove cmdline_parser.cmo/cmx in" >> lib/util/cmdline_parser.ml ++ @echo -e "\n Alternatively to 2, one can just remove cmdline_parser.cmo/cmx in" >> lib/util/cmdline_parser.ml + @echo " Makefile.users *)" >> lib/util/cmdline_parser.ml +- @echo "\nlet () = Options.parse_cmdline_arguments ()" >> lib/util/cmdline_parser.ml ++ @echo -e "\nlet () = Options.parse_cmdline_arguments ()" >> lib/util/cmdline_parser.ml + + META: config.status + @echo "description = \"API of Alt-Ergo: An automatic theorem prover dedicated to program verification\"" > META diff --git a/alt-ergo.spec b/alt-ergo.spec index a4c5a33..b9c3c97 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,10 +8,10 @@ %endif Name: alt-ergo -Version: 1.30 -Release: 16%{?dist} +Version: 2.0.0 +Release: 1%{?dist} Summary: Automated theorem prover including linear arithmetic -License: CeCILL-C +License: ASL 2.0 URL: http://alt-ergo.ocamlpro.com/ Source0: http://alt-ergo.ocamlpro.com/http/%{name}-%{version}/%{name}-%{version}.tar.gz @@ -21,15 +21,18 @@ Source2: %{name}.desktop Source3: %{name}.appdata.xml # Use the asmrun_pic variant when linking the binary. -Patch1: alt-ergo-1.30-use-pic.patch +Patch0: %{name}-1.30-use-pic.patch + +# Process embedded newlines in echo commands +Patch1: %{name}-2.0.0-newline.patch BuildRequires: desktop-file-utils BuildRequires: gtksourceview2-devel BuildRequires: ocaml BuildRequires: ocaml-findlib BuildRequires: ocaml-lablgtk-devel +BuildRequires: ocaml-menhir-devel BuildRequires: ocaml-num-devel -BuildRequires: ocaml-ocamlgraph-devel BuildRequires: ocaml-ocplib-simplex-devel BuildRequires: ocaml-zarith-devel BuildRequires: ocaml-zip-devel @@ -58,17 +61,12 @@ A graphical front end for the alt-ergo theorem prover. %setup -q %setup -q -T -D -a 1 +%patch0 -p1 %patch1 -p1 cp -p %{SOURCE2} . -# Fix encoding -iconv -f ISO-8859-1 -t UTF-8 -o LICENSE.utf8 LICENSE -touch -r LICENSE LICENSE.utf8 -mv -f LICENSE.utf8 LICENSE - # Use Fedora LDFLAGS -sed -i "s|^OFLAGS =.*|& -g|" Makefile.users for arg in $RPM_LD_FLAGS; do sed -i "s|^OFLAGS =.*-g|& -ccopt $arg|" Makefile.users done @@ -125,9 +123,10 @@ done %files %doc README.md CHANGES examples -%license COPYING.md LICENSE +%license COPYING.md LICENSE.md %{_bindir}/%{name} %{_mandir}/man1/alt-ergo.1.* +%{_libdir}/%{name}/ %files gui %{_bindir}/altgr-ergo @@ -137,6 +136,11 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Wed Jun 5 2019 Jerry James - 2.0.0-1 +- Update to version 2.0.0 +- Add -newline patch to fix FTBFS +- Add a 256x256 icon + * Thu Jan 31 2019 Fedora Release Engineering - 1.30-16 - Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild diff --git a/sources b/sources index 6f0dcae..7b8dc34 100644 --- a/sources +++ b/sources @@ -1,2 +1,2 @@ -c7100ebd625fbd7d3e5247dbac689748 alt-ergo-1.30.tar.gz -90052f03870cc94a1ceb8ac3fae77b7b alt-ergo-icons.tar.xz +SHA512 (alt-ergo-2.0.0.tar.gz) = aaf8d948a8bd77cd1ff0d8fffcaf0dd30a906a90769c4c463705c212c4b12e1bd124024b50cd244334c96088b367a8a41ae2a16876732f116c9bd418be4ec341 +SHA512 (alt-ergo-icons.tar.xz) = cb2e93bab3359f6f198e80e3e68840ed4b25a213b61f388a2de8abc299fd3c89240f64f610290ac89e6005088c484b2718a68ec18063076f73d7871a38ee038f From 84816c8abd454e51a4304fc2dedbd6c380c84d8d Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 8 Jun 2019 20:18:21 -0600 Subject: [PATCH 03/77] Add a workaround for https://github.com/ocaml/ocaml/issues/7608. --- alt-ergo.spec | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/alt-ergo.spec b/alt-ergo.spec index b9c3c97..2dbf9af 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -71,6 +71,12 @@ for arg in $RPM_LD_FLAGS; do sed -i "s|^OFLAGS =.*-g|& -ccopt $arg|" Makefile.users done +%ifarch %{arm} +# Work around for https://github.com/ocaml/ocaml/issues/7608 +# Remove this once a released ocaml version fixes that issue. +sed -i "s|^OFLAGS =|& -fno-thumb|" Makefile.users +%endif + %build %configure From 87d647fe87c70470607956527e7e20b2aa246235 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Wed, 24 Jul 2019 17:48:33 +0000 Subject: [PATCH 04/77] - Rebuilt for https://fedoraproject.org/wiki/Fedora_31_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 2dbf9af..661bf12 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -9,7 +9,7 @@ Name: alt-ergo Version: 2.0.0 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -142,6 +142,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Wed Jul 24 2019 Fedora Release Engineering - 2.0.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild + * Wed Jun 5 2019 Jerry James - 2.0.0-1 - Update to version 2.0.0 - Add -newline patch to fix FTBFS From 004cf953dfdaf2aad39b94581beaa221db0959be Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Thu, 1 Aug 2019 00:02:40 +0100 Subject: [PATCH 05/77] OCaml 4.08.1 (rc2) rebuild. --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index 661bf12..e013532 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -9,7 +9,7 @@ Name: alt-ergo Version: 2.0.0 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -142,6 +142,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Wed Jul 31 2019 Richard W.M. Jones - 2.0.0-3 +- OCaml 4.08.1 (rc2) rebuild. + * Wed Jul 24 2019 Fedora Release Engineering - 2.0.0-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild From 199f1599a88273e280495297bda3d0a7ff7a147a Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Fri, 16 Aug 2019 16:28:54 +0100 Subject: [PATCH 06/77] OCaml 4.08.1 (final) rebuild. --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index e013532..57c7be7 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -9,7 +9,7 @@ Name: alt-ergo Version: 2.0.0 -Release: 3%{?dist} +Release: 4%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -142,6 +142,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Fri Aug 16 2019 Richard W.M. Jones - 2.0.0-4 +- OCaml 4.08.1 (final) rebuild. + * Wed Jul 31 2019 Richard W.M. Jones - 2.0.0-3 - OCaml 4.08.1 (rc2) rebuild. From 23076e58d83d7afbd1be1ede01dd493184479d4f Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 6 Sep 2019 09:11:18 -0600 Subject: [PATCH 07/77] Rebuild for ocaml-zarith 1.9. --- alt-ergo.spec | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index 57c7be7..cca9c21 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -2,14 +2,13 @@ # https://www.redhat.com/archives/fedora-packaging/2008-August/msg00017.html # and ocaml-ocamlgraph spec file for a discussion of this issue. -%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0) -%if !%{opt} +%ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif Name: alt-ergo Version: 2.0.0 -Release: 4%{?dist} +Release: 5%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -51,9 +50,6 @@ Requires: %{name}%{?_isa} = %{version}-%{release} Requires: gtksourceview2 Requires: hicolor-icon-theme -Requires(post): coreutils -Requires(postun): coreutils - %description gui A graphical front end for the alt-ergo theorem prover. @@ -80,7 +76,7 @@ sed -i "s|^OFLAGS =|& -fno-thumb|" Makefile.users %build %configure -%if ! %{opt} +%ifnarch %{ocaml_native_compiler} %global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLLEX=ocamllex %else %global opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt @@ -142,6 +138,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Fri Sep 6 2019 Jerry James - 2.0.0-5 +- Rebuild for ocaml-zarith 1.9 + * Fri Aug 16 2019 Richard W.M. Jones - 2.0.0-4 - OCaml 4.08.1 (final) rebuild. From 44c4aa7df61e2b51f33bb4ab4f83dc5ea119a802 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Fri, 6 Dec 2019 13:33:22 +0000 Subject: [PATCH 08/77] OCaml 4.09.0 (final) rebuild. --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index cca9c21..9a9cf01 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.0.0 -Release: 5%{?dist} +Release: 6%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -138,6 +138,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Fri Dec 06 2019 Richard W.M. Jones - 2.0.0-6 +- OCaml 4.09.0 (final) rebuild. + * Fri Sep 6 2019 Jerry James - 2.0.0-5 - Rebuild for ocaml-zarith 1.9 From 4ecc6462d6fa761537040615f95c33b982ba1959 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Sun, 19 Jan 2020 14:47:50 +0000 Subject: [PATCH 09/77] OCaml 4.10.0+beta1 rebuild. --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index 9a9cf01..67df2ca 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.0.0 -Release: 6%{?dist} +Release: 7%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -138,6 +138,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Sun Jan 19 2020 Richard W.M. Jones - 2.0.0-7 +- OCaml 4.10.0+beta1 rebuild. + * Fri Dec 06 2019 Richard W.M. Jones - 2.0.0-6 - OCaml 4.09.0 (final) rebuild. From e409180af0727ff22f2dc79fdd36f7e1f44a1fdf Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Tue, 28 Jan 2020 11:28:29 +0000 Subject: [PATCH 10/77] - Rebuilt for https://fedoraproject.org/wiki/Fedora_32_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 67df2ca..9d5ee02 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.0.0 -Release: 7%{?dist} +Release: 8%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -138,6 +138,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Tue Jan 28 2020 Fedora Release Engineering - 2.0.0-8 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild + * Sun Jan 19 2020 Richard W.M. Jones - 2.0.0-7 - OCaml 4.10.0+beta1 rebuild. From 41c768f03f642a8abed7e8909b1b23fd0ba401bf Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 26 Feb 2020 16:40:16 +0000 Subject: [PATCH 11/77] OCaml 4.10.0 final. --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index 9d5ee02..c25911b 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.0.0 -Release: 8%{?dist} +Release: 9%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -138,6 +138,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Wed Feb 26 2020 Richard W.M. Jones - 2.0.0-9 +- OCaml 4.10.0 final. + * Tue Jan 28 2020 Fedora Release Engineering - 2.0.0-8 - Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild From 0e23a449762820cd92c4c25d92b762cb122d94e7 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 25 Mar 2020 13:27:34 -0600 Subject: [PATCH 12/77] Rebuild for ocaml-menhir 20200211. --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index c25911b..2d92e68 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.0.0 -Release: 9%{?dist} +Release: 10%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -138,6 +138,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Tue Mar 24 2020 Jerry James - 2.0.0-10 +- Rebuild for ocaml-menhir 20200211 + * Wed Feb 26 2020 Richard W.M. Jones - 2.0.0-9 - OCaml 4.10.0 final. From 15bcc3b4c1996cdf02c8b39444d71e2a511ff156 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 1 Apr 2020 10:26:17 -0600 Subject: [PATCH 13/77] Rebuild for ocaml-zip 1.10. --- alt-ergo.spec | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index 2d92e68..1c81541 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.0.0 -Release: 10%{?dist} +Release: 11%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -67,6 +67,9 @@ for arg in $RPM_LD_FLAGS; do sed -i "s|^OFLAGS =.*-g|& -ccopt $arg|" Makefile.users done +# Look for zip instead of camlzip +sed -i 's/camlzip/zip/g' configure opam + %ifarch %{arm} # Work around for https://github.com/ocaml/ocaml/issues/7608 # Remove this once a released ocaml version fixes that issue. @@ -138,6 +141,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Mon Mar 30 2020 Jerry James - 2.0.0-11 +- Rebuild for ocaml-zip 1.10 + * Tue Mar 24 2020 Jerry James - 2.0.0-10 - Rebuild for ocaml-menhir 20200211 From d1cd03adbed832a6d1ea2c7b94cf9292643c78cb Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Fri, 3 Apr 2020 13:38:22 +0100 Subject: [PATCH 14/77] Update all OCaml dependencies for RPM 4.16. --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index 1c81541..7d95357 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.0.0 -Release: 11%{?dist} +Release: 12%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -141,6 +141,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Fri Apr 03 2020 Richard W.M. Jones - 2.0.0-12 +- Update all OCaml dependencies for RPM 4.16. + * Mon Mar 30 2020 Jerry James - 2.0.0-11 - Rebuild for ocaml-zip 1.10 From 220d1db4409f1fdfcc44bde167a04c704c8ccb3a Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 8 Apr 2020 21:14:29 -0600 Subject: [PATCH 15/77] Filter out Requires for private interfaces we do not Provide. --- alt-ergo.rpmlintrc | 14 ++++++++++++++ alt-ergo.spec | 8 +++++++- 2 files changed, 21 insertions(+), 1 deletion(-) create mode 100644 alt-ergo.rpmlintrc diff --git a/alt-ergo.rpmlintrc b/alt-ergo.rpmlintrc new file mode 100644 index 0000000..7a6e1a4 --- /dev/null +++ b/alt-ergo.rpmlintrc @@ -0,0 +1,14 @@ +# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON +# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors + +# The dictionary lacks some technical words +addFilter(r'W: spelling-error .* (arithmetics|equational|instantiation|parameterized|prover)') + +# Caused by ocaml; this package cannot fix it +addFilter(r'alt-ergo(-gui)?\.[^:]+: E: missing-call-to-chdir-with-chroot') + +# Documentation is in the main package +addFilter(r'alt-ergo-gui\.[^:]+: W: no-documentation') + +# There is no man page for the graphical launcher +addFilter(r'alt-ergo-gui\.[^:]+: W: no-manual-page-for-binary altgr-ergo') diff --git a/alt-ergo.spec b/alt-ergo.spec index 7d95357..b018424 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.0.0 -Release: 12%{?dist} +Release: 13%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -36,6 +36,9 @@ BuildRequires: ocaml-ocplib-simplex-devel BuildRequires: ocaml-zarith-devel BuildRequires: ocaml-zip-devel +# Do not Require private ocaml interfaces that we don't Provide +%global __requires_exclude ocamlx?\\\((Ccx|Com(bine|mands)|Ex(ception|planation)|F(ormula|un_sat)|H(consing|string)|In(equalities|stances)|L(iteral|oc)|Matching_types|Numbers(Interface)?|Options|P(arsed|olynome|rofiling)|S(at_solver(_sig)?|ig|ymbols)|T(erm|heory|imers|y(ped)?)|U(f|se|til))\\\) + %description Alt-Ergo is an automated theorem prover implemented in OCaml. It is based on CC(X) - a congruence closure algorithm parameterized by an @@ -141,6 +144,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Wed Apr 8 2020 Jerry James - 2.0.0-13 +- Filter out Requires for private interfaces we do not Provide + * Fri Apr 03 2020 Richard W.M. Jones - 2.0.0-12 - Update all OCaml dependencies for RPM 4.16. From 60a1450297158b6e4b53e5e4997ed1fbd1024799 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 22 Apr 2020 15:45:05 +0100 Subject: [PATCH 16/77] OCaml 4.11.0 pre-release attempt 2 --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index b018424..0f6493e 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.0.0 -Release: 13%{?dist} +Release: 14%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -144,6 +144,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Wed Apr 22 2020 Richard W.M. Jones - 2.0.0-14 +- OCaml 4.11.0 pre-release attempt 2 + * Wed Apr 8 2020 Jerry James - 2.0.0-13 - Filter out Requires for private interfaces we do not Provide From 941831eb84b83cf2ce35a3a8c1cddbc8933511d0 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 5 May 2020 16:25:31 +0100 Subject: [PATCH 17/77] OCaml 4.11.0+dev2-2020-04-22 rebuild --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index 0f6493e..947569a 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.0.0 -Release: 14%{?dist} +Release: 15%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -144,6 +144,9 @@ done %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog +* Tue May 05 2020 Richard W.M. Jones - 2.0.0-15 +- OCaml 4.11.0+dev2-2020-04-22 rebuild + * Wed Apr 22 2020 Richard W.M. Jones - 2.0.0-14 - OCaml 4.11.0 pre-release attempt 2 From 8d58e8b229178a38dbc868b51d035affd2c568cd Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 19 Jun 2020 15:30:19 -0600 Subject: [PATCH 18/77] Version 2.2.0. Drop upstreamed -newline patch. --- alt-ergo-2.0.0-newline.patch | 18 -------- alt-ergo.spec | 90 +++++++++++++++++++++++++----------- sources | 2 +- 3 files changed, 64 insertions(+), 46 deletions(-) delete mode 100644 alt-ergo-2.0.0-newline.patch diff --git a/alt-ergo-2.0.0-newline.patch b/alt-ergo-2.0.0-newline.patch deleted file mode 100644 index ed46c53..0000000 --- a/alt-ergo-2.0.0-newline.patch +++ /dev/null @@ -1,18 +0,0 @@ ---- alt-ergo-2.0.0/Makefile.users.orig 2017-11-14 10:01:38.000000000 -0700 -+++ alt-ergo-2.0.0/Makefile.users 2019-05-31 10:27:59.204322901 -0600 -@@ -180,12 +180,12 @@ lib/util/cmdline_parser.ml: config.statu - @echo "(* parse_args () should be called as soon as possible (put earlier" > lib/util/cmdline_parser.ml - @echo " when linking) because some choices during compilation depend on" >> lib/util/cmdline_parser.ml - @echo " given options (e.g. dfs-sat)" >> lib/util/cmdline_parser.ml -- @echo "\n -> The following call:" >> lib/util/cmdline_parser.ml -+ @echo -e "\n -> The following call:" >> lib/util/cmdline_parser.ml - @echo " 1 - should be kept when builtind Alt-Ergo tools" >> lib/util/cmdline_parser.ml - @echo " 2 - should be removed to build and use only the library." >> lib/util/cmdline_parser.ml -- @echo "\n Alternatively to 2, one can just remove cmdline_parser.cmo/cmx in" >> lib/util/cmdline_parser.ml -+ @echo -e "\n Alternatively to 2, one can just remove cmdline_parser.cmo/cmx in" >> lib/util/cmdline_parser.ml - @echo " Makefile.users *)" >> lib/util/cmdline_parser.ml -- @echo "\nlet () = Options.parse_cmdline_arguments ()" >> lib/util/cmdline_parser.ml -+ @echo -e "\nlet () = Options.parse_cmdline_arguments ()" >> lib/util/cmdline_parser.ml - - META: config.status - @echo "description = \"API of Alt-Ergo: An automatic theorem prover dedicated to program verification\"" > META diff --git a/alt-ergo.spec b/alt-ergo.spec index 947569a..98b16ed 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -7,23 +7,20 @@ %endif Name: alt-ergo -Version: 2.0.0 -Release: 15%{?dist} +Version: 2.2.0 +Release: 1%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 -URL: http://alt-ergo.ocamlpro.com/ -Source0: http://alt-ergo.ocamlpro.com/http/%{name}-%{version}/%{name}-%{version}.tar.gz +URL: https://alt-ergo.ocamlpro.com/ +Source0: https://alt-ergo.ocamlpro.com/http/%{name}-%{version}/%{name}-%{version}.tar.gz # Created with gimp from official upstream icon Source1: %{name}-icons.tar.xz Source2: %{name}.desktop Source3: %{name}.appdata.xml # Use the asmrun_pic variant when linking the binary. -Patch0: %{name}-1.30-use-pic.patch - -# Process embedded newlines in echo commands -Patch1: %{name}-2.0.0-newline.patch +Patch0: %{name}-1.30-use-pic.patch BuildRequires: desktop-file-utils BuildRequires: gtksourceview2-devel @@ -33,54 +30,69 @@ BuildRequires: ocaml-lablgtk-devel BuildRequires: ocaml-menhir-devel BuildRequires: ocaml-num-devel BuildRequires: ocaml-ocplib-simplex-devel +BuildRequires: ocaml-psmt2-frontend-devel BuildRequires: ocaml-zarith-devel BuildRequires: ocaml-zip-devel -# Do not Require private ocaml interfaces that we don't Provide -%global __requires_exclude ocamlx?\\\((Ccx|Com(bine|mands)|Ex(ception|planation)|F(ormula|un_sat)|H(consing|string)|In(equalities|stances)|L(iteral|oc)|Matching_types|Numbers(Interface)?|Options|P(arsed|olynome|rofiling)|S(at_solver(_sig)?|ig|ymbols)|T(erm|heory|imers|y(ped)?)|U(f|se|til))\\\) +Requires: ocaml-alt-ergo%{?_isa} = %{version}-%{release} -%description +# Do not Require private ocaml interfaces that we don't Provide +%global __requires_exclude ocamlx?\\\((Commands|Ex(ception|planation)|Formula|Hstring|Inequalities|L(iteral|oc)|Matching_types|Numbers(Interface)?|Options|P(arsed|olynome)|S(atml_types|ig|ymbols)|T(erm|y(ped)?)|U(f|til)|Vec)\\\) + +%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. +instantiation mechanism by which it fully supports quantifiers.} + +%description %_desc %package gui -Summary: Graphical front end for alt-ergo +Summary: Graphical front end for Alt-Ergo Requires: %{name}%{?_isa} = %{version}-%{release} Requires: gtksourceview2 Requires: hicolor-icon-theme -%description gui -A graphical front end for the alt-ergo theorem prover. +%description gui %_desc + +This package contains a graphical front end for the Alt-Ergo theorem +prover. + +%package -n ocaml-alt-ergo +Summary: Automated theorem prover library + +%description -n ocaml-alt-ergo %_desc + +This package is the core of Alt-Ergo as an OCaml library. + +%package -n ocaml-alt-ergo-devel +Summary: Development files for ocaml-altergolib +Requires: ocaml-alt-ergo%{?_isa} = %{version}-%{release} + +%description -n ocaml-alt-ergo-devel %_desc + +This package contains development files needed to build applications +that use the Alt-Ergo library. %prep -%setup -q +%autosetup -p1 %setup -q -T -D -a 1 -%patch0 -p1 -%patch1 -p1 - cp -p %{SOURCE2} . -# Use Fedora LDFLAGS -for arg in $RPM_LD_FLAGS; do - sed -i "s|^OFLAGS =.*-g|& -ccopt $arg|" Makefile.users -done - # Look for zip instead of camlzip sed -i 's/camlzip/zip/g' configure opam %ifarch %{arm} # Work around for https://github.com/ocaml/ocaml/issues/7608 # Remove this once a released ocaml version fixes that issue. -sed -i "s|^OFLAGS =|& -fno-thumb|" Makefile.users +sed -i "s|^LIGHT_OFLAGS =|& -fno-thumb|" Makefile.users %endif %build -%configure +%configure --libdir=%{_libdir}/ocaml %ifnarch %{ocaml_native_compiler} %global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLLEX=ocamllex @@ -134,7 +146,6 @@ done %license COPYING.md LICENSE.md %{_bindir}/%{name} %{_mandir}/man1/alt-ergo.1.* -%{_libdir}/%{name}/ %files gui %{_bindir}/altgr-ergo @@ -143,7 +154,32 @@ done %{_datadir}/gtksourceview-2.0/language-specs/%{name}.lang %{_datadir}/icons/hicolor/*/apps/%{name}.png +%files -n ocaml-alt-ergo +%dir %{_libdir}/ocaml/%{name}/ +%{_libdir}/ocaml/%{name}/plugins/ +%{_libdir}/ocaml/%{name}/preludes/ +%{_libdir}/ocaml/%{name}/altErgoLib.cma +%{_libdir}/ocaml/%{name}/altErgoLib.cmi +%ifarch %{ocaml_native_compiler} +%{_libdir}/ocaml/%{name}/altErgoLib.cmxs +%endif + +%files -n ocaml-%{name}-devel +%{_libdir}/ocaml/%{name}/META +%ifarch %{ocaml_native_compiler} +%{_libdir}/ocaml/%{name}/altErgoLib.a +%{_libdir}/ocaml/%{name}/altErgoLib.cmx +%{_libdir}/ocaml/%{name}/altErgoLib.cmxa +%endif +%{_libdir}/ocaml/%{name}/altErgoLib.o +%{_libdir}/ocaml/%{name}/altErgoLib.cmo +%{_libdir}/ocaml/%{name}/altErgoLib.cmt + %changelog +* Fri Jun 19 2020 Jerry James - 2.2.0-1 +- Version 2.2.0 +- Drop upstreamed -newline patch + * Tue May 05 2020 Richard W.M. Jones - 2.0.0-15 - OCaml 4.11.0+dev2-2020-04-22 rebuild diff --git a/sources b/sources index 7b8dc34..8679a4d 100644 --- a/sources +++ b/sources @@ -1,2 +1,2 @@ -SHA512 (alt-ergo-2.0.0.tar.gz) = aaf8d948a8bd77cd1ff0d8fffcaf0dd30a906a90769c4c463705c212c4b12e1bd124024b50cd244334c96088b367a8a41ae2a16876732f116c9bd418be4ec341 +SHA512 (alt-ergo-2.2.0.tar.gz) = 08ac8250ef2b853edc4885038ffbc8a5b4bbbedd170812fda3a4c4e59609f9642ae995d3a75ed637fbabb1163c6e84afa61c41204d41ba4b1377b3b84cc01eb8 SHA512 (alt-ergo-icons.tar.xz) = cb2e93bab3359f6f198e80e3e68840ed4b25a213b61f388a2de8abc299fd3c89240f64f610290ac89e6005088c484b2718a68ec18063076f73d7871a38ee038f From 08fa9904e77e0bb70f765a63997f58abd117195b Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 21 Jul 2020 20:36:44 -0600 Subject: [PATCH 19/77] Replace obsolete ocaml-menhir-devel BR with ocaml-menhir. --- alt-ergo.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index 98b16ed..cb428aa 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -27,7 +27,7 @@ BuildRequires: gtksourceview2-devel BuildRequires: ocaml BuildRequires: ocaml-findlib BuildRequires: ocaml-lablgtk-devel -BuildRequires: ocaml-menhir-devel +BuildRequires: ocaml-menhir BuildRequires: ocaml-num-devel BuildRequires: ocaml-ocplib-simplex-devel BuildRequires: ocaml-psmt2-frontend-devel From 43e929537f651a145ef21e68f1e44edbd15a5bf9 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Mon, 27 Jul 2020 11:58:12 +0000 Subject: [PATCH 20/77] - Rebuilt for https://fedoraproject.org/wiki/Fedora_33_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 cb428aa..3ed9f07 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.2.0 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -176,6 +176,9 @@ done %{_libdir}/ocaml/%{name}/altErgoLib.cmt %changelog +* Mon Jul 27 2020 Fedora Release Engineering - 2.2.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild + * Fri Jun 19 2020 Jerry James - 2.2.0-1 - Version 2.2.0 - Drop upstreamed -newline patch From 4b9dbb22feba94d5e6c1623e07c8e1f52912dd02 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Fri, 21 Aug 2020 19:58:39 +0100 Subject: [PATCH 21/77] OCaml 4.11.0 rebuild --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index 3ed9f07..1cecddd 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.2.0 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -176,6 +176,9 @@ done %{_libdir}/ocaml/%{name}/altErgoLib.cmt %changelog +* Fri Aug 21 2020 Richard W.M. Jones - 2.2.0-3 +- OCaml 4.11.0 rebuild + * Mon Jul 27 2020 Fedora Release Engineering - 2.2.0-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild From 2a865ec4382b6a83289c4118537428dec2f1ad42 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 2 Sep 2020 00:13:21 +0100 Subject: [PATCH 22/77] OCaml 4.11.1 rebuild --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index 1cecddd..cbe870d 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.2.0 -Release: 3%{?dist} +Release: 4%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -176,6 +176,9 @@ done %{_libdir}/ocaml/%{name}/altErgoLib.cmt %changelog +* Tue Sep 01 2020 Richard W.M. Jones - 2.2.0-4 +- OCaml 4.11.1 rebuild + * Fri Aug 21 2020 Richard W.M. Jones - 2.2.0-3 - OCaml 4.11.0 rebuild From bd924aba140d6926181528fd1e10ebcb4636ea8a Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 25 Sep 2020 12:22:22 -0600 Subject: [PATCH 23/77] Rebuild for ocaml-zarith 1.10. --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index cbe870d..75167f2 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.2.0 -Release: 4%{?dist} +Release: 5%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -176,6 +176,9 @@ done %{_libdir}/ocaml/%{name}/altErgoLib.cmt %changelog +* Fri Sep 25 2020 Jerry James - 2.2.0-5 +- Rebuild for ocaml-zarith 1.10 + * Tue Sep 01 2020 Richard W.M. Jones - 2.2.0-4 - OCaml 4.11.1 rebuild From 0b8900769504c2c15bf34d612e4ef29c7ad612ab Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 9 Nov 2020 10:48:15 -0700 Subject: [PATCH 24/77] Explicitly BR make. --- alt-ergo.spec | 1 + 1 file changed, 1 insertion(+) diff --git a/alt-ergo.spec b/alt-ergo.spec index 75167f2..d4b22af 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -24,6 +24,7 @@ Patch0: %{name}-1.30-use-pic.patch BuildRequires: desktop-file-utils BuildRequires: gtksourceview2-devel +BuildRequires: make BuildRequires: ocaml BuildRequires: ocaml-findlib BuildRequires: ocaml-lablgtk-devel From 1599ff6b11fc506608a3cd2ccc6d42276e1b48af Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 16 Nov 2020 17:51:27 -0700 Subject: [PATCH 25/77] Rebuild for ocaml-zarith 1.11. --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index d4b22af..c965da6 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.2.0 -Release: 5%{?dist} +Release: 6%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -177,6 +177,9 @@ done %{_libdir}/ocaml/%{name}/altErgoLib.cmt %changelog +* Mon Nov 16 2020 Jerry James - 2.2.0-6 +- Rebuild for ocaml-zarith 1.11 + * Fri Sep 25 2020 Jerry James - 2.2.0-5 - Rebuild for ocaml-zarith 1.10 From c78b6cc3b9c43bfba5e6594ca53ce3fdf0245539 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Tue, 26 Jan 2021 00:01:26 +0000 Subject: [PATCH 26/77] - Rebuilt for https://fedoraproject.org/wiki/Fedora_34_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 c965da6..93fb250 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.2.0 -Release: 6%{?dist} +Release: 7%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -177,6 +177,9 @@ done %{_libdir}/ocaml/%{name}/altErgoLib.cmt %changelog +* Tue Jan 26 2021 Fedora Release Engineering - 2.2.0-7 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild + * Mon Nov 16 2020 Jerry James - 2.2.0-6 - Rebuild for ocaml-zarith 1.11 From eae4588b66681be25c7686962bb80425d3f171d0 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 4 Feb 2021 09:01:16 -0700 Subject: [PATCH 27/77] Updates to the desktop and metainfo files. Add -pervasives patch. --- alt-ergo-pervasives.patch | 566 ++++++++++++++++++ alt-ergo.appdata.xml => alt-ergo.metainfo.xml | 14 +- alt-ergo.spec | 33 +- 3 files changed, 597 insertions(+), 16 deletions(-) create mode 100644 alt-ergo-pervasives.patch rename alt-ergo.appdata.xml => alt-ergo.metainfo.xml (69%) diff --git a/alt-ergo-pervasives.patch b/alt-ergo-pervasives.patch new file mode 100644 index 0000000..b782e21 --- /dev/null +++ b/alt-ergo-pervasives.patch @@ -0,0 +1,566 @@ +--- alt-ergo-2.2.0/lib/frontend/parsers.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/frontend/parsers.ml 2021-01-29 16:42:13.025134465 -0700 +@@ -100,7 +100,7 @@ let parse_input_file file = + stdin, Lexing.from_string file_content, false, ext + else + let ext = Filename.extension file in +- if Pervasives.(<>) file "" then ++ if Stdlib.(<>) file "" then + let cin = open_in file in + cin, Lexing.from_channel cin, true, ext + else +--- alt-ergo-2.2.0/lib/frontend/triggers.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/frontend/triggers.ml 2021-01-29 16:15:57.819513468 -0700 +@@ -33,7 +33,7 @@ module Sy = Symbols + type polarity = Pos | Neg + + module Vterm = Sy.Set +-module Vtype = Set.Make(struct type t=int let compare=Pervasives.compare end) ++module Vtype = Set.Make(struct type t=int let compare=Stdlib.compare end) + + module STRS = Set.Make( + struct +@@ -50,12 +50,12 @@ module STRS = Set.Make( + let c=compare_term a1 a2 in if c=0 then compare_term b1 b2 else c + else c + | TTconst (Treal r1) , TTconst (Treal r2) -> Num.compare_num r1 r2 +- | x , y -> Pervasives.compare x y ++ | x , y -> Stdlib.compare x y + and compare_list l1 l2 = match l1,l2 with + [] , _ -> -1 + | _ , [] -> 1 + | x::l1 , y::l2 -> +- let c = Pervasives.compare x y in if c=0 then compare_list l1 l2 else c ++ let c = Stdlib.compare x y in if c=0 then compare_list l1 l2 else c + + let compare (t1,_,_) (t2,_,_) = compare_term t1 t2 + end) +@@ -75,7 +75,7 @@ let compare_tconstant c1 c2 = + | Tbitv s1, Tbitv s2 -> String.compare s1 s2 + | Tbitv s1, _ -> 1 + | _, Tbitv s2 -> -1 +- | _ -> Pervasives.compare c1 c2 ++ | _ -> Stdlib.compare c1 c2 + + let rec depth_tterm t = + match t.c.tt_desc with +@@ -153,7 +153,7 @@ let rec compare_tterm t1 t2 = + + | TTinInterval (e1, a1, b1, c1, d1), TTinInterval (e2, a2, b2, c2, d2) -> + let c = compare_tterm e1 e2 in +- if c <> 0 then c else Pervasives.compare (a1, b1, c1, d1) (a2, b2, c2, d2) ++ if c <> 0 then c else Stdlib.compare (a1, b1, c1, d1) (a2, b2, c2, d2) + + | TTinInterval _, _ -> -1 + | _, TTinInterval _ -> 1 +@@ -191,7 +191,7 @@ let rec compare_tterm t1 t2 = + | TTconcat _, _ -> -1 + | _, TTconcat _ -> 1 + | TTdot(t1, a1), TTdot(t2,a2) -> +- let c = Pervasives.compare a1 a2 in ++ let c = Stdlib.compare a1 a2 in + if c<>0 then c else + compare_tterm t1 t2 + | TTdot _, _ -> -1 +--- alt-ergo-2.2.0/lib/frontend/typechecker.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/frontend/typechecker.ml 2021-01-29 16:43:14.235096310 -0700 +@@ -36,7 +36,7 @@ module S = Set.Make(String) + module Sy = Symbols.Set + + module MString = +- Map.Make(struct type t = string let compare = Pervasives.compare end) ++ Map.Make(struct type t = string let compare = Stdlib.compare end) + + module Types = struct + +@@ -78,7 +78,7 @@ module Types = struct + List.for_all2 + (fun pp x -> + match pp with +- | PPTvarid (y, _) -> Pervasives.(=) x y ++ | PPTvarid (y, _) -> Stdlib.(=) x y + | _ -> false + ) lpp lvars + with Invalid_argument _ -> false +@@ -97,7 +97,7 @@ module Types = struct + to_tyvars := MString.add s nty !to_tyvars; + nty + end +- | PPTexternal (l, s, loc) when Pervasives.(=) s "farray" -> ++ | PPTexternal (l, s, loc) when Stdlib.(=) s "farray" -> + let t1,t2 = match l with + | [t2] -> PPTint,t2 + | [t1;t2] -> t1,t2 +@@ -108,7 +108,7 @@ module Types = struct + | PPTexternal (l, s, loc) -> + begin + match rectype with +- | Some (id, vars, ty) when Pervasives.(=) s id && ++ | Some (id, vars, ty) when Stdlib.(=) s id && + equal_pp_vars l vars -> ty + | _ -> + try +@@ -769,7 +769,7 @@ and type_form ?(in_theory=false) env f = + try + List.iter2 Ty.unify lt lt_args; + let r = +- if Pervasives.(=) p "<=" || Pervasives.(=) p "<" then ++ if Stdlib.(=) p "<=" || Stdlib.(=) p "<" then + TFatom { c = TAbuilt(Hstring.make p,te_args); + annot=new_id ()} + else +@@ -1871,10 +1871,10 @@ let file ld = + exit 1 + + let is_local_hyp s = +- try Pervasives.(=) (String.sub s 0 2) "@L" with Invalid_argument _ -> false ++ try Stdlib.(=) (String.sub s 0 2) "@L" with Invalid_argument _ -> false + + let is_global_hyp s = +- try Pervasives.(=) (String.sub s 0 2) "@H" with Invalid_argument _ -> false ++ try Stdlib.(=) (String.sub s 0 2) "@H" with Invalid_argument _ -> false + + let split_goals_aux f l = + let _, _, _, ret = +--- alt-ergo-2.2.0/lib/reasoners/fun_sat.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/reasoners/fun_sat.ml 2021-01-29 16:44:04.915064713 -0700 +@@ -69,7 +69,7 @@ module Make (Th : Theory.S) : Sat_solver + SF.fold + (fun f mp -> + let w = var_inc +. try MF.find f mp with Not_found -> 0. in +- stable := !stable && Pervasives.(<=) w 1e100; ++ stable := !stable && Stdlib.(<=) w 1e100; + MF.add f w mp + )(Ex.bj_formulas_of expl) mp + in +@@ -95,9 +95,9 @@ module Make (Th : Theory.S) : Sat_solver + let dec = + List.fast_sort + (fun (_, x1, b1) (_, x2, b2) -> +- let c = Pervasives.compare b2 b1 in ++ let c = Stdlib.compare b2 b1 in + if c <> 0 then c +- else Pervasives.compare x2 x1 ++ else Stdlib.compare x2 x1 + )dec + in + (* +@@ -967,7 +967,7 @@ module Make (Th : Theory.S) : Sat_solver + let i = abs (interpretation ()) in + assert (i = 1 || i = 2 || i = 3); + if not !(env.model_gen_mode) && +- Pervasives.(<>) (Options.interpretation_timelimit ()) 0. then ++ Stdlib.(<>) (Options.interpretation_timelimit ()) 0. then + begin + Options.Time.unset_timeout ~is_gui:(Options.get_is_gui()); + Options.Time.set_timeout +--- alt-ergo-2.2.0/lib/reasoners/ite.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/reasoners/ite.ml 2021-01-29 15:13:41.631062282 -0700 +@@ -72,7 +72,7 @@ module Relation (X : ALIEN) (Uf : Uf.S) + type t = T.t * bool + let compare (a1, b1) (a2, b2) = + let c = T.compare a1 a2 in +- if c <> 0 then c else Pervasives.compare b1 b2 ++ if c <> 0 then c else Stdlib.compare b1 b2 + end) + + type t = +--- alt-ergo-2.2.0/lib/reasoners/satml_frontend.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/reasoners/satml_frontend.ml 2021-01-29 16:16:47.003462456 -0700 +@@ -533,7 +533,7 @@ module Make (Th : Theory.S) : Sat_solver + if res <> 0 then res + else + (* higher weight is better hence compare w2 w1 *) +- let res = Pervasives.compare w2 w1 in ++ let res = Stdlib.compare w2 w1 in + if res <> 0 then res + else + (* lower index is better *) +@@ -922,7 +922,7 @@ module Make (Th : Theory.S) : Sat_solver + + (* copied from sat_solvers.ml *) + let max_term_depth_in_sat env = +- let aux mx f = Pervasives.max mx (F.max_term_depth f) in ++ let aux mx f = Stdlib.max mx (F.max_term_depth f) in + let max_t = MF.fold (fun f _ mx -> aux mx f) env.gamma 0 in + A.Map.fold (fun _ {F.f} mx -> aux mx f) env.ground_preds max_t + +--- alt-ergo-2.2.0/lib/reasoners/satml.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/reasoners/satml.ml 2021-01-29 16:44:54.595033743 -0700 +@@ -351,7 +351,7 @@ module Make (Th : Theory.S) : SAT_ML wit + *) + + let f_weight env i j = +- Pervasives.(<) (Vec.get env.vars j).weight (Vec.get env.vars i).weight ++ Stdlib.(<) (Vec.get env.vars j).weight (Vec.get env.vars i).weight + + let f_filter env i = (Vec.get env.vars i).level < 0 + +@@ -365,7 +365,7 @@ module Make (Th : Theory.S) : SAT_ML wit + + let var_bump_activity env v = + v.weight <- v.weight +. env.var_inc; +- if Pervasives.(>) v.weight 1e100 then begin ++ if Stdlib.(>) v.weight 1e100 then begin + for i = 0 to env.vars.Vec.sz - 1 do + (Vec.get env.vars i).weight <- (Vec.get env.vars i).weight *. 1e-100 + done; +@@ -377,7 +377,7 @@ module Make (Th : Theory.S) : SAT_ML wit + + let clause_bump_activity env c = + c.activity <- c.activity +. env.clause_inc; +- if Pervasives.(>) c.activity 1e20 then begin ++ if Stdlib.(>) c.activity 1e20 then begin + for i = 0 to env.learnts.Vec.sz - 1 do + (Vec.get env.learnts i).activity <- + (Vec.get env.learnts i).activity *. 1e-20; +@@ -861,7 +861,7 @@ let compute_facts_for_theory_propagate e + let f_sort_db c1 c2 = + let sz1 = Vec.size c1.atoms in + let sz2 = Vec.size c2.atoms in +- let c = Pervasives.compare c1.activity c2.activity in ++ let c = Stdlib.compare c1.activity c2.activity in + if sz1 = sz2 && c = 0 then 0 + else + if sz1 > 2 && (sz2 = 2 || c < 0) then -1 +--- alt-ergo-2.2.0/lib/structures/formula.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/structures/formula.ml 2021-01-29 16:34:03.946514585 -0700 +@@ -108,8 +108,8 @@ type gformula = { + let size (t,_) = t.size + + let compare ((v1,_) as f1) ((v2,_) as f2) = +- let c = Pervasives.compare (size f1) (size f2) in +- if c=0 then Pervasives.compare v1.tag v2.tag else c ++ let c = Stdlib.compare (size f1) (size f2) in ++ if c=0 then Stdlib.compare v1.tag v2.tag else c + + let equal (f1,_) (f2,_) = + assert ((f1 == f2) == (f1.tag == f2.tag)); +@@ -866,7 +866,7 @@ let label f = + | _ -> Hstring.empty + + let label_model h = +- try Pervasives.(=) (String.sub (Hstring.view h) 0 6) "model:" ++ try Stdlib.(=) (String.sub (Hstring.view h) 0 6) "model:" + with Invalid_argument _ -> false + + let is_in_model f = +--- alt-ergo-2.2.0/lib/structures/literal.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/structures/literal.ml 2021-01-29 15:11:35.935224734 -0700 +@@ -95,7 +95,7 @@ module Make (X : OrderedType) : S with t + + type t = { at : atom; neg : bool; tpos : int; tneg : int } + +- let compare a1 a2 = Pervasives.compare a1.tpos a2.tpos ++ let compare a1 a2 = Stdlib.compare a1.tpos a2.tpos + let equal a1 a2 = a1.tpos = a2.tpos (* XXX == *) + let hash a1 = a1.tpos + let uid a1 = a1.tpos +--- alt-ergo-2.2.0/lib/structures/profiling.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/structures/profiling.ml 2021-01-29 16:41:48.035150044 -0700 +@@ -86,7 +86,7 @@ let state = + let set_sigprof () = + let tm = + let v = Options.profiling_period () in +- if Pervasives.(>) v 0. then v else -. v ++ if Stdlib.(>) v 0. then v else -. v + in + ignore + (Unix.setitimer Unix.ITIMER_PROF +@@ -626,9 +626,9 @@ let switch () = + + + let float_print fmt v = +- if Pervasives.(=) v 0. then fprintf fmt "-- " +- else if Pervasives.(<) v 10. then fprintf fmt "%0.5f" v +- else if Pervasives.(<) v 100. then fprintf fmt "%0.4f" v ++ if Stdlib.(=) v 0. then fprintf fmt "-- " ++ else if Stdlib.(<) v 10. then fprintf fmt "%0.5f" v ++ else if Stdlib.(<) v 100. then fprintf fmt "%0.4f" v + else fprintf fmt "%0.3f" v + + let line_of_module arr f = +--- alt-ergo-2.2.0/lib/structures/symbols.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/structures/symbols.ml 2021-01-29 15:10:23.775316438 -0700 +@@ -114,7 +114,7 @@ let compare s1 s2 = match s1, s2 with + | Op(Access s1), Op(Access s2) -> Hstring.compare s1 s2 + | Op(Access _), _ -> -1 + | _, Op(Access _) -> 1 +- | _ -> Pervasives.compare s1 s2 ++ | _ -> Stdlib.compare s1 s2 + + let equal s1 s2 = compare s1 s2 = 0 + +--- alt-ergo-2.2.0/lib/structures/term.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/structures/term.ml 2021-01-29 16:33:11.033560074 -0700 +@@ -270,7 +270,7 @@ let gen_sko ty = make (Sy.fresh "@sko") + + let is_skolem_cst v = + try +- Pervasives.(=) (String.sub (Sy.to_string v.f) 0 4) "_sko" ++ Stdlib.(=) (String.sub (Sy.to_string v.f) 0 4) "_sko" + with Invalid_argument _ -> false + + let find_skolem = +@@ -338,7 +338,7 @@ let label t = try Labels.find labels t w + + + let label_model h = +- try Pervasives.(=) (String.sub (Hstring.view h) 0 6) "model:" ++ try Stdlib.(=) (String.sub (Hstring.view h) 0 6) "model:" + with Invalid_argument _ -> false + + let rec is_in_model_rec depth { f = f; xs = xs } = +--- alt-ergo-2.2.0/lib/structures/ty.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/structures/ty.ml 2021-01-29 16:18:15.746370389 -0700 +@@ -202,7 +202,7 @@ let rec equal t1 t2 = + + let rec compare t1 t2 = + match shorten t1 , shorten t2 with +- | Tvar{v=v1} , Tvar{v=v2} -> Pervasives.compare v1 v2 ++ | Tvar{v=v1} , Tvar{v=v2} -> Stdlib.compare v1 v2 + | Tvar _, _ -> -1 | _ , Tvar _ -> 1 + | Text(l1, s1) , Text(l2, s2) -> + let c = Hstring.compare s1 s2 in +@@ -225,7 +225,7 @@ let rec compare t1 t2 = + let l1, l2 = List.map snd l1, List.map snd l2 in + compare_list l1 l2 + | Trecord _, _ -> -1 | _ , Trecord _ -> 1 +- | t1 , t2 -> Pervasives.compare t1 t2 ++ | t1 , t2 -> Stdlib.compare t1 t2 + and compare_list l1 l2 = match l1, l2 with + | [] , [] -> 0 + | [] , _ -> -1 +@@ -268,7 +268,7 @@ let rec unify t1 t2 = + + + (*** matching with a substitution mechanism ***) +-module M = Map.Make(struct type t=int let compare = Pervasives.compare end) ++module M = Map.Make(struct type t=int let compare = Stdlib.compare end) + type subst = t M.t + + let esubst = M.empty +@@ -340,9 +340,9 @@ let instantiate lvar lty ty = + let union_subst s1 s2 = + M.fold (fun k x s2 -> M.add k x s2) (M.map (apply_subst s2) s1) s2 + +-let compare_subst = M.compare Pervasives.compare ++let compare_subst = M.compare Stdlib.compare + +-let equal_subst = M.equal Pervasives.(=) ++let equal_subst = M.equal Stdlib.(=) + + let rec fresh ty subst = + match ty with +@@ -383,7 +383,7 @@ and fresh_list lty subst = + ty::lty, subst) lty ([], subst) + + module Svty = +- Set.Make(struct type t = int let compare = Pervasives.compare end) ++ Set.Make(struct type t = int let compare = Stdlib.compare end) + + module Set = + Set.Make(struct +--- alt-ergo-2.2.0/lib/util/myUnix.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/util/myUnix.ml 2021-01-29 16:45:33.010009798 -0700 +@@ -16,7 +16,7 @@ module Default_Unix = struct + let cur_time () = (times()).tms_utime + + let set_timeout ~is_gui timelimit = +- if Pervasives.(<>) timelimit 0. then ++ if Stdlib.(<>) timelimit 0. then + let itimer = + if is_gui then Unix.ITIMER_REAL (* troubles with VIRTUAL *) + else Unix.ITIMER_VIRTUAL +--- alt-ergo-2.2.0/lib/util/numbers.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/util/numbers.ml 2021-01-29 16:46:06.130989159 -0700 +@@ -48,8 +48,8 @@ module Q = struct + else + let v = to_float q in + let w = +- if Pervasives.(<) v min_float then min_float +- else if Pervasives.(>) v max_float then max_float ++ if Stdlib.(<) v min_float then min_float ++ else if Stdlib.(>) v max_float then max_float + else v + in + let flt = if n = 2 then sqrt w else w ** (1. /. float n) in +--- alt-ergo-2.2.0/lib/util/options.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/util/options.ml 2021-01-29 16:11:53.387767103 -0700 +@@ -902,8 +902,7 @@ let (>) (a: int) (b: int) = a > b + let (<=) (a: int) (b: int) = a <= b + let (>=) (a: int) (b: int) = a >= b + +-let compare (a: int) (b: int) = Pervasives.compare a b +- ++let compare (a: int) (b: int) = Stdlib.compare a b + + (* extra **) + +--- alt-ergo-2.2.0/lib/util/zarithNumbers.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/lib/util/zarithNumbers.ml 2021-01-29 16:08:45.571962041 -0700 +@@ -153,7 +153,7 @@ module Q : NumbersInterface.QSig with mo + let floor t = from_z (Z.fdiv (num t) (den t)) + let ceiling t = from_z (Z.cdiv (num t) (den t)) + let power t n = +- let abs_n = Pervasives.abs n in ++ let abs_n = Stdlib.abs n in + let num_pow = Z.power (num t) abs_n in + let den_pow = Z.power (den t) abs_n in + if n >= 0 then from_zz num_pow den_pow else from_zz den_pow num_pow +--- alt-ergo-2.2.0/tools/gui/annoted_ast.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/tools/gui/annoted_ast.ml 2021-01-29 16:47:08.762950125 -0700 +@@ -188,7 +188,7 @@ type annoted_node = + module MDep = Map.Make ( + struct + type t = atyped_decl annoted +- let compare = Pervasives.compare ++ let compare = Stdlib.compare + end) + + +@@ -862,9 +862,9 @@ let find_dep_by_string dep s = + | None -> begin + match d.c with + | ALogic (_, ls, ty) when List.mem s ls -> Some d +- | ATypeDecl (_, _, s', _) when Pervasives.(=) s s'-> Some d +- | APredicate_def (_, p, _, _) when Pervasives.(=) s p -> Some d +- | AFunction_def (_, f, _, _, _) when Pervasives.(=) s f -> Some d ++ | ATypeDecl (_, _, s', _) when Stdlib.(=) s s'-> Some d ++ | APredicate_def (_, p, _, _) when Stdlib.(=) s p -> Some d ++ | AFunction_def (_, f, _, _, _) when Stdlib.(=) s f -> Some d + | _ -> None + end + ) dep None +@@ -874,7 +874,7 @@ let find_tag_deps dep tag = + (fun d (deps,_) found -> + match found with + | Some _ -> found +- | None -> if Pervasives.(=) d.tag tag then Some deps else None ++ | None -> if Stdlib.(=) d.tag tag then Some deps else None + ) dep None + + let find_tag_inversedeps dep tag = +@@ -882,7 +882,7 @@ let find_tag_inversedeps dep tag = + (fun d (_,deps) found -> + match found with + | Some _ -> found +- | None -> if Pervasives.(=) d.tag tag then Some deps else None ++ | None -> if Stdlib.(=) d.tag tag then Some deps else None + ) dep None + + let make_dep_string d ex dep s = +@@ -1965,7 +1965,7 @@ and findtags_aform sl aform acc = + (fun sl (sy, _) -> + let s = Symbols.to_string_clean sy in + List.fold_left +- (fun l s' -> if Pervasives.(=) s' s then l else s'::l) [] sl ++ (fun l s' -> if Stdlib.(=) s' s then l else s'::l) [] sl + )sl l + in + findtags_aform sl aaf.c acc +--- alt-ergo-2.2.0/tools/gui/connected_ast.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/tools/gui/connected_ast.ml 2021-01-29 16:47:43.226928651 -0700 +@@ -386,7 +386,7 @@ let rec unquantify_aform (buffer:sbuffer + List.fold_left (fun (nbv, used, goal_used, ve, uplet, lets) v -> + let ((s, _) as v'), e = List.hd ve in + let cdr_ve = List.tl ve in +- assert (Pervasives.(=) v v'); ++ assert (Stdlib.(=) v v'); + if String.length e == 0 then + (v'::nbv, used, goal_used, cdr_ve, v'::uplet, lets) + else +@@ -541,7 +541,7 @@ let rec add_instance_aux ?(register=true + make_instance env.inst_buffer vars entries af goal_form tyenv in + let ln_form = least_nested_form used_vars goal_form in + env.inst_buffer#place_cursor ~where:env.inst_buffer#end_iter; +- if Pervasives.(=) ln_form (Exists goal_form) then begin ++ if Stdlib.(=) ln_form (Exists goal_form) then begin + let hy = + AAxiom (loc, (sprintf "%s%s" "_instance_" aname), ax_kd, instance.c) in + let ahy = new_annot env.inst_buffer hy instance.id ptag in +@@ -735,7 +735,7 @@ and add_trigger ?(register=true) t qid e + if register then + save env.actions + (AddTrigger (qf.id, +- Pervasives.(=) sbuf env.inst_buffer, str)); ++ Stdlib.(=) sbuf env.inst_buffer, str)); + commit_tags_buffer sbuf + | _ -> assert false + end +--- alt-ergo-2.2.0/tools/gui/main_gui.ml.orig 2018-04-21 11:02:10.000000000 -0600 ++++ alt-ergo-2.2.0/tools/gui/main_gui.ml 2021-01-29 16:49:56.218845792 -0700 +@@ -148,7 +148,7 @@ let save_session envs = + + let save_dialog cancel envs () = + if List.exists +- (fun env -> Pervasives.(<>) env.actions env.saved_actions) envs then ++ (fun env -> Stdlib.(<>) env.actions env.saved_actions) envs then + if List.exists + (fun env -> not (Gui_session.safe_session env.actions)) envs then + GToolbox.message_box +@@ -247,7 +247,7 @@ let pop_model sat_env () = + let compare_rows icol_number (model:#GTree.model) row1 row2 = + let t1 = model#get ~row:row1 ~column:icol_number in + let t2 = model#get ~row:row2 ~column:icol_number in +- Pervasives.compare t1 t2 ++ Stdlib.compare t1 t2 + + + let empty_inst_model () = +@@ -382,7 +382,7 @@ let refresh_timers t () = + let total = + tsat +. tmatch +. tcc +. tarith +. tarrays +. tsum +. trecords +. tac in + +- let total = if Pervasives.(=) total 0. then 1. else total in ++ let total = if Stdlib.(=) total 0. then 1. else total in + + t.tl_sat#set_text (sprintf "%3.2f s" tsat); + t.tl_match#set_text (sprintf "%3.2f s" tmatch); +@@ -455,7 +455,7 @@ let add_inst ({h=h} as inst_model) orig + let id = Formula.id orig in + let name = + match Formula.view orig with +- | Formula.Lemma {Formula.name=n} when Pervasives.(<>) n "" -> n ++ | Formula.Lemma {Formula.name=n} when Stdlib.(<>) n "" -> n + | _ -> string_of_int id + in + let r, n, limit, to_add = +@@ -604,7 +604,7 @@ let vt_signal = + + let force_interrupt old_action_ref n = + (* This function is called just before the thread's timeslice ends *) +- if Pervasives.(=) (Some (Thread.id(Thread.self()))) !interrupt then ++ if Stdlib.(=) (Some (Thread.id(Thread.self()))) !interrupt then + raise Abort_thread; + match !old_action_ref with + | Sys.Signal_handle f -> f n +@@ -718,8 +718,8 @@ let remove_context env () = + toggle_prune env td + | AAxiom (_, s, _, _) + when String.length s = 0 || +- (Pervasives.(<>) s.[0] '_' && +- Pervasives.(<>) s.[0] '@') -> ++ (Stdlib.(<>) s.[0] '_' && ++ Stdlib.(<>) s.[0] '@') -> + toggle_prune env td + | _ -> () + ) env.ast +@@ -945,7 +945,7 @@ let search_all entry (sv:GSourceView2.so + buf#remove_tag found_all_tag ~start:buf#start_iter ~stop:buf#end_iter; + let str = entry#text in + let iter = ref buf#start_iter in +- if Pervasives.(<>) str "" then ++ if Stdlib.(<>) str "" then + let result = ref None in + search_one buf str result iter found_all_tag; + while !result != None do +@@ -1286,7 +1286,7 @@ let start_gui () = + + let set_wrap_lines _ = + List.iter (fun env -> +- if Pervasives.(=) env.goal_view#wrap_mode `NONE then ( ++ if Stdlib.(=) env.goal_view#wrap_mode `NONE then ( + env.goal_view#set_wrap_mode `CHAR; + env.inst_view#set_wrap_mode `CHAR; + Gui_config.update_wrap true diff --git a/alt-ergo.appdata.xml b/alt-ergo.metainfo.xml similarity index 69% rename from alt-ergo.appdata.xml rename to alt-ergo.metainfo.xml index 145c9a1..cdb417e 100644 --- a/alt-ergo.appdata.xml +++ b/alt-ergo.metainfo.xml @@ -1,6 +1,6 @@ - - alt-ergo.desktop + + com.ocamlpro.alt-ergo CC0-1.0 CECILL-C Alt-Ergo @@ -17,13 +17,19 @@ by which it fully supports quantifiers.

+ com.ocamlpro.alt-ergo.desktop http://jjames.fedorapeople.org/alt-ergo/altgr-ergo-screenshot.png Basic Alt-Ergo usage - loganjerry@gmail.com - http://alt-ergo.ocamlpro.com/ + loganjerry@gmail.com + 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 93fb250..c5ff404 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.2.0 -Release: 7%{?dist} +Release: 8%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -17,13 +17,16 @@ Source0: https://alt-ergo.ocamlpro.com/http/%{name}-%{version}/%{name}-%{version # Created with gimp from official upstream icon Source1: %{name}-icons.tar.xz Source2: %{name}.desktop -Source3: %{name}.appdata.xml +Source3: %{name}.metainfo.xml # Use the asmrun_pic variant when linking the binary. Patch0: %{name}-1.30-use-pic.patch +# Do not use the deprecated Pervasives interface +Patch1: %{name}-pervasives.patch BuildRequires: desktop-file-utils BuildRequires: gtksourceview2-devel +BuildRequires: libappstream-glib BuildRequires: make BuildRequires: ocaml BuildRequires: ocaml-findlib @@ -78,10 +81,9 @@ This package contains development files needed to build applications that use the Alt-Ergo library. %prep -%autosetup -p1 -%setup -q -T -D -a 1 +%autosetup -p1 -a 1 -cp -p %{SOURCE2} . +cp -p %{SOURCE2} com.ocamlpro.%{name}.desktop # Look for zip instead of camlzip sed -i 's/camlzip/zip/g' configure opam @@ -102,11 +104,10 @@ sed -i "s|^LIGHT_OFLAGS =|& -fno-thumb|" Makefile.users %endif make %{opt_option} -make %{opt_option} gui %install mkdir -p %{buildroot}%{_bindir} -make %{opt_option} DESTDIR=%{buildroot} install install-gui +make %{opt_option} DESTDIR=%{buildroot} install # Move the gtksourceview file to the right place mv %{buildroot}%{_datadir}/%{name}/gtksourceview-2.0 %{buildroot}%{_datadir} @@ -114,11 +115,15 @@ rmdir %{buildroot}%{_datadir}/%{name} # Install the desktop file mkdir -p %{buildroot}%{_datadir}/applications -desktop-file-install --dir %{buildroot}%{_datadir}/applications %{name}.desktop +desktop-file-install --dir %{buildroot}%{_datadir}/applications \ + com.ocamlpro.%{name}.desktop # Install the AppData file -mkdir -p %{buildroot}%{_datadir}/appdata -install -pm 644 %{SOURCE3} %{buildroot}%{_datadir}/appdata +mkdir -p %{buildroot}%{_metainfodir} +install -pm 644 %{SOURCE3} \ + %{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml +appstream-util validate-relax --nonet \ + %{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml # Install the icons mkdir -p %{buildroot}%{_datadir}/icons @@ -150,10 +155,10 @@ done %files gui %{_bindir}/altgr-ergo -%{_datadir}/appdata/%{name}.appdata.xml -%{_datadir}/applications/%{name}.desktop +%{_datadir}/applications/com.ocamlpro.%{name}.desktop %{_datadir}/gtksourceview-2.0/language-specs/%{name}.lang %{_datadir}/icons/hicolor/*/apps/%{name}.png +%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml %files -n ocaml-alt-ergo %dir %{_libdir}/ocaml/%{name}/ @@ -177,6 +182,10 @@ done %{_libdir}/ocaml/%{name}/altErgoLib.cmt %changelog +* Thu Feb 4 2021 Jerry James - 2.2.0-8 +- Updates to the desktop and metainfo files +- Add -pervasives patch + * Tue Jan 26 2021 Fedora Release Engineering - 2.2.0-7 - Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild From 3a917b3309e26ce4047ab1b540b53d0567ca32fc Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 2 Mar 2021 11:26:15 +0000 Subject: [PATCH 28/77] OCaml 4.12.0 build --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index c5ff404..0d261ed 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.2.0 -Release: 8%{?dist} +Release: 9%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -182,6 +182,9 @@ done %{_libdir}/ocaml/%{name}/altErgoLib.cmt %changelog +* Tue Mar 2 11:26:14 GMT 2021 Richard W.M. Jones - 2.2.0-9 +- OCaml 4.12.0 build + * Thu Feb 4 2021 Jerry James - 2.2.0-8 - Updates to the desktop and metainfo files - Add -pervasives patch From 335accbed6e4aa4db24e07e8ca1d95f23f0e8062 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 3 Mar 2021 12:07:12 -0700 Subject: [PATCH 29/77] Rebuild for ocaml-zarith 1.12. --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index 0d261ed..f1d22c9 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.2.0 -Release: 9%{?dist} +Release: 10%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -182,6 +182,9 @@ done %{_libdir}/ocaml/%{name}/altErgoLib.cmt %changelog +* Wed Mar 3 2021 Jerry James - 2.2.0-10 +- Rebuild for ocaml-zarith 1.12 + * Tue Mar 2 11:26:14 GMT 2021 Richard W.M. Jones - 2.2.0-9 - OCaml 4.12.0 build From a0af6956e8d953280625f8517b3cf8a628a1a4bc Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 24 Jun 2021 14:53:02 -0600 Subject: [PATCH 30/77] Rebuild for ocaml-lablgtk without gnomeui. --- alt-ergo.spec | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index f1d22c9..ca6cf7b 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.2.0 -Release: 10%{?dist} +Release: 11%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -24,9 +24,9 @@ Patch0: %{name}-1.30-use-pic.patch # Do not use the deprecated Pervasives interface Patch1: %{name}-pervasives.patch +BuildRequires: appstream BuildRequires: desktop-file-utils BuildRequires: gtksourceview2-devel -BuildRequires: libappstream-glib BuildRequires: make BuildRequires: ocaml BuildRequires: ocaml-findlib @@ -122,7 +122,7 @@ desktop-file-install --dir %{buildroot}%{_datadir}/applications \ mkdir -p %{buildroot}%{_metainfodir} install -pm 644 %{SOURCE3} \ %{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml -appstream-util validate-relax --nonet \ +appstreamcli validate --no-net \ %{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml # Install the icons @@ -182,6 +182,9 @@ done %{_libdir}/ocaml/%{name}/altErgoLib.cmt %changelog +* Tue Jun 22 2021 Jerry James - 2.2.0-11 +- Rebuild for ocaml-lablgtk without gnomeui + * Wed Mar 3 2021 Jerry James - 2.2.0-10 - Rebuild for ocaml-zarith 1.12 From 3480332c8e8a4bbc809373a7c7cdeb7e4a89d031 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 19 Jul 2021 13:19:50 -0600 Subject: [PATCH 31/77] Move META to the main package. --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index ca6cf7b..1b3abd2 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -162,6 +162,7 @@ done %files -n ocaml-alt-ergo %dir %{_libdir}/ocaml/%{name}/ +%{_libdir}/ocaml/%{name}/META %{_libdir}/ocaml/%{name}/plugins/ %{_libdir}/ocaml/%{name}/preludes/ %{_libdir}/ocaml/%{name}/altErgoLib.cma @@ -171,7 +172,6 @@ done %endif %files -n ocaml-%{name}-devel -%{_libdir}/ocaml/%{name}/META %ifarch %{ocaml_native_compiler} %{_libdir}/ocaml/%{name}/altErgoLib.a %{_libdir}/ocaml/%{name}/altErgoLib.cmx @@ -182,6 +182,9 @@ done %{_libdir}/ocaml/%{name}/altErgoLib.cmt %changelog +* Mon Jul 19 2021 Jerry James - 2.2.0-11 +- Move META to the main package + * Tue Jun 22 2021 Jerry James - 2.2.0-11 - Rebuild for ocaml-lablgtk without gnomeui From 154f03ab069c55237e63011a69914064eeb467be Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Wed, 21 Jul 2021 12:33:38 +0000 Subject: [PATCH 32/77] - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild Signed-off-by: Fedora Release Engineering From d4fa98b0182fc2c9fa0571120bdf7878977896e5 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Wed, 21 Jul 2021 17:29:03 +0000 Subject: [PATCH 33/77] - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_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 1b3abd2..6818f2c 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.2.0 -Release: 11%{?dist} +Release: 12%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -182,6 +182,9 @@ done %{_libdir}/ocaml/%{name}/altErgoLib.cmt %changelog +* Wed Jul 21 2021 Fedora Release Engineering - 2.2.0-12 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild + * Mon Jul 19 2021 Jerry James - 2.2.0-11 - Move META to the main package From 9a10ab3b2a47cf684f402c404e1adc7ee15b70d9 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 29 Jul 2021 12:57:23 -0600 Subject: [PATCH 34/77] Rebuild for changed ocamlx(Dynlink). --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index 6818f2c..9fedc78 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.2.0 -Release: 12%{?dist} +Release: 13%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -182,6 +182,9 @@ done %{_libdir}/ocaml/%{name}/altErgoLib.cmt %changelog +* Thu Jul 29 2021 Jerry James - 2.2.0-13 +- Rebuild for changed ocamlx(Dynlink) + * Wed Jul 21 2021 Fedora Release Engineering - 2.2.0-12 - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild From ed81837150d45206a2b06d7cf3e0077422c095c1 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 5 Oct 2021 12:54:42 +0100 Subject: [PATCH 35/77] OCaml 4.13.1 build --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index 9fedc78..81eca7a 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.2.0 -Release: 13%{?dist} +Release: 14%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -182,6 +182,9 @@ done %{_libdir}/ocaml/%{name}/altErgoLib.cmt %changelog +* Tue Oct 05 2021 Richard W.M. Jones - 2.2.0-14 +- OCaml 4.13.1 build + * Thu Jul 29 2021 Jerry James - 2.2.0-13 - Rebuild for changed ocamlx(Dynlink) From 4b29dc3ccc4cabd7aba6c4e8651049e6f616963b Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 30 Dec 2021 17:12:44 -0700 Subject: [PATCH 36/77] Version 2.3.0. New ocaml-alt-ergo-lib and ocaml-alt-ergo-parsers subpackages. --- README.md | 9 + alt-ergo-1.30-use-pic.patch | 19 - alt-ergo-pervasives.patch | 687 ++++++++++++++++++---------------- alt-ergo-psmt2-frontend.patch | 12 + alt-ergo.spec | 190 ++++++---- sources | 2 +- 6 files changed, 500 insertions(+), 419 deletions(-) create mode 100644 README.md delete mode 100644 alt-ergo-1.30-use-pic.patch create mode 100644 alt-ergo-psmt2-frontend.patch diff --git a/README.md b/README.md new file mode 100644 index 0000000..fa65fbb --- /dev/null +++ b/README.md @@ -0,0 +1,9 @@ +# alt-ergo + +[Alt-Ergo](https://alt-ergo.ocamlpro.com/) 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. diff --git a/alt-ergo-1.30-use-pic.patch b/alt-ergo-1.30-use-pic.patch deleted file mode 100644 index 71d6ad0..0000000 --- a/alt-ergo-1.30-use-pic.patch +++ /dev/null @@ -1,19 +0,0 @@ ---- alt-ergo-1.30.old/Makefile.users 2017-11-09 09:55:47.337871409 +0000 -+++ alt-ergo-1.30/Makefile.users 2017-11-09 10:00:52.374639872 +0000 -@@ -140,14 +140,14 @@ - $(OCAMLC) $(BFLAGS) -o $@ $(BIBBYTE) $^ - - $(NAME).opt: $(MAINCMX) -- $(OCAMLOPT) $(OFLAGS) -o $@ $(BIBOPT) $^ -+ $(OCAMLOPT) $(OFLAGS) -runtime-variant _pic -o $@ $(BIBOPT) $^ - - #### - $(GUINAME).byte: $(GUICMO) - $(OCAMLC) $(BFLAGS) -o $(GUINAME).byte $(BIBBYTE) $(BIBGUIBYTE) $^ - - $(GUINAME).opt: $(GUICMX) -- $(OCAMLOPT) $(OFLAGS) -o $(GUINAME).opt $(BIBOPT) $(BIBGUIOPT) $^ -+ $(OCAMLOPT) $(OFLAGS) -runtime-variant _pic -o $(GUINAME).opt $(BIBOPT) $(BIBGUIOPT) $^ - - ifeq ($(ENABLEGUI),yes) - gui: $(GUINAME).$(OCAMLBEST) diff --git a/alt-ergo-pervasives.patch b/alt-ergo-pervasives.patch index b782e21..23ad048 100644 --- a/alt-ergo-pervasives.patch +++ b/alt-ergo-pervasives.patch @@ -1,71 +1,7 @@ ---- alt-ergo-2.2.0/lib/frontend/parsers.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/frontend/parsers.ml 2021-01-29 16:42:13.025134465 -0700 -@@ -100,7 +100,7 @@ let parse_input_file file = - stdin, Lexing.from_string file_content, false, ext - else - let ext = Filename.extension file in -- if Pervasives.(<>) file "" then -+ if Stdlib.(<>) file "" then - let cin = open_in file in - cin, Lexing.from_channel cin, true, ext - else ---- alt-ergo-2.2.0/lib/frontend/triggers.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/frontend/triggers.ml 2021-01-29 16:15:57.819513468 -0700 -@@ -33,7 +33,7 @@ module Sy = Symbols - type polarity = Pos | Neg - - module Vterm = Sy.Set --module Vtype = Set.Make(struct type t=int let compare=Pervasives.compare end) -+module Vtype = Set.Make(struct type t=int let compare=Stdlib.compare end) - - module STRS = Set.Make( - struct -@@ -50,12 +50,12 @@ module STRS = Set.Make( - let c=compare_term a1 a2 in if c=0 then compare_term b1 b2 else c - else c - | TTconst (Treal r1) , TTconst (Treal r2) -> Num.compare_num r1 r2 -- | x , y -> Pervasives.compare x y -+ | x , y -> Stdlib.compare x y - and compare_list l1 l2 = match l1,l2 with - [] , _ -> -1 - | _ , [] -> 1 - | x::l1 , y::l2 -> -- let c = Pervasives.compare x y in if c=0 then compare_list l1 l2 else c -+ let c = Stdlib.compare x y in if c=0 then compare_list l1 l2 else c - - let compare (t1,_,_) (t2,_,_) = compare_term t1 t2 - end) -@@ -75,7 +75,7 @@ let compare_tconstant c1 c2 = - | Tbitv s1, Tbitv s2 -> String.compare s1 s2 - | Tbitv s1, _ -> 1 - | _, Tbitv s2 -> -1 -- | _ -> Pervasives.compare c1 c2 -+ | _ -> Stdlib.compare c1 c2 - - let rec depth_tterm t = - match t.c.tt_desc with -@@ -153,7 +153,7 @@ let rec compare_tterm t1 t2 = - - | TTinInterval (e1, a1, b1, c1, d1), TTinInterval (e2, a2, b2, c2, d2) -> - let c = compare_tterm e1 e2 in -- if c <> 0 then c else Pervasives.compare (a1, b1, c1, d1) (a2, b2, c2, d2) -+ if c <> 0 then c else Stdlib.compare (a1, b1, c1, d1) (a2, b2, c2, d2) - - | TTinInterval _, _ -> -1 - | _, TTinInterval _ -> 1 -@@ -191,7 +191,7 @@ let rec compare_tterm t1 t2 = - | TTconcat _, _ -> -1 - | _, TTconcat _ -> 1 - | TTdot(t1, a1), TTdot(t2,a2) -> -- let c = Pervasives.compare a1 a2 in -+ let c = Stdlib.compare a1 a2 in - if c<>0 then c else - compare_tterm t1 t2 - | TTdot _, _ -> -1 ---- alt-ergo-2.2.0/lib/frontend/typechecker.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/frontend/typechecker.ml 2021-01-29 16:43:14.235096310 -0700 -@@ -36,7 +36,7 @@ module S = Set.Make(String) - module Sy = Symbols.Set +--- alt-ergo-2.3.0/lib/frontend/typechecker.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/frontend/typechecker.ml 2021-12-13 11:22:42.669959468 -0700 +@@ -37,7 +37,7 @@ module S = Set.Make(String) + module HSS = Hstring.Set module MString = - Map.Make(struct type t = string let compare = Pervasives.compare end) @@ -73,17 +9,17 @@ module Types = struct -@@ -78,7 +78,7 @@ module Types = struct +@@ -86,7 +86,7 @@ module Types = struct List.for_all2 - (fun pp x -> - match pp with -- | PPTvarid (y, _) -> Pervasives.(=) x y -+ | PPTvarid (y, _) -> Stdlib.(=) x y - | _ -> false + (fun pp x -> + match pp with +- | PPTvarid (y, _) -> Pervasives.(=) x y ++ | PPTvarid (y, _) -> Stdlib.(=) x y + | _ -> false ) lpp lvars with Invalid_argument _ -> false -@@ -97,7 +97,7 @@ module Types = struct - to_tyvars := MString.add s nty !to_tyvars; +@@ -105,7 +105,7 @@ module Types = struct + to_tyvars := MString.add s nty !to_tyvars; nty end - | PPTexternal (l, s, loc) when Pervasives.(=) s "farray" -> @@ -91,49 +27,27 @@ let t1,t2 = match l with | [t2] -> PPTint,t2 | [t1;t2] -> t1,t2 -@@ -108,7 +108,7 @@ module Types = struct +@@ -116,7 +116,7 @@ module Types = struct | PPTexternal (l, s, loc) -> begin - match rectype with -- | Some (id, vars, ty) when Pervasives.(=) s id && -+ | Some (id, vars, ty) when Stdlib.(=) s id && - equal_pp_vars l vars -> ty - | _ -> - try -@@ -769,7 +769,7 @@ and type_form ?(in_theory=false) env f = + match rectype with +- | Some (id, vars, ty) when Pervasives.(=) s id && ++ | Some (id, vars, ty) when Stdlib.(=) s id && + equal_pp_vars l vars -> ty + | _ -> try - List.iter2 Ty.unify lt lt_args; - let r = -- if Pervasives.(=) p "<=" || Pervasives.(=) p "<" then -+ if Stdlib.(=) p "<=" || Stdlib.(=) p "<" then - TFatom { c = TAbuilt(Hstring.make p,te_args); - annot=new_id ()} - else -@@ -1871,10 +1871,10 @@ let file ld = - exit 1 - - let is_local_hyp s = -- try Pervasives.(=) (String.sub s 0 2) "@L" with Invalid_argument _ -> false -+ try Stdlib.(=) (String.sub s 0 2) "@L" with Invalid_argument _ -> false - - let is_global_hyp s = -- try Pervasives.(=) (String.sub s 0 2) "@H" with Invalid_argument _ -> false -+ try Stdlib.(=) (String.sub s 0 2) "@H" with Invalid_argument _ -> false - - let split_goals_aux f l = - let _, _, _, ret = ---- alt-ergo-2.2.0/lib/reasoners/fun_sat.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/reasoners/fun_sat.ml 2021-01-29 16:44:04.915064713 -0700 -@@ -69,7 +69,7 @@ module Make (Th : Theory.S) : Sat_solver - SF.fold +--- alt-ergo-2.3.0/lib/reasoners/fun_sat.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/reasoners/fun_sat.ml 2021-12-13 11:17:14.158193751 -0700 +@@ -75,7 +75,7 @@ module Make (Th : Theory.S) : Sat_solver + SE.fold (fun f mp -> - let w = var_inc +. try MF.find f mp with Not_found -> 0. in + let w = var_inc +. try ME.find f mp with Not_found -> 0. in - stable := !stable && Pervasives.(<=) w 1e100; + stable := !stable && Stdlib.(<=) w 1e100; - MF.add f w mp + ME.add f w mp )(Ex.bj_formulas_of expl) mp in -@@ -95,9 +95,9 @@ module Make (Th : Theory.S) : Sat_solver +@@ -118,9 +118,9 @@ module Make (Th : Theory.S) : Sat_solver let dec = List.fast_sort (fun (_, x1, b1) (_, x2, b2) -> @@ -145,7 +59,7 @@ )dec in (* -@@ -967,7 +967,7 @@ module Make (Th : Theory.S) : Sat_solver +@@ -1171,7 +1171,7 @@ module Make (Th : Theory.S) : Sat_solver let i = abs (interpretation ()) in assert (i = 1 || i = 2 || i = 3); if not !(env.model_gen_mode) && @@ -154,20 +68,20 @@ begin Options.Time.unset_timeout ~is_gui:(Options.get_is_gui()); Options.Time.set_timeout ---- alt-ergo-2.2.0/lib/reasoners/ite.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/reasoners/ite.ml 2021-01-29 15:13:41.631062282 -0700 -@@ -72,7 +72,7 @@ module Relation (X : ALIEN) (Uf : Uf.S) - type t = T.t * bool - let compare (a1, b1) (a2, b2) = - let c = T.compare a1 a2 in -- if c <> 0 then c else Pervasives.compare b1 b2 -+ if c <> 0 then c else Stdlib.compare b1 b2 - end) +--- alt-ergo-2.3.0/lib/reasoners/ite_rel.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/reasoners/ite_rel.ml 2021-12-13 11:18:06.781156246 -0700 +@@ -32,7 +32,7 @@ module TB = + type t = E.t * bool + let compare (a1, b1) (a2, b2) = + let c = E.compare a1 a2 in +- if c <> 0 then c else Pervasives.compare b1 b2 ++ if c <> 0 then c else Stdlib.compare b1 b2 + end) - type t = ---- alt-ergo-2.2.0/lib/reasoners/satml_frontend.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/reasoners/satml_frontend.ml 2021-01-29 16:16:47.003462456 -0700 -@@ -533,7 +533,7 @@ module Make (Th : Theory.S) : Sat_solver + type t = +--- alt-ergo-2.3.0/lib/reasoners/satml_frontend.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/reasoners/satml_frontend.ml 2021-12-13 11:17:48.709169125 -0700 +@@ -508,7 +508,7 @@ module Make (Th : Theory.S) : Sat_solver if res <> 0 then res else (* higher weight is better hence compare w2 w1 *) @@ -176,27 +90,45 @@ if res <> 0 then res else (* lower index is better *) -@@ -922,7 +922,7 @@ module Make (Th : Theory.S) : Sat_solver +@@ -844,7 +844,7 @@ module Make (Th : Theory.S) : Sat_solver + } + + let normal_mconf () = +- {Util.nb_triggers = Pervasives.max 2 (nb_triggers () * 2); ++ {Util.nb_triggers = Stdlib.max 2 (nb_triggers () * 2); + no_ematching = no_Ematching(); + triggers_var = triggers_var (); + use_cs = false; +@@ -853,7 +853,7 @@ module Make (Th : Theory.S) : Sat_solver + } + + let greedy_mconf () = +- {Util.nb_triggers = Pervasives.max 10 (nb_triggers () * 10); ++ {Util.nb_triggers = Stdlib.max 10 (nb_triggers () * 10); + no_ematching = false; + triggers_var = true; + use_cs = true; +@@ -951,7 +951,7 @@ module Make (Th : Theory.S) : Sat_solver (* copied from sat_solvers.ml *) let max_term_depth_in_sat env = -- let aux mx f = Pervasives.max mx (F.max_term_depth f) in -+ let aux mx f = Stdlib.max mx (F.max_term_depth f) in - let max_t = MF.fold (fun f _ mx -> aux mx f) env.gamma 0 in - A.Map.fold (fun _ {F.f} mx -> aux mx f) env.ground_preds max_t +- let aux mx f = Pervasives.max mx (E.depth f) in ++ let aux mx f = Stdlib.max mx (E.depth f) in + let max_t = ME.fold (fun f _ mx -> aux mx f) env.gamma 0 in + ME.fold (fun _ ({ E.ff = f; _ }, _) mx -> aux mx f) env.ground_preds max_t ---- alt-ergo-2.2.0/lib/reasoners/satml.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/reasoners/satml.ml 2021-01-29 16:44:54.595033743 -0700 -@@ -351,7 +351,7 @@ module Make (Th : Theory.S) : SAT_ML wit +--- alt-ergo-2.3.0/lib/reasoners/satml.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/reasoners/satml.ml 2021-12-13 11:18:53.173123173 -0700 +@@ -361,7 +361,7 @@ module Make (Th : Theory.S) : SAT_ML wit *) let f_weight env i j = - Pervasives.(<) (Vec.get env.vars j).weight (Vec.get env.vars i).weight + Stdlib.(<) (Vec.get env.vars j).weight (Vec.get env.vars i).weight - let f_filter env i = (Vec.get env.vars i).level < 0 + (* unused -- let f_filter env i = (Vec.get env.vars i).level < 0 *) -@@ -365,7 +365,7 @@ module Make (Th : Theory.S) : SAT_ML wit +@@ -375,7 +375,7 @@ module Make (Th : Theory.S) : SAT_ML wit let var_bump_activity env v = v.weight <- v.weight +. env.var_inc; @@ -205,7 +137,7 @@ for i = 0 to env.vars.Vec.sz - 1 do (Vec.get env.vars i).weight <- (Vec.get env.vars i).weight *. 1e-100 done; -@@ -377,7 +377,7 @@ module Make (Th : Theory.S) : SAT_ML wit +@@ -387,7 +387,7 @@ module Make (Th : Theory.S) : SAT_ML wit let clause_bump_activity env c = c.activity <- c.activity +. env.clause_inc; @@ -214,51 +146,77 @@ for i = 0 to env.learnts.Vec.sz - 1 do (Vec.get env.learnts i).activity <- (Vec.get env.learnts i).activity *. 1e-20; -@@ -861,7 +861,7 @@ let compute_facts_for_theory_propagate e - let f_sort_db c1 c2 = - let sz1 = Vec.size c1.atoms in - let sz2 = Vec.size c2.atoms in -- let c = Pervasives.compare c1.activity c2.activity in -+ let c = Stdlib.compare c1.activity c2.activity in - if sz1 = sz2 && c = 0 then 0 - else - if sz1 > 2 && (sz2 = 2 || c < 0) then -1 ---- alt-ergo-2.2.0/lib/structures/formula.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/structures/formula.ml 2021-01-29 16:34:03.946514585 -0700 -@@ -108,8 +108,8 @@ type gformula = { - let size (t,_) = t.size +--- alt-ergo-2.3.0/lib/structures/expr.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/structures/expr.ml 2021-12-13 11:27:30.381754212 -0700 +@@ -1031,7 +1031,7 @@ let mk_builtin ~is_pos n l = + (** Substitutions *) - let compare ((v1,_) as f1) ((v2,_) as f2) = -- let c = Pervasives.compare (size f1) (size f2) in -- if c=0 then Pervasives.compare v1.tag v2.tag else c -+ let c = Stdlib.compare (size f1) (size f2) in -+ if c=0 then Stdlib.compare v1.tag v2.tag else c - - let equal (f1,_) (f2,_) = - assert ((f1 == f2) == (f1.tag == f2.tag)); -@@ -866,7 +866,7 @@ let label f = - | _ -> Hstring.empty - - let label_model h = -- try Pervasives.(=) (String.sub (Hstring.view h) 0 6) "model:" -+ try Stdlib.(=) (String.sub (Hstring.view h) 0 6) "model:" + let is_skolem_cst v = +- try Pervasives.(=) (String.sub (Sy.to_string v.f) 0 4) "_sko" ++ try Stdlib.(=) (String.sub (Sy.to_string v.f) 0 4) "_sko" with Invalid_argument _ -> false - let is_in_model f = ---- alt-ergo-2.2.0/lib/structures/literal.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/structures/literal.ml 2021-01-29 15:11:35.935224734 -0700 -@@ -95,7 +95,7 @@ module Make (X : OrderedType) : S with t + let get_skolem = +@@ -1669,9 +1669,9 @@ module Triggers = struct + | { f = (Name _) as s1; xs=tl1; _ }, { f = (Name _) as s2; xs=tl2; _ } -> + let l1 = List.map score_term tl1 in + let l2 = List.map score_term tl2 in +- let l1 = List.fast_sort Pervasives.compare l1 in +- let l2 = List.fast_sort Pervasives.compare l2 in +- let c = Util.cmp_lists l1 l2 Pervasives.compare in ++ let l1 = List.fast_sort Stdlib.compare l1 in ++ let l2 = List.fast_sort Stdlib.compare l2 in ++ let c = Util.cmp_lists l1 l2 Stdlib.compare in + if c <> 0 then c + else + let c = Sy.compare s1 s2 in +@@ -1702,7 +1702,7 @@ module Triggers = struct - type t = { at : atom; neg : bool; tpos : int; tneg : int } + | { f = Op (Access a1) ; xs=[t1]; _ }, + { f = Op (Access a2) ; xs=[t2]; _ } -> +- let c = Pervasives.compare a1 a2 in (* should be Hstring.compare *) ++ let c = Stdlib.compare a1 a2 in (* should be Hstring.compare *) + if c<>0 then c else cmp_trig_term t1 t2 -- let compare a1 a2 = Pervasives.compare a1.tpos a2.tpos -+ let compare a1 a2 = Stdlib.compare a1.tpos a2.tpos - let equal a1 a2 = a1.tpos = a2.tpos (* XXX == *) - let hash a1 = a1.tpos - let uid a1 = a1.tpos ---- alt-ergo-2.2.0/lib/structures/profiling.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/structures/profiling.ml 2021-01-29 16:41:48.035150044 -0700 -@@ -86,7 +86,7 @@ let state = + | { f = Op (Access _); _ }, _ -> -1 +@@ -1710,7 +1710,7 @@ module Triggers = struct + + | { f = Op (Destruct (_,a1)) ; xs = [t1]; _ }, + { f = Op (Destruct (_,a2)) ; xs = [t2]; _ } -> +- let c = Pervasives.compare a1 a2 in (* should be Hstring.compare *) ++ let c = Stdlib.compare a1 a2 in (* should be Hstring.compare *) + if c<>0 then c else cmp_trig_term t1 t2 + + | { f = Op (Destruct _); _ }, _ -> -1 +@@ -1725,9 +1725,9 @@ module Triggers = struct + (* ops that are not infix or prefix *) + let l1 = List.map score_term tl1 in + let l2 = List.map score_term tl2 in +- let l1 = List.fast_sort Pervasives.compare l1 in +- let l2 = List.fast_sort Pervasives.compare l2 in +- let c = Util.cmp_lists l1 l2 Pervasives.compare in ++ let l1 = List.fast_sort Stdlib.compare l1 in ++ let l2 = List.fast_sort Stdlib.compare l2 in ++ let c = Util.cmp_lists l1 l2 Stdlib.compare in + if c <> 0 then c + else + let c = Sy.compare s1 s2 in +@@ -1741,9 +1741,9 @@ module Triggers = struct + let cmp_trig_term_list tl2 tl1 = + let l1 = List.map score_term tl1 in + let l2 = List.map score_term tl2 in +- let l1 = List.rev (List.fast_sort Pervasives.compare l1) in +- let l2 = List.rev (List.fast_sort Pervasives.compare l2) in +- let c = Util.cmp_lists l1 l2 Pervasives.compare in ++ let l1 = List.rev (List.fast_sort Stdlib.compare l1) in ++ let l2 = List.rev (List.fast_sort Stdlib.compare l2) in ++ let c = Util.cmp_lists l1 l2 Stdlib.compare in + if c <> 0 then c else Util.cmp_lists tl1 tl2 cmp_trig_term + + let unique_stable_sort = +--- alt-ergo-2.3.0/lib/structures/profiling.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/structures/profiling.ml 2021-12-13 11:28:14.180722957 -0700 +@@ -85,7 +85,7 @@ let state = let set_sigprof () = let tm = let v = Options.profiling_period () in @@ -267,7 +225,7 @@ in ignore (Unix.setitimer Unix.ITIMER_PROF -@@ -626,9 +626,9 @@ let switch () = +@@ -629,9 +629,9 @@ let switch () = let float_print fmt v = @@ -280,59 +238,61 @@ else fprintf fmt "%0.3f" v let line_of_module arr f = ---- alt-ergo-2.2.0/lib/structures/symbols.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/structures/symbols.ml 2021-01-29 15:10:23.775316438 -0700 -@@ -114,7 +114,7 @@ let compare s1 s2 = match s1, s2 with - | Op(Access s1), Op(Access s2) -> Hstring.compare s1 s2 - | Op(Access _), _ -> -1 - | _, Op(Access _) -> 1 -- | _ -> Pervasives.compare s1 s2 -+ | _ -> Stdlib.compare s1 s2 +--- alt-ergo-2.3.0/lib/structures/symbols.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/structures/symbols.ml 2021-12-13 11:23:17.604934542 -0700 +@@ -124,7 +124,7 @@ let compare_operators op1 op2 = + (function + | Access h1, Access h2 | Constr h1, Constr h2 -> Hstring.compare h1 h2 + | Destruct (h1, b1), Destruct(h2, b2) -> +- let c = Pervasives.compare b1 b2 in ++ let c = Stdlib.compare b1 b2 in + if c <> 0 then c else Hstring.compare h1 h2 + | _ , (Plus | Minus | Mult | Div | Modulo + | Concat | Extract | Get | Set | Fixed | Float | Reach +@@ -155,7 +155,7 @@ let compare_forms f1 f2 = + Util.compare_algebraic f1 f2 + (function + | F_Unit b1, F_Unit b2 +- | F_Clause b1, F_Clause b2 -> Pervasives.compare b1 b2 ++ | F_Clause b1, F_Clause b2 -> Stdlib.compare b1 b2 + | _, (F_Unit _ | F_Clause _ | F_Lemma | F_Skolem + | F_Iff | F_Xor) -> + assert false +@@ -173,10 +173,10 @@ let compare_bounds a b = + let c = Ty.compare a.sort b.sort in + if c <> 0 then c + else +- let c = Pervasives.compare a.is_open b.is_open in ++ let c = Stdlib.compare a.is_open b.is_open in + if c <> 0 then c + else +- let c = Pervasives.compare a.is_lower b.is_lower in ++ let c = Stdlib.compare a.is_lower b.is_lower in + if c <> 0 then c + else compare_bounds_kind a.kind b.kind - let equal s1 s2 = compare s1 s2 = 0 - ---- alt-ergo-2.2.0/lib/structures/term.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/structures/term.ml 2021-01-29 16:33:11.033560074 -0700 -@@ -270,7 +270,7 @@ let gen_sko ty = make (Sy.fresh "@sko") - - let is_skolem_cst v = - try -- Pervasives.(=) (String.sub (Sy.to_string v.f) 0 4) "_sko" -+ Stdlib.(=) (String.sub (Sy.to_string v.f) 0 4) "_sko" - with Invalid_argument _ -> false - - let find_skolem = -@@ -338,7 +338,7 @@ let label t = try Labels.find labels t w - - - let label_model h = -- try Pervasives.(=) (String.sub (Hstring.view h) 0 6) "model:" -+ try Stdlib.(=) (String.sub (Hstring.view h) 0 6) "model:" - with Invalid_argument _ -> false - - let rec is_in_model_rec depth { f = f; xs = xs } = ---- alt-ergo-2.2.0/lib/structures/ty.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/structures/ty.ml 2021-01-29 16:18:15.746370389 -0700 -@@ -202,7 +202,7 @@ let rec equal t1 t2 = +--- alt-ergo-2.3.0/lib/structures/ty.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/structures/ty.ml 2021-12-13 11:23:47.596913146 -0700 +@@ -201,7 +201,7 @@ and shorten_body _ _ = let rec compare t1 t2 = match shorten t1 , shorten t2 with -- | Tvar{v=v1} , Tvar{v=v2} -> Pervasives.compare v1 v2 -+ | Tvar{v=v1} , Tvar{v=v2} -> Stdlib.compare v1 v2 - | Tvar _, _ -> -1 | _ , Tvar _ -> 1 - | Text(l1, s1) , Text(l2, s2) -> - let c = Hstring.compare s1 s2 in -@@ -225,7 +225,7 @@ let rec compare t1 t2 = - let l1, l2 = List.map snd l1, List.map snd l2 in - compare_list l1 l2 - | Trecord _, _ -> -1 | _ , Trecord _ -> 1 -- | t1 , t2 -> Pervasives.compare t1 t2 -+ | t1 , t2 -> Stdlib.compare t1 t2 - and compare_list l1 l2 = match l1, l2 with - | [] , [] -> 0 - | [] , _ -> -1 -@@ -268,7 +268,7 @@ let rec unify t1 t2 = +- | Tvar{ v = v1; _ } , Tvar{ v = v2; _ } -> Pervasives.compare v1 v2 ++ | Tvar{ v = v1; _ } , Tvar{ v = v2; _ } -> Stdlib.compare v1 v2 + | Tvar _, _ -> -1 | _ , Tvar _ -> 1 + | Text(l1, s1) , Text(l2, s2) -> + let c = Hstring.compare s1 s2 in +@@ -234,7 +234,7 @@ let rec compare t1 t2 = + | Tadt _, _ -> -1 | _ , Tadt _ -> 1 + +- | t1 , t2 -> Pervasives.compare t1 t2 ++ | t1 , t2 -> Stdlib.compare t1 t2 + + + and compare_list l1 l2 = match l1, l2 with +@@ -278,7 +278,7 @@ let rec equal t1 t2 = + | _ -> false (*** matching with a substitution mechanism ***) -module M = Map.Make(struct type t=int let compare = Pervasives.compare end) @@ -340,7 +300,7 @@ type subst = t M.t let esubst = M.empty -@@ -340,9 +340,9 @@ let instantiate lvar lty ty = +@@ -602,12 +602,12 @@ let instantiate lvar lty ty = let union_subst s1 s2 = M.fold (fun k x s2 -> M.add k x s2) (M.map (apply_subst s2) s1) s2 @@ -350,20 +310,61 @@ -let equal_subst = M.equal Pervasives.(=) +let equal_subst = M.equal Stdlib.(=) - let rec fresh ty subst = - match ty with -@@ -383,7 +383,7 @@ and fresh_list lty subst = - ty::lty, subst) lty ([], subst) - module Svty = - Set.Make(struct type t = int let compare = Pervasives.compare end) + Set.Make(struct type t = int let compare = Stdlib.compare end) module Set = Set.Make(struct ---- alt-ergo-2.2.0/lib/util/myUnix.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/util/myUnix.ml 2021-01-29 16:45:33.010009798 -0700 -@@ -16,7 +16,7 @@ module Default_Unix = struct +--- alt-ergo-2.3.0/lib/structures/typed.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/structures/typed.ml 2021-12-13 11:28:32.876709614 -0700 +@@ -369,8 +369,8 @@ let fresh_hypothesis_name = + | _ -> "@L"^(string_of_int !cpt) + + let is_local_hyp s = +- try Pervasives.(=) (String.sub s 0 2) "@L" with Invalid_argument _ -> false ++ try Stdlib.(=) (String.sub s 0 2) "@L" with Invalid_argument _ -> false + + let is_global_hyp s = +- try Pervasives.(=) (String.sub s 0 2) "@H" with Invalid_argument _ -> false ++ try Stdlib.(=) (String.sub s 0 2) "@H" with Invalid_argument _ -> false + +--- alt-ergo-2.3.0/lib/structures/xliteral.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/structures/xliteral.ml 2021-12-13 11:27:49.604740495 -0700 +@@ -103,7 +103,7 @@ module Make (X : OrderedType) : S with t + + type t = { at : atom; neg : bool; tpos : int; tneg : int } + +- let compare a1 a2 = Pervasives.compare a1.tpos a2.tpos ++ let compare a1 a2 = Stdlib.compare a1.tpos a2.tpos + let equal a1 a2 = a1.tpos = a2.tpos (* XXX == *) + let hash a1 = a1.tpos + let uid a1 = a1.tpos +--- alt-ergo-2.3.0/lib/util/emap.mli.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/util/emap.mli 2021-12-13 11:20:53.277037515 -0700 +@@ -41,8 +41,8 @@ + struct + type t = int * int + let compare (x0,y0) (x1,y1) = +- match Pervasives.compare x0 x1 with +- 0 -> Pervasives.compare y0 y1 ++ match Stdlib.compare x0 x1 with ++ 0 -> Stdlib.compare y0 y1 + | c -> c + end + +@@ -68,7 +68,7 @@ sig + [f e1 e2] is strictly negative if [e1] is smaller than [e2], + and [f e1 e2] is strictly positive if [e1] is greater than [e2]. + Example: a suitable ordering function is the generic structural +- comparison function {!Pervasives.compare}. *) ++ comparison function {!Stdlib.compare}. *) + end + (** Input signature of the functor {!Map.Make}. *) + +--- alt-ergo-2.3.0/lib/util/myUnix.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/util/myUnix.ml 2021-12-13 11:19:46.141085403 -0700 +@@ -18,7 +18,7 @@ module Default_Unix = struct let cur_time () = (times()).tms_utime let set_timeout ~is_gui timelimit = @@ -372,33 +373,54 @@ let itimer = if is_gui then Unix.ITIMER_REAL (* troubles with VIRTUAL *) else Unix.ITIMER_VIRTUAL ---- alt-ergo-2.2.0/lib/util/numbers.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/util/numbers.ml 2021-01-29 16:46:06.130989159 -0700 +--- alt-ergo-2.3.0/lib/util/numbers.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/util/numbers.ml 2021-12-13 11:22:11.316981841 -0700 @@ -48,8 +48,8 @@ module Q = struct - else - let v = to_float q in - let w = -- if Pervasives.(<) v min_float then min_float -- else if Pervasives.(>) v max_float then max_float -+ if Stdlib.(<) v min_float then min_float -+ else if Stdlib.(>) v max_float then max_float - else v - in - let flt = if n = 2 then sqrt w else w ** (1. /. float n) in ---- alt-ergo-2.2.0/lib/util/options.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/util/options.ml 2021-01-29 16:11:53.387767103 -0700 -@@ -902,8 +902,7 @@ let (>) (a: int) (b: int) = a > b + else + let v = to_float q in + let w = +- if Pervasives.(<) v min_float then min_float +- else if Pervasives.(>) v max_float then max_float ++ if Stdlib.(<) v min_float then min_float ++ else if Stdlib.(>) v max_float then max_float + else v + in + let flt = if n = 2 then sqrt w else w ** (1. /. float n) in +--- alt-ergo-2.3.0/lib/util/options.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/util/options.ml 2021-12-13 11:21:27.477013115 -0700 +@@ -957,7 +957,7 @@ let (>) (a: int) (b: int) = a > b let (<=) (a: int) (b: int) = a <= b let (>=) (a: int) (b: int) = a >= b -let compare (a: int) (b: int) = Pervasives.compare a b -- +let compare (a: int) (b: int) = Stdlib.compare a b - (* extra **) ---- alt-ergo-2.2.0/lib/util/zarithNumbers.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/lib/util/zarithNumbers.ml 2021-01-29 16:08:45.571962041 -0700 + (* extra **) +--- alt-ergo-2.3.0/lib/util/util.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/util/util.ml 2021-12-13 11:20:25.717057175 -0700 +@@ -83,7 +83,7 @@ let [@inline always] compare_algebraic s + let r1 = Obj.repr s1 in + let r2 = Obj.repr s2 in + match Obj.is_int r1, Obj.is_int r2 with +- | true, true -> Pervasives.compare s1 s2 (* both constructors without args *) ++ | true, true -> Stdlib.compare s1 s2 (* both constructors without args *) + | true, false -> -1 + | false, true -> 1 + | false, false -> +--- alt-ergo-2.3.0/lib/util/util.mli.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/util/util.mli 2021-12-13 11:20:10.341068143 -0700 +@@ -56,7 +56,7 @@ val string_of_th_ext : theories_extensio + (** + generic function for comparing algebraic data types. + [compare_algebraic a b f] +- - Pervasives.compare a b is used if ++ - Stdlib.compare a b is used if + + *) + val [@inline always] compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int +--- alt-ergo-2.3.0/lib/util/zarithNumbers.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/lib/util/zarithNumbers.ml 2021-12-13 11:19:11.821109879 -0700 @@ -153,7 +153,7 @@ module Q : NumbersInterface.QSig with mo let floor t = from_z (Z.fdiv (num t) (den t)) let ceiling t = from_z (Z.cdiv (num t) (den t)) @@ -408,9 +430,20 @@ let num_pow = Z.power (num t) abs_n in let den_pow = Z.power (den t) abs_n in if n >= 0 then from_zz num_pow den_pow else from_zz den_pow num_pow ---- alt-ergo-2.2.0/tools/gui/annoted_ast.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/tools/gui/annoted_ast.ml 2021-01-29 16:47:08.762950125 -0700 -@@ -188,7 +188,7 @@ type annoted_node = +--- alt-ergo-2.3.0/parsers/parsers.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/parsers/parsers.ml 2021-12-13 11:16:42.461216342 -0700 +@@ -124,7 +124,7 @@ let parse_input_file file = + stdin, Lexing.from_string file_content, false, ext + else + let ext = Filename.extension file in +- if Pervasives.(<>) file "" then ++ if Stdlib.(<>) file "" then + let cin = open_in file in + cin, Lexing.from_channel cin, true, ext + else +--- alt-ergo-2.3.0/tools/gui/annoted_ast.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/tools/gui/annoted_ast.ml 2021-12-13 11:15:02.334287694 -0700 +@@ -191,7 +191,7 @@ type annoted_node = module MDep = Map.Make ( struct type t = atyped_decl annoted @@ -419,58 +452,58 @@ end) -@@ -862,9 +862,9 @@ let find_dep_by_string dep s = - | None -> begin - match d.c with - | ALogic (_, ls, ty) when List.mem s ls -> Some d -- | ATypeDecl (_, _, s', _) when Pervasives.(=) s s'-> Some d -- | APredicate_def (_, p, _, _) when Pervasives.(=) s p -> Some d -- | AFunction_def (_, f, _, _, _) when Pervasives.(=) s f -> Some d -+ | ATypeDecl (_, _, s', _) when Stdlib.(=) s s'-> Some d -+ | APredicate_def (_, p, _, _) when Stdlib.(=) s p -> Some d -+ | AFunction_def (_, f, _, _, _) when Stdlib.(=) s f -> Some d - | _ -> None - end +@@ -880,9 +880,9 @@ let find_dep_by_string dep s = + | None -> begin + match d.c with + | ALogic (_, ls, _, _) when List.mem s ls -> Some d +- | ATypeDecl (_, _, s', _, _) when Pervasives.(=) s s'-> Some d +- | APredicate_def (_, p, _, _) when Pervasives.(=) s p -> Some d +- | AFunction_def (_, f, _, _, _, _) when Pervasives.(=) s f -> Some d ++ | ATypeDecl (_, _, s', _, _) when Stdlib.(=) s s'-> Some d ++ | APredicate_def (_, p, _, _) when Stdlib.(=) s p -> Some d ++ | AFunction_def (_, f, _, _, _, _) when Stdlib.(=) s f -> Some d + | _ -> None + end ) dep None -@@ -874,7 +874,7 @@ let find_tag_deps dep tag = +@@ -892,7 +892,7 @@ let find_tag_deps dep tag = (fun d (deps,_) found -> - match found with - | Some _ -> found -- | None -> if Pervasives.(=) d.tag tag then Some deps else None -+ | None -> if Stdlib.(=) d.tag tag then Some deps else None + match found with + | Some _ -> found +- | None -> if Pervasives.(=) d.tag tag then Some deps else None ++ | None -> if Stdlib.(=) d.tag tag then Some deps else None ) dep None let find_tag_inversedeps dep tag = -@@ -882,7 +882,7 @@ let find_tag_inversedeps dep tag = +@@ -900,7 +900,7 @@ let find_tag_inversedeps dep tag = (fun d (_,deps) found -> - match found with - | Some _ -> found -- | None -> if Pervasives.(=) d.tag tag then Some deps else None -+ | None -> if Stdlib.(=) d.tag tag then Some deps else None + match found with + | Some _ -> found +- | None -> if Pervasives.(=) d.tag tag then Some deps else None ++ | None -> if Stdlib.(=) d.tag tag then Some deps else None ) dep None let make_dep_string d ex dep s = -@@ -1965,7 +1965,7 @@ and findtags_aform sl aform acc = - (fun sl (sy, _) -> - let s = Symbols.to_string_clean sy in - List.fold_left -- (fun l s' -> if Pervasives.(=) s' s then l else s'::l) [] sl -+ (fun l s' -> if Stdlib.(=) s' s then l else s'::l) [] sl - )sl l - in - findtags_aform sl aaf.c acc ---- alt-ergo-2.2.0/tools/gui/connected_ast.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/tools/gui/connected_ast.ml 2021-01-29 16:47:43.226928651 -0700 -@@ -386,7 +386,7 @@ let rec unquantify_aform (buffer:sbuffer - List.fold_left (fun (nbv, used, goal_used, ve, uplet, lets) v -> - let ((s, _) as v'), e = List.hd ve in - let cdr_ve = List.tl ve in -- assert (Pervasives.(=) v v'); -+ assert (Stdlib.(=) v v'); - if String.length e == 0 then - (v'::nbv, used, goal_used, cdr_ve, v'::uplet, lets) - else -@@ -541,7 +541,7 @@ let rec add_instance_aux ?(register=true +@@ -2046,7 +2046,7 @@ and findtags_aform sl aform acc = + (fun sl (sy, _) -> + let s = Symbols.to_string_clean sy in + List.fold_left +- (fun l s' -> if Pervasives.(=) s' s then l else s'::l) [] sl ++ (fun l s' -> if Stdlib.(=) s' s then l else s'::l) [] sl + )sl l + in + findtags_aform sl aaf.c acc +--- alt-ergo-2.3.0/tools/gui/connected_ast.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/tools/gui/connected_ast.ml 2021-12-13 11:16:16.069235150 -0700 +@@ -388,7 +388,7 @@ let rec unquantify_aform (buffer:sbuffer + List.fold_left (fun (nbv, used, goal_used, ve, uplet, lets) v -> + let ((s, _) as v'), e = List.hd ve in + let cdr_ve = List.tl ve in +- assert (Pervasives.(=) v v'); ++ assert (Stdlib.(=) v v'); + if String.length e == 0 then + (v'::nbv, used, goal_used, cdr_ve, v'::uplet, lets) + else +@@ -545,7 +545,7 @@ let rec add_instance_aux ?(register=true make_instance env.inst_buffer vars entries af goal_form tyenv in let ln_form = least_nested_form used_vars goal_form in env.inst_buffer#place_cursor ~where:env.inst_buffer#end_iter; @@ -479,18 +512,18 @@ let hy = AAxiom (loc, (sprintf "%s%s" "_instance_" aname), ax_kd, instance.c) in let ahy = new_annot env.inst_buffer hy instance.id ptag in -@@ -735,7 +735,7 @@ and add_trigger ?(register=true) t qid e - if register then - save env.actions - (AddTrigger (qf.id, -- Pervasives.(=) sbuf env.inst_buffer, str)); -+ Stdlib.(=) sbuf env.inst_buffer, str)); - commit_tags_buffer sbuf - | _ -> assert false - end ---- alt-ergo-2.2.0/tools/gui/main_gui.ml.orig 2018-04-21 11:02:10.000000000 -0600 -+++ alt-ergo-2.2.0/tools/gui/main_gui.ml 2021-01-29 16:49:56.218845792 -0700 -@@ -148,7 +148,7 @@ let save_session envs = +@@ -739,7 +739,7 @@ and add_trigger ?(register=true) t qid e + if register then + save env.actions + (AddTrigger (qf.id, +- Pervasives.(=) sbuf env.inst_buffer, str)); ++ Stdlib.(=) sbuf env.inst_buffer, str)); + commit_tags_buffer sbuf + | _ -> assert false + end +--- alt-ergo-2.3.0/tools/gui/main_gui.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/tools/gui/main_gui.ml 2021-12-13 11:15:49.445254125 -0700 +@@ -151,7 +151,7 @@ let save_session envs = let save_dialog cancel envs () = if List.exists @@ -499,7 +532,7 @@ if List.exists (fun env -> not (Gui_session.safe_session env.actions)) envs then GToolbox.message_box -@@ -247,7 +247,7 @@ let pop_model sat_env () = +@@ -250,7 +250,7 @@ let pop_model sat_env () = let compare_rows icol_number (model:#GTree.model) row1 row2 = let t1 = model#get ~row:row1 ~column:icol_number in let t2 = model#get ~row:row2 ~column:icol_number in @@ -517,16 +550,16 @@ t.tl_sat#set_text (sprintf "%3.2f s" tsat); t.tl_match#set_text (sprintf "%3.2f s" tmatch); -@@ -455,7 +455,7 @@ let add_inst ({h=h} as inst_model) orig - let id = Formula.id orig in +@@ -455,7 +455,7 @@ let add_inst ({ h; _ } as inst_model) or + let id = Expr.id orig in let name = - match Formula.view orig with -- | Formula.Lemma {Formula.name=n} when Pervasives.(<>) n "" -> n -+ | Formula.Lemma {Formula.name=n} when Stdlib.(<>) n "" -> n - | _ -> string_of_int id - in - let r, n, limit, to_add = -@@ -604,7 +604,7 @@ let vt_signal = + match Expr.form_view orig with +- | Expr.Lemma { Expr.name = n ; _ } when Pervasives.(<>) n "" -> n ++ | Expr.Lemma { Expr.name = n ; _ } when Stdlib.(<>) n "" -> n + | Expr.Lemma _ | Expr.Unit _ | Expr.Clause _ | Expr.Literal _ + | Expr.Skolem _ | Expr.Let _ | Expr.Iff _ | Expr.Xor _ -> + string_of_int id +@@ -607,7 +607,7 @@ let vt_signal = let force_interrupt old_action_ref n = (* This function is called just before the thread's timeslice ends *) @@ -535,18 +568,18 @@ raise Abort_thread; match !old_action_ref with | Sys.Signal_handle f -> f n -@@ -718,8 +718,8 @@ let remove_context env () = - toggle_prune env td +@@ -723,8 +723,8 @@ let remove_context env () = + toggle_prune env td | AAxiom (_, s, _, _) - when String.length s = 0 || + when String.length s = 0 || - (Pervasives.(<>) s.[0] '_' && - Pervasives.(<>) s.[0] '@') -> + (Stdlib.(<>) s.[0] '_' && + Stdlib.(<>) s.[0] '@') -> - toggle_prune env td + toggle_prune env td | _ -> () ) env.ast -@@ -945,7 +945,7 @@ let search_all entry (sv:GSourceView2.so +@@ -951,7 +951,7 @@ let search_all entry (_sv:GSourceView2.s buf#remove_tag found_all_tag ~start:buf#start_iter ~stop:buf#end_iter; let str = entry#text in let iter = ref buf#start_iter in @@ -555,7 +588,7 @@ let result = ref None in search_one buf str result iter found_all_tag; while !result != None do -@@ -1286,7 +1286,7 @@ let start_gui () = +@@ -1300,7 +1300,7 @@ let start_gui all_used_context = let set_wrap_lines _ = List.iter (fun env -> diff --git a/alt-ergo-psmt2-frontend.patch b/alt-ergo-psmt2-frontend.patch new file mode 100644 index 0000000..1c58d9e --- /dev/null +++ b/alt-ergo-psmt2-frontend.patch @@ -0,0 +1,12 @@ +--- alt-ergo-2.3.0/parsers/psmt2_to_alt_ergo.ml.orig 2019-02-11 09:43:50.000000000 -0700 ++++ alt-ergo-2.3.0/parsers/psmt2_to_alt_ergo.ml 2021-12-13 13:45:45.216802816 -0700 +@@ -403,6 +403,9 @@ module Translate = struct + | Cmd_Push _ -> not_supported "push"; assert false + | Cmd_Pop _ -> not_supported "pop"; assert false + | Cmd_Exit -> acc ++ | Cmd_CheckAllSat _ -> not_supported "check-all-sat"; assert false ++ | Cmd_Maximize _ -> not_supported "maximize"; assert false ++ | Cmd_Minimize _ -> not_supported "minimize"; assert false + + let init () = + if Psmt2Frontend.Options.get_is_int_real () then diff --git a/alt-ergo.spec b/alt-ergo.spec index 81eca7a..b1b8edf 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -7,8 +7,8 @@ %endif Name: alt-ergo -Version: 2.2.0 -Release: 14%{?dist} +Version: 2.3.0 +Release: 1%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -18,30 +18,29 @@ Source0: https://alt-ergo.ocamlpro.com/http/%{name}-%{version}/%{name}-%{version Source1: %{name}-icons.tar.xz Source2: %{name}.desktop Source3: %{name}.metainfo.xml - -# Use the asmrun_pic variant when linking the binary. -Patch0: %{name}-1.30-use-pic.patch # Do not use the deprecated Pervasives interface -Patch1: %{name}-pervasives.patch +Patch0: %{name}-pervasives.patch +# Adapt to recent changes in psmt2-frontend +Patch1: %{name}-psmt2-frontend.patch BuildRequires: appstream BuildRequires: desktop-file-utils BuildRequires: gtksourceview2-devel BuildRequires: make -BuildRequires: ocaml +BuildRequires: ocaml >= 4.04.0 +BuildRequires: ocaml-dune BuildRequires: ocaml-findlib BuildRequires: ocaml-lablgtk-devel BuildRequires: ocaml-menhir BuildRequires: ocaml-num-devel -BuildRequires: ocaml-ocplib-simplex-devel -BuildRequires: ocaml-psmt2-frontend-devel +BuildRequires: ocaml-ocplib-simplex-devel >= 0.4 +BuildRequires: ocaml-odoc +BuildRequires: ocaml-psmt2-frontend-devel >= 0.2 +BuildRequires: ocaml-seq-devel BuildRequires: ocaml-zarith-devel BuildRequires: ocaml-zip-devel -Requires: ocaml-alt-ergo%{?_isa} = %{version}-%{release} - -# Do not Require private ocaml interfaces that we don't Provide -%global __requires_exclude ocamlx?\\\((Commands|Ex(ception|planation)|Formula|Hstring|Inequalities|L(iteral|oc)|Matching_types|Numbers(Interface)?|Options|P(arsed|olynome)|S(atml_types|ig|ymbols)|T(erm|y(ped)?)|U(f|til)|Vec)\\\) +Requires: ocaml-alt-ergo-parsers%{?_isa} = %{version}-%{release} %global _desc %{expand: Alt-Ergo is an automated theorem prover implemented in OCaml. It is @@ -64,18 +63,41 @@ Requires: hicolor-icon-theme This package contains a graphical front end for the Alt-Ergo theorem prover. -%package -n ocaml-alt-ergo +%package -n ocaml-alt-ergo-parsers +Summary: Parser library used by the Alt-Ergo SMT solver +Requires: ocaml-alt-ergo-lib%{?_isa} = %{version}-%{release} + +%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 +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 + +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 -%description -n ocaml-alt-ergo %_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-devel -Summary: Development files for ocaml-altergolib -Requires: ocaml-alt-ergo%{?_isa} = %{version}-%{release} +%package -n ocaml-alt-ergo-lib-devel +Summary: Development files for ocaml-alt-ergo-lib +Requires: ocaml-alt-ergo-lib%{?_isa} = %{version}-%{release} +Requires: ocaml-num-devel%{?_isa} +Requires: ocaml-ocplib-simplex-devel%{?_isa} +Requires: ocaml-seq-devel%{?_isa} +Requires: ocaml-zarith-devel%{?_isa} -%description -n ocaml-alt-ergo-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. @@ -85,33 +107,44 @@ that use the Alt-Ergo library. cp -p %{SOURCE2} com.ocamlpro.%{name}.desktop -# Look for zip instead of camlzip -sed -i 's/camlzip/zip/g' configure opam - -%ifarch %{arm} -# Work around for https://github.com/ocaml/ocaml/issues/7608 -# Remove this once a released ocaml version fixes that issue. -sed -i "s|^LIGHT_OFLAGS =|& -fno-thumb|" Makefile.users -%endif +# Unzip an example +cd examples/AB-Why3-plugin +unzip p4_34.why.zip +rm p4_34.why.zip +cd - %build -%configure --libdir=%{_libdir}/ocaml - -%ifnarch %{ocaml_native_compiler} -%global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLLEX=ocamllex -%else -%global opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt -%endif - -make %{opt_option} +# This is not an autoconf-generated script. Do NOT use %%configure. +./configure --prefix=%{_prefix} --libdir=%{_libdir}/ocaml --sharedir=%{_datadir} +%make_build +%make_build doc %install -mkdir -p %{buildroot}%{_bindir} -make %{opt_option} DESTDIR=%{buildroot} install +%make_install -# Move the gtksourceview file to the right place -mv %{buildroot}%{_datadir}/%{name}/gtksourceview-2.0 %{buildroot}%{_datadir} -rmdir %{buildroot}%{_datadir}/%{name} +# We do not want the dune markers +find _build/default/_doc/_html -name .dune-keep -delete + +# We do not want the ml files +find %{buildroot}%{_libdir}/ocaml -name \*.ml -delete + +# We install the documentation with the doc macro +rm -fr %{buildroot}%{_prefix}/doc + +# Install the man page +mkdir -p %{buildroot}%{_mandir}/man1 +cp -p doc/alt-ergo.1 %{buildroot}%{_mandir}/man1 + +# Make the plugins directory +mkdir -p %{buildroot}%{_libdir}/ocaml/%{name}/plugins + +# Install the preludes +cp -a preludes %{buildroot}%{_libdir}/ocaml/%{name} + +# Install the gtksourceview file +mkdir -p %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs +cp -p doc/gtk-lang/alt-ergo.lang \ + %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs # Install the desktop file mkdir -p %{buildroot}%{_datadir}/applications @@ -130,58 +163,71 @@ mkdir -p %{buildroot}%{_datadir}/icons cp -a icons %{buildroot}%{_datadir}/icons/hicolor %check -# Test alt-ergo on the examples. -%define altergo %{buildroot}%{_bindir}/alt-ergo -cd examples/valid -for fil in *.why; do - if ! %{altergo} $fil | grep -Fq Valid; then - echo $fil was not found valid - exit 1 - fi -done -cd ../invalid -for fil in *.why; do - if %{altergo} $fil | grep -Fq Valid; then - echo $fil was erroneously found valid - exit 1 - fi -done +dune runtest --profile release %files %doc README.md CHANGES examples %license COPYING.md LICENSE.md %{_bindir}/%{name} %{_mandir}/man1/alt-ergo.1.* +%{_libdir}/ocaml/%{name}/ %files gui %{_bindir}/altgr-ergo %{_datadir}/applications/com.ocamlpro.%{name}.desktop %{_datadir}/gtksourceview-2.0/language-specs/%{name}.lang %{_datadir}/icons/hicolor/*/apps/%{name}.png +%{_libdir}/ocaml/altgr-ergo/ %{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml -%files -n ocaml-alt-ergo -%dir %{_libdir}/ocaml/%{name}/ -%{_libdir}/ocaml/%{name}/META -%{_libdir}/ocaml/%{name}/plugins/ -%{_libdir}/ocaml/%{name}/preludes/ -%{_libdir}/ocaml/%{name}/altErgoLib.cma -%{_libdir}/ocaml/%{name}/altErgoLib.cmi +%files -n ocaml-%{name}-parsers +%dir %{_libdir}/ocaml/%{name}-parsers/ +%{_libdir}/ocaml/%{name}-parsers/META +%{_libdir}/ocaml/%{name}-parsers/*.cma +%{_libdir}/ocaml/%{name}-parsers/*.cmi %ifarch %{ocaml_native_compiler} -%{_libdir}/ocaml/%{name}/altErgoLib.cmxs +%{_libdir}/ocaml/%{name}-parsers/*.cmxs %endif -%files -n ocaml-%{name}-devel +%files -n ocaml-%{name}-parsers-devel +%{_libdir}/ocaml/%{name}-parsers/dune-package +%{_libdir}/ocaml/%{name}-parsers/opam %ifarch %{ocaml_native_compiler} -%{_libdir}/ocaml/%{name}/altErgoLib.a -%{_libdir}/ocaml/%{name}/altErgoLib.cmx -%{_libdir}/ocaml/%{name}/altErgoLib.cmxa +%{_libdir}/ocaml/%{name}-parsers/*.a +%{_libdir}/ocaml/%{name}-parsers/*.cmx +%{_libdir}/ocaml/%{name}-parsers/*.cmxa %endif -%{_libdir}/ocaml/%{name}/altErgoLib.o -%{_libdir}/ocaml/%{name}/altErgoLib.cmo -%{_libdir}/ocaml/%{name}/altErgoLib.cmt +%{_libdir}/ocaml/%{name}-parsers/*.mli +%{_libdir}/ocaml/%{name}-parsers/*.cmt +%{_libdir}/ocaml/%{name}-parsers/*.cmti + +%files -n ocaml-%{name}-lib +%dir %{_libdir}/ocaml/%{name}-lib/ +%{_libdir}/ocaml/%{name}-lib/META +%{_libdir}/ocaml/%{name}-lib/*.cma +%{_libdir}/ocaml/%{name}-lib/*.cmi +%ifarch %{ocaml_native_compiler} +%{_libdir}/ocaml/%{name}-lib/*.cmxs +%endif + +%files -n ocaml-%{name}-lib-devel +%doc _build/default/_doc/* +%{_libdir}/ocaml/%{name}-lib/dune-package +%{_libdir}/ocaml/%{name}-lib/opam +%ifarch %{ocaml_native_compiler} +%{_libdir}/ocaml/%{name}-lib/*.a +%{_libdir}/ocaml/%{name}-lib/*.cmx +%{_libdir}/ocaml/%{name}-lib/*.cmxa +%endif +%{_libdir}/ocaml/%{name}-lib/*.mli +%{_libdir}/ocaml/%{name}-lib/*.cmt +%{_libdir}/ocaml/%{name}-lib/*.cmti %changelog +* Mon Dec 27 2021 Jerry James - 2.3.0-1 +- Version 2.3.0 +- New ocaml-alt-ergo-lib and ocaml-alt-ergo-parsers subpackages + * Tue Oct 05 2021 Richard W.M. Jones - 2.2.0-14 - OCaml 4.13.1 build diff --git a/sources b/sources index 8679a4d..f5aec05 100644 --- a/sources +++ b/sources @@ -1,2 +1,2 @@ -SHA512 (alt-ergo-2.2.0.tar.gz) = 08ac8250ef2b853edc4885038ffbc8a5b4bbbedd170812fda3a4c4e59609f9642ae995d3a75ed637fbabb1163c6e84afa61c41204d41ba4b1377b3b84cc01eb8 +SHA512 (alt-ergo-2.3.0.tar.gz) = a2f209b62b8494bfefe84328cdc786185e0534c5e224e212b83045b078352a51d2ab02622f72c22c74c7de95c7a554cbdae2a9a8a0c41f3f26c841f8c72f6b21 SHA512 (alt-ergo-icons.tar.xz) = cb2e93bab3359f6f198e80e3e68840ed4b25a213b61f388a2de8abc299fd3c89240f64f610290ac89e6005088c484b2718a68ec18063076f73d7871a38ee038f From 9cf9f87095d23cc63b2bca2622aab7997657d789 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Wed, 19 Jan 2022 21:10:09 +0000 Subject: [PATCH 37/77] - Rebuilt for https://fedoraproject.org/wiki/Fedora_36_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 b1b8edf..b968115 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,7 +8,7 @@ Name: alt-ergo Version: 2.3.0 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -224,6 +224,9 @@ dune runtest --profile release %{_libdir}/ocaml/%{name}-lib/*.cmti %changelog +* Wed Jan 19 2022 Fedora Release Engineering - 2.3.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild + * Mon Dec 27 2021 Jerry James - 2.3.0-1 - Version 2.3.0 - New ocaml-alt-ergo-lib and ocaml-alt-ergo-parsers subpackages From 4817f805f6023dcf39594ff9f683aa851ffa5f77 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Fri, 4 Feb 2022 20:19:28 +0000 Subject: [PATCH 38/77] OCaml 4.13.1 rebuild to remove package notes --- alt-ergo.spec | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index b968115..5cecc07 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -1,3 +1,4 @@ +%undefine _package_note_flags # 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. @@ -8,7 +9,7 @@ Name: alt-ergo Version: 2.3.0 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -224,6 +225,9 @@ dune runtest --profile release %{_libdir}/ocaml/%{name}-lib/*.cmti %changelog +* Fri Feb 04 2022 Richard W.M. Jones - 2.3.0-3 +- OCaml 4.13.1 rebuild to remove package notes + * Wed Jan 19 2022 Fedora Release Engineering - 2.3.0-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild From 20c71462b63c4a182e78e2f69bc076f4f83c53e3 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 28 Feb 2022 12:02:56 -0700 Subject: [PATCH 39/77] Switch to the correct tarball. - Drop unneeded ocaml-findlib BR. - Add dependency on ocaml-alt-ergo-parsers from ocaml-alt-ergo-parsers-devel. --- alt-ergo-pervasives.patch | 104 ++++++++++++++++++++-------------- alt-ergo-psmt2-frontend.patch | 4 +- alt-ergo.rpmlintrc | 14 ----- alt-ergo.spec | 29 +++++++--- sources | 2 +- 5 files changed, 83 insertions(+), 70 deletions(-) delete mode 100644 alt-ergo.rpmlintrc diff --git a/alt-ergo-pervasives.patch b/alt-ergo-pervasives.patch index 23ad048..4c0a255 100644 --- a/alt-ergo-pervasives.patch +++ b/alt-ergo-pervasives.patch @@ -1,5 +1,21 @@ ---- alt-ergo-2.3.0/lib/frontend/typechecker.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/frontend/typechecker.ml 2021-12-13 11:22:42.669959468 -0700 +--- alt-ergo-2.3.0-free/extra/ocpChecker.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/extra/ocpChecker.ml 2022-02-23 12:58:05.976390283 -0700 +@@ -45,10 +45,10 @@ let update_file file lines = + exit 2 + in + Queue.iter (fun line -> +- Pervasives.output_string cout line; +- Pervasives.output_string cout "\n" ++ Stdlib.output_string cout line; ++ Stdlib.output_string cout "\n" + )lines; +- Pervasives.flush cout; ++ Stdlib.flush cout; + close_out cout + + +--- alt-ergo-2.3.0-free/sources/lib/frontend/typechecker.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/frontend/typechecker.ml 2022-02-23 12:57:12.849376944 -0700 @@ -37,7 +37,7 @@ module S = Set.Make(String) module HSS = Hstring.Set @@ -36,8 +52,8 @@ equal_pp_vars l vars -> ty | _ -> try ---- alt-ergo-2.3.0/lib/reasoners/fun_sat.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/reasoners/fun_sat.ml 2021-12-13 11:17:14.158193751 -0700 +--- alt-ergo-2.3.0-free/sources/lib/reasoners/fun_sat.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/reasoners/fun_sat.ml 2022-02-23 12:57:12.849376944 -0700 @@ -75,7 +75,7 @@ module Make (Th : Theory.S) : Sat_solver SE.fold (fun f mp -> @@ -68,8 +84,8 @@ begin Options.Time.unset_timeout ~is_gui:(Options.get_is_gui()); Options.Time.set_timeout ---- alt-ergo-2.3.0/lib/reasoners/ite_rel.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/reasoners/ite_rel.ml 2021-12-13 11:18:06.781156246 -0700 +--- alt-ergo-2.3.0-free/sources/lib/reasoners/ite_rel.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/reasoners/ite_rel.ml 2022-02-23 12:57:12.850376945 -0700 @@ -32,7 +32,7 @@ module TB = type t = E.t * bool let compare (a1, b1) (a2, b2) = @@ -79,8 +95,8 @@ end) type t = ---- alt-ergo-2.3.0/lib/reasoners/satml_frontend.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/reasoners/satml_frontend.ml 2021-12-13 11:17:48.709169125 -0700 +--- alt-ergo-2.3.0-free/sources/lib/reasoners/satml_frontend.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/reasoners/satml_frontend.ml 2022-02-23 12:57:12.850376945 -0700 @@ -508,7 +508,7 @@ module Make (Th : Theory.S) : Sat_solver if res <> 0 then res else @@ -117,8 +133,8 @@ let max_t = ME.fold (fun f _ mx -> aux mx f) env.gamma 0 in ME.fold (fun _ ({ E.ff = f; _ }, _) mx -> aux mx f) env.ground_preds max_t ---- alt-ergo-2.3.0/lib/reasoners/satml.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/reasoners/satml.ml 2021-12-13 11:18:53.173123173 -0700 +--- alt-ergo-2.3.0-free/sources/lib/reasoners/satml.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/reasoners/satml.ml 2022-02-23 12:57:12.850376945 -0700 @@ -361,7 +361,7 @@ module Make (Th : Theory.S) : SAT_ML wit *) @@ -146,8 +162,8 @@ for i = 0 to env.learnts.Vec.sz - 1 do (Vec.get env.learnts i).activity <- (Vec.get env.learnts i).activity *. 1e-20; ---- alt-ergo-2.3.0/lib/structures/expr.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/structures/expr.ml 2021-12-13 11:27:30.381754212 -0700 +--- alt-ergo-2.3.0-free/sources/lib/structures/expr.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/structures/expr.ml 2022-02-23 12:57:12.851376945 -0700 @@ -1031,7 +1031,7 @@ let mk_builtin ~is_pos n l = (** Substitutions *) @@ -214,8 +230,8 @@ if c <> 0 then c else Util.cmp_lists tl1 tl2 cmp_trig_term let unique_stable_sort = ---- alt-ergo-2.3.0/lib/structures/profiling.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/structures/profiling.ml 2021-12-13 11:28:14.180722957 -0700 +--- alt-ergo-2.3.0-free/sources/lib/structures/profiling.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/structures/profiling.ml 2022-02-23 12:57:12.851376945 -0700 @@ -85,7 +85,7 @@ let state = let set_sigprof () = let tm = @@ -238,8 +254,8 @@ else fprintf fmt "%0.3f" v let line_of_module arr f = ---- alt-ergo-2.3.0/lib/structures/symbols.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/structures/symbols.ml 2021-12-13 11:23:17.604934542 -0700 +--- alt-ergo-2.3.0-free/sources/lib/structures/symbols.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/structures/symbols.ml 2022-02-23 12:57:12.851376945 -0700 @@ -124,7 +124,7 @@ let compare_operators op1 op2 = (function | Access h1, Access h2 | Constr h1, Constr h2 -> Hstring.compare h1 h2 @@ -271,8 +287,8 @@ if c <> 0 then c else compare_bounds_kind a.kind b.kind ---- alt-ergo-2.3.0/lib/structures/ty.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/structures/ty.ml 2021-12-13 11:23:47.596913146 -0700 +--- alt-ergo-2.3.0-free/sources/lib/structures/ty.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/structures/ty.ml 2022-02-23 12:57:12.852376945 -0700 @@ -201,7 +201,7 @@ and shorten_body _ _ = let rec compare t1 t2 = @@ -316,8 +332,8 @@ module Set = Set.Make(struct ---- alt-ergo-2.3.0/lib/structures/typed.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/structures/typed.ml 2021-12-13 11:28:32.876709614 -0700 +--- alt-ergo-2.3.0-free/sources/lib/structures/typed.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/structures/typed.ml 2022-02-23 12:57:12.852376945 -0700 @@ -369,8 +369,8 @@ let fresh_hypothesis_name = | _ -> "@L"^(string_of_int !cpt) @@ -329,8 +345,8 @@ - try Pervasives.(=) (String.sub s 0 2) "@H" with Invalid_argument _ -> false + try Stdlib.(=) (String.sub s 0 2) "@H" with Invalid_argument _ -> false ---- alt-ergo-2.3.0/lib/structures/xliteral.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/structures/xliteral.ml 2021-12-13 11:27:49.604740495 -0700 +--- alt-ergo-2.3.0-free/sources/lib/structures/xliteral.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/structures/xliteral.ml 2022-02-23 12:57:12.852376945 -0700 @@ -103,7 +103,7 @@ module Make (X : OrderedType) : S with t type t = { at : atom; neg : bool; tpos : int; tneg : int } @@ -340,8 +356,8 @@ let equal a1 a2 = a1.tpos = a2.tpos (* XXX == *) let hash a1 = a1.tpos let uid a1 = a1.tpos ---- alt-ergo-2.3.0/lib/util/emap.mli.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/util/emap.mli 2021-12-13 11:20:53.277037515 -0700 +--- alt-ergo-2.3.0-free/sources/lib/util/emap.mli.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/util/emap.mli 2022-02-23 12:57:12.852376945 -0700 @@ -41,8 +41,8 @@ struct type t = int * int @@ -362,8 +378,8 @@ end (** Input signature of the functor {!Map.Make}. *) ---- alt-ergo-2.3.0/lib/util/myUnix.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/util/myUnix.ml 2021-12-13 11:19:46.141085403 -0700 +--- alt-ergo-2.3.0-free/sources/lib/util/myUnix.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/util/myUnix.ml 2022-02-23 12:57:12.852376945 -0700 @@ -18,7 +18,7 @@ module Default_Unix = struct let cur_time () = (times()).tms_utime @@ -373,8 +389,8 @@ let itimer = if is_gui then Unix.ITIMER_REAL (* troubles with VIRTUAL *) else Unix.ITIMER_VIRTUAL ---- alt-ergo-2.3.0/lib/util/numbers.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/util/numbers.ml 2021-12-13 11:22:11.316981841 -0700 +--- alt-ergo-2.3.0-free/sources/lib/util/numbers.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/util/numbers.ml 2022-02-23 12:57:12.853376946 -0700 @@ -48,8 +48,8 @@ module Q = struct else let v = to_float q in @@ -386,8 +402,8 @@ else v in let flt = if n = 2 then sqrt w else w ** (1. /. float n) in ---- alt-ergo-2.3.0/lib/util/options.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/util/options.ml 2021-12-13 11:21:27.477013115 -0700 +--- alt-ergo-2.3.0-free/sources/lib/util/options.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/util/options.ml 2022-02-23 12:57:12.853376946 -0700 @@ -957,7 +957,7 @@ let (>) (a: int) (b: int) = a > b let (<=) (a: int) (b: int) = a <= b let (>=) (a: int) (b: int) = a >= b @@ -397,8 +413,8 @@ (* extra **) ---- alt-ergo-2.3.0/lib/util/util.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/util/util.ml 2021-12-13 11:20:25.717057175 -0700 +--- alt-ergo-2.3.0-free/sources/lib/util/util.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/util/util.ml 2022-02-23 12:57:12.853376946 -0700 @@ -83,7 +83,7 @@ let [@inline always] compare_algebraic s let r1 = Obj.repr s1 in let r2 = Obj.repr s2 in @@ -408,8 +424,8 @@ | true, false -> -1 | false, true -> 1 | false, false -> ---- alt-ergo-2.3.0/lib/util/util.mli.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/util/util.mli 2021-12-13 11:20:10.341068143 -0700 +--- alt-ergo-2.3.0-free/sources/lib/util/util.mli.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/util/util.mli 2022-02-23 12:57:12.853376946 -0700 @@ -56,7 +56,7 @@ val string_of_th_ext : theories_extensio (** generic function for comparing algebraic data types. @@ -419,8 +435,8 @@ *) val [@inline always] compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int ---- alt-ergo-2.3.0/lib/util/zarithNumbers.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/lib/util/zarithNumbers.ml 2021-12-13 11:19:11.821109879 -0700 +--- alt-ergo-2.3.0-free/sources/lib/util/zarithNumbers.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/util/zarithNumbers.ml 2022-02-23 12:57:12.853376946 -0700 @@ -153,7 +153,7 @@ module Q : NumbersInterface.QSig with mo let floor t = from_z (Z.fdiv (num t) (den t)) let ceiling t = from_z (Z.cdiv (num t) (den t)) @@ -430,8 +446,8 @@ let num_pow = Z.power (num t) abs_n in let den_pow = Z.power (den t) abs_n in if n >= 0 then from_zz num_pow den_pow else from_zz den_pow num_pow ---- alt-ergo-2.3.0/parsers/parsers.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/parsers/parsers.ml 2021-12-13 11:16:42.461216342 -0700 +--- alt-ergo-2.3.0-free/sources/parsers/parsers.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/parsers/parsers.ml 2022-02-23 12:57:12.853376946 -0700 @@ -124,7 +124,7 @@ let parse_input_file file = stdin, Lexing.from_string file_content, false, ext else @@ -441,8 +457,8 @@ let cin = open_in file in cin, Lexing.from_channel cin, true, ext else ---- alt-ergo-2.3.0/tools/gui/annoted_ast.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/tools/gui/annoted_ast.ml 2021-12-13 11:15:02.334287694 -0700 +--- alt-ergo-2.3.0-free/sources/tools/gui/annoted_ast.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/tools/gui/annoted_ast.ml 2022-02-23 12:57:12.854376946 -0700 @@ -191,7 +191,7 @@ type annoted_node = module MDep = Map.Make ( struct @@ -492,8 +508,8 @@ )sl l in findtags_aform sl aaf.c acc ---- alt-ergo-2.3.0/tools/gui/connected_ast.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/tools/gui/connected_ast.ml 2021-12-13 11:16:16.069235150 -0700 +--- alt-ergo-2.3.0-free/sources/tools/gui/connected_ast.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/tools/gui/connected_ast.ml 2022-02-23 12:57:12.854376946 -0700 @@ -388,7 +388,7 @@ let rec unquantify_aform (buffer:sbuffer List.fold_left (fun (nbv, used, goal_used, ve, uplet, lets) v -> let ((s, _) as v'), e = List.hd ve in @@ -521,8 +537,8 @@ commit_tags_buffer sbuf | _ -> assert false end ---- alt-ergo-2.3.0/tools/gui/main_gui.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/tools/gui/main_gui.ml 2021-12-13 11:15:49.445254125 -0700 +--- alt-ergo-2.3.0-free/sources/tools/gui/main_gui.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/tools/gui/main_gui.ml 2022-02-23 12:57:12.854376946 -0700 @@ -151,7 +151,7 @@ let save_session envs = let save_dialog cancel envs () = diff --git a/alt-ergo-psmt2-frontend.patch b/alt-ergo-psmt2-frontend.patch index 1c58d9e..caa9af7 100644 --- a/alt-ergo-psmt2-frontend.patch +++ b/alt-ergo-psmt2-frontend.patch @@ -1,5 +1,5 @@ ---- alt-ergo-2.3.0/parsers/psmt2_to_alt_ergo.ml.orig 2019-02-11 09:43:50.000000000 -0700 -+++ alt-ergo-2.3.0/parsers/psmt2_to_alt_ergo.ml 2021-12-13 13:45:45.216802816 -0700 +--- alt-ergo-2.3.0-free/sources/parsers/psmt2_to_alt_ergo.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/parsers/psmt2_to_alt_ergo.ml 2022-02-23 12:59:13.497394356 -0700 @@ -403,6 +403,9 @@ module Translate = struct | Cmd_Push _ -> not_supported "push"; assert false | Cmd_Pop _ -> not_supported "pop"; assert false diff --git a/alt-ergo.rpmlintrc b/alt-ergo.rpmlintrc deleted file mode 100644 index 7a6e1a4..0000000 --- a/alt-ergo.rpmlintrc +++ /dev/null @@ -1,14 +0,0 @@ -# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON -# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors - -# The dictionary lacks some technical words -addFilter(r'W: spelling-error .* (arithmetics|equational|instantiation|parameterized|prover)') - -# Caused by ocaml; this package cannot fix it -addFilter(r'alt-ergo(-gui)?\.[^:]+: E: missing-call-to-chdir-with-chroot') - -# Documentation is in the main package -addFilter(r'alt-ergo-gui\.[^:]+: W: no-documentation') - -# There is no man page for the graphical launcher -addFilter(r'alt-ergo-gui\.[^:]+: W: no-manual-page-for-binary altgr-ergo') diff --git a/alt-ergo.spec b/alt-ergo.spec index 5cecc07..0c15271 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -1,20 +1,21 @@ -%undefine _package_note_flags # 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 Name: alt-ergo Version: 2.3.0 -Release: 3%{?dist} +Release: 4%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 URL: https://alt-ergo.ocamlpro.com/ -Source0: https://alt-ergo.ocamlpro.com/http/%{name}-%{version}/%{name}-%{version}.tar.gz +Source0: https://alt-ergo.ocamlpro.com/http/%{name}-free-%{version}/%{name}-free-%{version}.tar.gz # Created with gimp from official upstream icon Source1: %{name}-icons.tar.xz Source2: %{name}.desktop @@ -30,7 +31,6 @@ BuildRequires: gtksourceview2-devel BuildRequires: make BuildRequires: ocaml >= 4.04.0 BuildRequires: ocaml-dune -BuildRequires: ocaml-findlib BuildRequires: ocaml-lablgtk-devel BuildRequires: ocaml-menhir BuildRequires: ocaml-num-devel @@ -74,6 +74,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 +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} @@ -104,8 +105,9 @@ This package contains development files needed to build applications that use the Alt-Ergo library. %prep -%autosetup -p1 -a 1 +%autosetup -n %{name}-%{version}-free -p1 -a 1 +cd sources cp -p %{SOURCE2} com.ocamlpro.%{name}.desktop # Unzip an example @@ -116,11 +118,13 @@ cd - %build # This is not an autoconf-generated script. Do NOT use %%configure. +cd sources ./configure --prefix=%{_prefix} --libdir=%{_libdir}/ocaml --sharedir=%{_datadir} %make_build %make_build doc %install +cd sources %make_install # We do not want the dune markers @@ -160,15 +164,17 @@ appstreamcli validate --no-net \ %{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml # Install the icons +cd - mkdir -p %{buildroot}%{_datadir}/icons cp -a icons %{buildroot}%{_datadir}/icons/hicolor %check -dune runtest --profile release +cd sources +dune runtest --release %files -%doc README.md CHANGES examples -%license COPYING.md LICENSE.md +%doc README.md sources/CHANGES sources/examples publications/*.pdf +%license COPYING.md LICENSE.md License.OCamlPro %{_bindir}/%{name} %{_mandir}/man1/alt-ergo.1.* %{_libdir}/ocaml/%{name}/ @@ -212,7 +218,7 @@ dune runtest --profile release %endif %files -n ocaml-%{name}-lib-devel -%doc _build/default/_doc/* +%doc sources/_build/default/_doc/* %{_libdir}/ocaml/%{name}-lib/dune-package %{_libdir}/ocaml/%{name}-lib/opam %ifarch %{ocaml_native_compiler} @@ -225,6 +231,11 @@ dune runtest --profile release %{_libdir}/ocaml/%{name}-lib/*.cmti %changelog +* Mon Feb 28 2022 Jerry James - 2.3.0-4 +- Switch to the correct tarball +- Drop unneeded ocaml-findlib BR +- Add dependency on ocaml-alt-ergo-parsers from ocaml-alt-ergo-parsers-devel + * Fri Feb 04 2022 Richard W.M. Jones - 2.3.0-3 - OCaml 4.13.1 rebuild to remove package notes diff --git a/sources b/sources index f5aec05..56b9730 100644 --- a/sources +++ b/sources @@ -1,2 +1,2 @@ -SHA512 (alt-ergo-2.3.0.tar.gz) = a2f209b62b8494bfefe84328cdc786185e0534c5e224e212b83045b078352a51d2ab02622f72c22c74c7de95c7a554cbdae2a9a8a0c41f3f26c841f8c72f6b21 +SHA512 (alt-ergo-free-2.3.0.tar.gz) = e15efc6bbde59065c6ccaf1ef2f8158b8b9be4b00b2c2365e5eeb7d7114be72c47c813fc06880a6278edd7e288f24ef4588c88e0630d9bda9378a3eda3fd07ca SHA512 (alt-ergo-icons.tar.xz) = cb2e93bab3359f6f198e80e3e68840ed4b25a213b61f388a2de8abc299fd3c89240f64f610290ac89e6005088c484b2718a68ec18063076f73d7871a38ee038f From 5f6eee8592100c36eee8bbde19b5db0950ea3992 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Sun, 19 Jun 2022 13:28:13 +0100 Subject: [PATCH 40/77] OCaml 4.14.0 rebuild --- alt-ergo.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/alt-ergo.spec b/alt-ergo.spec index 0c15271..c1413a7 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -10,7 +10,7 @@ Name: alt-ergo Version: 2.3.0 -Release: 4%{?dist} +Release: 5%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -231,6 +231,9 @@ dune runtest --release %{_libdir}/ocaml/%{name}-lib/*.cmti %changelog +* Sun Jun 19 2022 Richard W.M. Jones - 2.3.0-5 +- OCaml 4.14.0 rebuild + * Mon Feb 28 2022 Jerry James - 2.3.0-4 - Switch to the correct tarball - Drop unneeded ocaml-findlib BR From cf26b7fc7efef5894e9e3b2814589a49147e7883 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 21 Jun 2022 09:01:13 -0600 Subject: [PATCH 41/77] Version 2.3.3. - Add -menhir patch to fix FTBFS. - Add -stdlib-shims patch since Fedora does not need stdlib-shims. --- alt-ergo-menhir.patch | 18 ++ alt-ergo-pervasives.patch | 455 +----------------------------------- alt-ergo-stdlib-shims.patch | 42 ++++ alt-ergo.spec | 61 +++-- sources | 1 + 5 files changed, 113 insertions(+), 464 deletions(-) create mode 100644 alt-ergo-menhir.patch create mode 100644 alt-ergo-stdlib-shims.patch diff --git a/alt-ergo-menhir.patch b/alt-ergo-menhir.patch new file mode 100644 index 0000000..4ab3e45 --- /dev/null +++ b/alt-ergo-menhir.patch @@ -0,0 +1,18 @@ +--- alt-ergo-2.3.0-free/sources/plugins/AB-Why3/dune.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/plugins/AB-Why3/dune 2022-06-20 13:27:36.662944620 -0600 +@@ -3,13 +3,13 @@ + + (menhir + (infer false) +- (flags --fixed-exception) ++ (flags --fixed-exception --table) + (modules why3_parser) + ) + + (library + (name ABWhy3Plugin) +- (libraries alt-ergo-lib alt-ergo-parsers) ++ (libraries alt-ergo-lib alt-ergo-parsers menhirLib) + (modules Why3_lexer Why3_parser Why3_loc Why3_ptree) + ) + diff --git a/alt-ergo-pervasives.patch b/alt-ergo-pervasives.patch index 4c0a255..bd72f54 100644 --- a/alt-ergo-pervasives.patch +++ b/alt-ergo-pervasives.patch @@ -14,451 +14,8 @@ close_out cout ---- alt-ergo-2.3.0-free/sources/lib/frontend/typechecker.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/frontend/typechecker.ml 2022-02-23 12:57:12.849376944 -0700 -@@ -37,7 +37,7 @@ module S = Set.Make(String) - module HSS = Hstring.Set - - module MString = -- Map.Make(struct type t = string let compare = Pervasives.compare end) -+ Map.Make(struct type t = string let compare = Stdlib.compare end) - - module Types = struct - -@@ -86,7 +86,7 @@ module Types = struct - List.for_all2 - (fun pp x -> - match pp with -- | PPTvarid (y, _) -> Pervasives.(=) x y -+ | PPTvarid (y, _) -> Stdlib.(=) x y - | _ -> false - ) lpp lvars - with Invalid_argument _ -> false -@@ -105,7 +105,7 @@ module Types = struct - to_tyvars := MString.add s nty !to_tyvars; - nty - end -- | PPTexternal (l, s, loc) when Pervasives.(=) s "farray" -> -+ | PPTexternal (l, s, loc) when Stdlib.(=) s "farray" -> - let t1,t2 = match l with - | [t2] -> PPTint,t2 - | [t1;t2] -> t1,t2 -@@ -116,7 +116,7 @@ module Types = struct - | PPTexternal (l, s, loc) -> - begin - match rectype with -- | Some (id, vars, ty) when Pervasives.(=) s id && -+ | Some (id, vars, ty) when Stdlib.(=) s id && - equal_pp_vars l vars -> ty - | _ -> - try ---- alt-ergo-2.3.0-free/sources/lib/reasoners/fun_sat.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/reasoners/fun_sat.ml 2022-02-23 12:57:12.849376944 -0700 -@@ -75,7 +75,7 @@ module Make (Th : Theory.S) : Sat_solver - SE.fold - (fun f mp -> - let w = var_inc +. try ME.find f mp with Not_found -> 0. in -- stable := !stable && Pervasives.(<=) w 1e100; -+ stable := !stable && Stdlib.(<=) w 1e100; - ME.add f w mp - )(Ex.bj_formulas_of expl) mp - in -@@ -118,9 +118,9 @@ module Make (Th : Theory.S) : Sat_solver - let dec = - List.fast_sort - (fun (_, x1, b1) (_, x2, b2) -> -- let c = Pervasives.compare b2 b1 in -+ let c = Stdlib.compare b2 b1 in - if c <> 0 then c -- else Pervasives.compare x2 x1 -+ else Stdlib.compare x2 x1 - )dec - in - (* -@@ -1171,7 +1171,7 @@ module Make (Th : Theory.S) : Sat_solver - let i = abs (interpretation ()) in - assert (i = 1 || i = 2 || i = 3); - if not !(env.model_gen_mode) && -- Pervasives.(<>) (Options.interpretation_timelimit ()) 0. then -+ Stdlib.(<>) (Options.interpretation_timelimit ()) 0. then - begin - Options.Time.unset_timeout ~is_gui:(Options.get_is_gui()); - Options.Time.set_timeout ---- alt-ergo-2.3.0-free/sources/lib/reasoners/ite_rel.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/reasoners/ite_rel.ml 2022-02-23 12:57:12.850376945 -0700 -@@ -32,7 +32,7 @@ module TB = - type t = E.t * bool - let compare (a1, b1) (a2, b2) = - let c = E.compare a1 a2 in -- if c <> 0 then c else Pervasives.compare b1 b2 -+ if c <> 0 then c else Stdlib.compare b1 b2 - end) - - type t = ---- alt-ergo-2.3.0-free/sources/lib/reasoners/satml_frontend.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/reasoners/satml_frontend.ml 2022-02-23 12:57:12.850376945 -0700 -@@ -508,7 +508,7 @@ module Make (Th : Theory.S) : Sat_solver - if res <> 0 then res - else - (* higher weight is better hence compare w2 w1 *) -- let res = Pervasives.compare w2 w1 in -+ let res = Stdlib.compare w2 w1 in - if res <> 0 then res - else - (* lower index is better *) -@@ -844,7 +844,7 @@ module Make (Th : Theory.S) : Sat_solver - } - - let normal_mconf () = -- {Util.nb_triggers = Pervasives.max 2 (nb_triggers () * 2); -+ {Util.nb_triggers = Stdlib.max 2 (nb_triggers () * 2); - no_ematching = no_Ematching(); - triggers_var = triggers_var (); - use_cs = false; -@@ -853,7 +853,7 @@ module Make (Th : Theory.S) : Sat_solver - } - - let greedy_mconf () = -- {Util.nb_triggers = Pervasives.max 10 (nb_triggers () * 10); -+ {Util.nb_triggers = Stdlib.max 10 (nb_triggers () * 10); - no_ematching = false; - triggers_var = true; - use_cs = true; -@@ -951,7 +951,7 @@ module Make (Th : Theory.S) : Sat_solver - - (* copied from sat_solvers.ml *) - let max_term_depth_in_sat env = -- let aux mx f = Pervasives.max mx (E.depth f) in -+ let aux mx f = Stdlib.max mx (E.depth f) in - let max_t = ME.fold (fun f _ mx -> aux mx f) env.gamma 0 in - ME.fold (fun _ ({ E.ff = f; _ }, _) mx -> aux mx f) env.ground_preds max_t - ---- alt-ergo-2.3.0-free/sources/lib/reasoners/satml.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/reasoners/satml.ml 2022-02-23 12:57:12.850376945 -0700 -@@ -361,7 +361,7 @@ module Make (Th : Theory.S) : SAT_ML wit - *) - - let f_weight env i j = -- Pervasives.(<) (Vec.get env.vars j).weight (Vec.get env.vars i).weight -+ Stdlib.(<) (Vec.get env.vars j).weight (Vec.get env.vars i).weight - - (* unused -- let f_filter env i = (Vec.get env.vars i).level < 0 *) - -@@ -375,7 +375,7 @@ module Make (Th : Theory.S) : SAT_ML wit - - let var_bump_activity env v = - v.weight <- v.weight +. env.var_inc; -- if Pervasives.(>) v.weight 1e100 then begin -+ if Stdlib.(>) v.weight 1e100 then begin - for i = 0 to env.vars.Vec.sz - 1 do - (Vec.get env.vars i).weight <- (Vec.get env.vars i).weight *. 1e-100 - done; -@@ -387,7 +387,7 @@ module Make (Th : Theory.S) : SAT_ML wit - - let clause_bump_activity env c = - c.activity <- c.activity +. env.clause_inc; -- if Pervasives.(>) c.activity 1e20 then begin -+ if Stdlib.(>) c.activity 1e20 then begin - for i = 0 to env.learnts.Vec.sz - 1 do - (Vec.get env.learnts i).activity <- - (Vec.get env.learnts i).activity *. 1e-20; ---- alt-ergo-2.3.0-free/sources/lib/structures/expr.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/structures/expr.ml 2022-02-23 12:57:12.851376945 -0700 -@@ -1031,7 +1031,7 @@ let mk_builtin ~is_pos n l = - (** Substitutions *) - - let is_skolem_cst v = -- try Pervasives.(=) (String.sub (Sy.to_string v.f) 0 4) "_sko" -+ try Stdlib.(=) (String.sub (Sy.to_string v.f) 0 4) "_sko" - with Invalid_argument _ -> false - - let get_skolem = -@@ -1669,9 +1669,9 @@ module Triggers = struct - | { f = (Name _) as s1; xs=tl1; _ }, { f = (Name _) as s2; xs=tl2; _ } -> - let l1 = List.map score_term tl1 in - let l2 = List.map score_term tl2 in -- let l1 = List.fast_sort Pervasives.compare l1 in -- let l2 = List.fast_sort Pervasives.compare l2 in -- let c = Util.cmp_lists l1 l2 Pervasives.compare in -+ let l1 = List.fast_sort Stdlib.compare l1 in -+ let l2 = List.fast_sort Stdlib.compare l2 in -+ let c = Util.cmp_lists l1 l2 Stdlib.compare in - if c <> 0 then c - else - let c = Sy.compare s1 s2 in -@@ -1702,7 +1702,7 @@ module Triggers = struct - - | { f = Op (Access a1) ; xs=[t1]; _ }, - { f = Op (Access a2) ; xs=[t2]; _ } -> -- let c = Pervasives.compare a1 a2 in (* should be Hstring.compare *) -+ let c = Stdlib.compare a1 a2 in (* should be Hstring.compare *) - if c<>0 then c else cmp_trig_term t1 t2 - - | { f = Op (Access _); _ }, _ -> -1 -@@ -1710,7 +1710,7 @@ module Triggers = struct - - | { f = Op (Destruct (_,a1)) ; xs = [t1]; _ }, - { f = Op (Destruct (_,a2)) ; xs = [t2]; _ } -> -- let c = Pervasives.compare a1 a2 in (* should be Hstring.compare *) -+ let c = Stdlib.compare a1 a2 in (* should be Hstring.compare *) - if c<>0 then c else cmp_trig_term t1 t2 - - | { f = Op (Destruct _); _ }, _ -> -1 -@@ -1725,9 +1725,9 @@ module Triggers = struct - (* ops that are not infix or prefix *) - let l1 = List.map score_term tl1 in - let l2 = List.map score_term tl2 in -- let l1 = List.fast_sort Pervasives.compare l1 in -- let l2 = List.fast_sort Pervasives.compare l2 in -- let c = Util.cmp_lists l1 l2 Pervasives.compare in -+ let l1 = List.fast_sort Stdlib.compare l1 in -+ let l2 = List.fast_sort Stdlib.compare l2 in -+ let c = Util.cmp_lists l1 l2 Stdlib.compare in - if c <> 0 then c - else - let c = Sy.compare s1 s2 in -@@ -1741,9 +1741,9 @@ module Triggers = struct - let cmp_trig_term_list tl2 tl1 = - let l1 = List.map score_term tl1 in - let l2 = List.map score_term tl2 in -- let l1 = List.rev (List.fast_sort Pervasives.compare l1) in -- let l2 = List.rev (List.fast_sort Pervasives.compare l2) in -- let c = Util.cmp_lists l1 l2 Pervasives.compare in -+ let l1 = List.rev (List.fast_sort Stdlib.compare l1) in -+ let l2 = List.rev (List.fast_sort Stdlib.compare l2) in -+ let c = Util.cmp_lists l1 l2 Stdlib.compare in - if c <> 0 then c else Util.cmp_lists tl1 tl2 cmp_trig_term - - let unique_stable_sort = ---- alt-ergo-2.3.0-free/sources/lib/structures/profiling.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/structures/profiling.ml 2022-02-23 12:57:12.851376945 -0700 -@@ -85,7 +85,7 @@ let state = - let set_sigprof () = - let tm = - let v = Options.profiling_period () in -- if Pervasives.(>) v 0. then v else -. v -+ if Stdlib.(>) v 0. then v else -. v - in - ignore - (Unix.setitimer Unix.ITIMER_PROF -@@ -629,9 +629,9 @@ let switch () = - - - let float_print fmt v = -- if Pervasives.(=) v 0. then fprintf fmt "-- " -- else if Pervasives.(<) v 10. then fprintf fmt "%0.5f" v -- else if Pervasives.(<) v 100. then fprintf fmt "%0.4f" v -+ if Stdlib.(=) v 0. then fprintf fmt "-- " -+ else if Stdlib.(<) v 10. then fprintf fmt "%0.5f" v -+ else if Stdlib.(<) v 100. then fprintf fmt "%0.4f" v - else fprintf fmt "%0.3f" v - - let line_of_module arr f = ---- alt-ergo-2.3.0-free/sources/lib/structures/symbols.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/structures/symbols.ml 2022-02-23 12:57:12.851376945 -0700 -@@ -124,7 +124,7 @@ let compare_operators op1 op2 = - (function - | Access h1, Access h2 | Constr h1, Constr h2 -> Hstring.compare h1 h2 - | Destruct (h1, b1), Destruct(h2, b2) -> -- let c = Pervasives.compare b1 b2 in -+ let c = Stdlib.compare b1 b2 in - if c <> 0 then c else Hstring.compare h1 h2 - | _ , (Plus | Minus | Mult | Div | Modulo - | Concat | Extract | Get | Set | Fixed | Float | Reach -@@ -155,7 +155,7 @@ let compare_forms f1 f2 = - Util.compare_algebraic f1 f2 - (function - | F_Unit b1, F_Unit b2 -- | F_Clause b1, F_Clause b2 -> Pervasives.compare b1 b2 -+ | F_Clause b1, F_Clause b2 -> Stdlib.compare b1 b2 - | _, (F_Unit _ | F_Clause _ | F_Lemma | F_Skolem - | F_Iff | F_Xor) -> - assert false -@@ -173,10 +173,10 @@ let compare_bounds a b = - let c = Ty.compare a.sort b.sort in - if c <> 0 then c - else -- let c = Pervasives.compare a.is_open b.is_open in -+ let c = Stdlib.compare a.is_open b.is_open in - if c <> 0 then c - else -- let c = Pervasives.compare a.is_lower b.is_lower in -+ let c = Stdlib.compare a.is_lower b.is_lower in - if c <> 0 then c - else compare_bounds_kind a.kind b.kind - ---- alt-ergo-2.3.0-free/sources/lib/structures/ty.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/structures/ty.ml 2022-02-23 12:57:12.852376945 -0700 -@@ -201,7 +201,7 @@ and shorten_body _ _ = - - let rec compare t1 t2 = - match shorten t1 , shorten t2 with -- | Tvar{ v = v1; _ } , Tvar{ v = v2; _ } -> Pervasives.compare v1 v2 -+ | Tvar{ v = v1; _ } , Tvar{ v = v2; _ } -> Stdlib.compare v1 v2 - | Tvar _, _ -> -1 | _ , Tvar _ -> 1 - | Text(l1, s1) , Text(l2, s2) -> - let c = Hstring.compare s1 s2 in -@@ -234,7 +234,7 @@ let rec compare t1 t2 = - - | Tadt _, _ -> -1 | _ , Tadt _ -> 1 - -- | t1 , t2 -> Pervasives.compare t1 t2 -+ | t1 , t2 -> Stdlib.compare t1 t2 - - - and compare_list l1 l2 = match l1, l2 with -@@ -278,7 +278,7 @@ let rec equal t1 t2 = - | _ -> false - - (*** matching with a substitution mechanism ***) --module M = Map.Make(struct type t=int let compare = Pervasives.compare end) -+module M = Map.Make(struct type t=int let compare = Stdlib.compare end) - type subst = t M.t - - let esubst = M.empty -@@ -602,12 +602,12 @@ let instantiate lvar lty ty = - let union_subst s1 s2 = - M.fold (fun k x s2 -> M.add k x s2) (M.map (apply_subst s2) s1) s2 - --let compare_subst = M.compare Pervasives.compare -+let compare_subst = M.compare Stdlib.compare - --let equal_subst = M.equal Pervasives.(=) -+let equal_subst = M.equal Stdlib.(=) - - module Svty = -- Set.Make(struct type t = int let compare = Pervasives.compare end) -+ Set.Make(struct type t = int let compare = Stdlib.compare end) - - module Set = - Set.Make(struct ---- alt-ergo-2.3.0-free/sources/lib/structures/typed.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/structures/typed.ml 2022-02-23 12:57:12.852376945 -0700 -@@ -369,8 +369,8 @@ let fresh_hypothesis_name = - | _ -> "@L"^(string_of_int !cpt) - - let is_local_hyp s = -- try Pervasives.(=) (String.sub s 0 2) "@L" with Invalid_argument _ -> false -+ try Stdlib.(=) (String.sub s 0 2) "@L" with Invalid_argument _ -> false - - let is_global_hyp s = -- try Pervasives.(=) (String.sub s 0 2) "@H" with Invalid_argument _ -> false -+ try Stdlib.(=) (String.sub s 0 2) "@H" with Invalid_argument _ -> false - ---- alt-ergo-2.3.0-free/sources/lib/structures/xliteral.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/structures/xliteral.ml 2022-02-23 12:57:12.852376945 -0700 -@@ -103,7 +103,7 @@ module Make (X : OrderedType) : S with t - - type t = { at : atom; neg : bool; tpos : int; tneg : int } - -- let compare a1 a2 = Pervasives.compare a1.tpos a2.tpos -+ let compare a1 a2 = Stdlib.compare a1.tpos a2.tpos - let equal a1 a2 = a1.tpos = a2.tpos (* XXX == *) - let hash a1 = a1.tpos - let uid a1 = a1.tpos ---- alt-ergo-2.3.0-free/sources/lib/util/emap.mli.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/emap.mli 2022-02-23 12:57:12.852376945 -0700 -@@ -41,8 +41,8 @@ - struct - type t = int * int - let compare (x0,y0) (x1,y1) = -- match Pervasives.compare x0 x1 with -- 0 -> Pervasives.compare y0 y1 -+ match Stdlib.compare x0 x1 with -+ 0 -> Stdlib.compare y0 y1 - | c -> c - end - -@@ -68,7 +68,7 @@ sig - [f e1 e2] is strictly negative if [e1] is smaller than [e2], - and [f e1 e2] is strictly positive if [e1] is greater than [e2]. - Example: a suitable ordering function is the generic structural -- comparison function {!Pervasives.compare}. *) -+ comparison function {!Stdlib.compare}. *) - end - (** Input signature of the functor {!Map.Make}. *) - ---- alt-ergo-2.3.0-free/sources/lib/util/myUnix.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/myUnix.ml 2022-02-23 12:57:12.852376945 -0700 -@@ -18,7 +18,7 @@ module Default_Unix = struct - let cur_time () = (times()).tms_utime - - let set_timeout ~is_gui timelimit = -- if Pervasives.(<>) timelimit 0. then -+ if Stdlib.(<>) timelimit 0. then - let itimer = - if is_gui then Unix.ITIMER_REAL (* troubles with VIRTUAL *) - else Unix.ITIMER_VIRTUAL ---- alt-ergo-2.3.0-free/sources/lib/util/numbers.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/numbers.ml 2022-02-23 12:57:12.853376946 -0700 -@@ -48,8 +48,8 @@ module Q = struct - else - let v = to_float q in - let w = -- if Pervasives.(<) v min_float then min_float -- else if Pervasives.(>) v max_float then max_float -+ if Stdlib.(<) v min_float then min_float -+ else if Stdlib.(>) v max_float then max_float - else v - in - let flt = if n = 2 then sqrt w else w ** (1. /. float n) in ---- alt-ergo-2.3.0-free/sources/lib/util/options.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/options.ml 2022-02-23 12:57:12.853376946 -0700 -@@ -957,7 +957,7 @@ let (>) (a: int) (b: int) = a > b - let (<=) (a: int) (b: int) = a <= b - let (>=) (a: int) (b: int) = a >= b - --let compare (a: int) (b: int) = Pervasives.compare a b -+let compare (a: int) (b: int) = Stdlib.compare a b - - - (* extra **) ---- alt-ergo-2.3.0-free/sources/lib/util/util.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/util.ml 2022-02-23 12:57:12.853376946 -0700 -@@ -83,7 +83,7 @@ let [@inline always] compare_algebraic s - let r1 = Obj.repr s1 in - let r2 = Obj.repr s2 in - match Obj.is_int r1, Obj.is_int r2 with -- | true, true -> Pervasives.compare s1 s2 (* both constructors without args *) -+ | true, true -> Stdlib.compare s1 s2 (* both constructors without args *) - | true, false -> -1 - | false, true -> 1 - | false, false -> ---- alt-ergo-2.3.0-free/sources/lib/util/util.mli.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/util.mli 2022-02-23 12:57:12.853376946 -0700 -@@ -56,7 +56,7 @@ val string_of_th_ext : theories_extensio - (** - generic function for comparing algebraic data types. - [compare_algebraic a b f] -- - Pervasives.compare a b is used if -+ - Stdlib.compare a b is used if - - *) - val [@inline always] compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int ---- alt-ergo-2.3.0-free/sources/lib/util/zarithNumbers.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/util/zarithNumbers.ml 2022-02-23 12:57:12.853376946 -0700 -@@ -153,7 +153,7 @@ module Q : NumbersInterface.QSig with mo - let floor t = from_z (Z.fdiv (num t) (den t)) - let ceiling t = from_z (Z.cdiv (num t) (den t)) - let power t n = -- let abs_n = Pervasives.abs n in -+ let abs_n = Stdlib.abs n in - let num_pow = Z.power (num t) abs_n in - let den_pow = Z.power (den t) abs_n in - if n >= 0 then from_zz num_pow den_pow else from_zz den_pow num_pow ---- alt-ergo-2.3.0-free/sources/parsers/parsers.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/parsers/parsers.ml 2022-02-23 12:57:12.853376946 -0700 -@@ -124,7 +124,7 @@ let parse_input_file file = - stdin, Lexing.from_string file_content, false, ext - else - let ext = Filename.extension file in -- if Pervasives.(<>) file "" then -+ if Stdlib.(<>) file "" then - let cin = open_in file in - cin, Lexing.from_channel cin, true, ext - else ---- alt-ergo-2.3.0-free/sources/tools/gui/annoted_ast.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/tools/gui/annoted_ast.ml 2022-02-23 12:57:12.854376946 -0700 +--- alt-ergo-2.3.0-free/sources/tools/gui/annoted_ast.ml.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/tools/gui/annoted_ast.ml 2022-06-18 16:08:13.053310654 -0600 @@ -191,7 +191,7 @@ type annoted_node = module MDep = Map.Make ( struct @@ -508,8 +65,8 @@ )sl l in findtags_aform sl aaf.c acc ---- alt-ergo-2.3.0-free/sources/tools/gui/connected_ast.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/tools/gui/connected_ast.ml 2022-02-23 12:57:12.854376946 -0700 +--- alt-ergo-2.3.0-free/sources/tools/gui/connected_ast.ml.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/tools/gui/connected_ast.ml 2022-06-18 16:08:37.469375133 -0600 @@ -388,7 +388,7 @@ let rec unquantify_aform (buffer:sbuffer List.fold_left (fun (nbv, used, goal_used, ve, uplet, lets) v -> let ((s, _) as v'), e = List.hd ve in @@ -537,8 +94,8 @@ commit_tags_buffer sbuf | _ -> assert false end ---- alt-ergo-2.3.0-free/sources/tools/gui/main_gui.ml.orig 2021-06-29 06:08:30.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/tools/gui/main_gui.ml 2022-02-23 12:57:12.854376946 -0700 +--- alt-ergo-2.3.0-free/sources/tools/gui/main_gui.ml.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/tools/gui/main_gui.ml 2022-06-18 16:09:14.324472461 -0600 @@ -151,7 +151,7 @@ let save_session envs = let save_dialog cancel envs () = diff --git a/alt-ergo-stdlib-shims.patch b/alt-ergo-stdlib-shims.patch new file mode 100644 index 0000000..5f266df --- /dev/null +++ b/alt-ergo-stdlib-shims.patch @@ -0,0 +1,42 @@ +--- alt-ergo-2.3.0-free/sources/alt-ergo-lib-free.opam.orig 2022-05-20 03:15:57.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/alt-ergo-lib-free.opam 2022-06-18 16:35:11.569523676 -0600 +@@ -16,7 +16,6 @@ depends: [ + "ocplib-simplex" {>= "0.4" } + "zarith" + "seq" +- "stdlib-shims" + ] + conflicts: [ + "alt-ergo" +--- alt-ergo-2.3.0-free/sources/alt-ergo-parsers-free.opam.orig 2022-05-20 03:16:01.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/alt-ergo-parsers-free.opam 2022-06-18 16:35:52.177624279 -0600 +@@ -16,7 +16,6 @@ depends: [ + "psmt2-frontend" { >= "0.2" & < "0.4" } + "camlzip" + "menhir" { < "20210310" } +- "stdlib-shims" + ] + conflicts: [ + "alt-ergo-parsers" +--- alt-ergo-2.3.0-free/sources/lib/dune.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/dune 2022-06-18 16:34:45.634456726 -0600 +@@ -9,7 +9,7 @@ + (public_name alt-ergo-lib) + + ; external dependencies +- (libraries seq unix num str zarith dynlink ocplib-simplex stdlib-shims) ++ (libraries seq unix num str zarith dynlink ocplib-simplex) + + ; .mli only modules *also* need to be in this field + (modules_without_implementation matching_types numbersInterface sig sig_rel) +--- alt-ergo-2.3.0-free/sources/parsers/dune.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/parsers/dune 2022-06-18 16:36:07.177661183 -0600 +@@ -14,7 +14,7 @@ + (library + (name AltErgoParsers) + (public_name alt-ergo-parsers) +- (libraries camlzip dynlink psmt2-frontend alt-ergo-lib stdlib-shims) ++ (libraries camlzip dynlink psmt2-frontend alt-ergo-lib) + (modules + ; common + Parsers Parsers_loader MyZip diff --git a/alt-ergo.spec b/alt-ergo.spec index c1413a7..79fa381 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -8,22 +8,39 @@ %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. +%global minorver 2.3 +%global patchrel 3 + Name: alt-ergo -Version: 2.3.0 -Release: 5%{?dist} +Version: %{minorver}.%{patchrel} +Release: 1%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 URL: https://alt-ergo.ocamlpro.com/ -Source0: https://alt-ergo.ocamlpro.com/http/%{name}-free-%{version}/%{name}-free-%{version}.tar.gz +# The patch releases contain only the sources directory. The other files come +# from the minor releases. +Source0: https://alt-ergo.ocamlpro.com/http/%{name}-free-%{minorver}.0/%{name}-free-%{minorver}.0.tar.gz +%if 0%{?patchrel} > 0 +Source1: https://alt-ergo.ocamlpro.com/http/%{name}-free-%{version}/%{name}-free-%{version}.tar.gz +%endif # Created with gimp from official upstream icon -Source1: %{name}-icons.tar.xz -Source2: %{name}.desktop -Source3: %{name}.metainfo.xml +Source2: %{name}-icons.tar.xz +Source3: %{name}.desktop +Source4: %{name}.metainfo.xml # Do not use the deprecated Pervasives interface Patch0: %{name}-pervasives.patch # Adapt to recent changes in psmt2-frontend Patch1: %{name}-psmt2-frontend.patch +# Temporarily use the menhir table backend instead of the code backend for the +# AB plugin. Menhir is unable to infer types with the current code and layout. +# Check each new release to see if this is still necessary. +Patch2: %{name}-menhir.patch +# Fedora does not have or need the forward compatibility stdlib-shims package +Patch3: %{name}-stdlib-shims.patch BuildRequires: appstream BuildRequires: desktop-file-utils @@ -105,10 +122,17 @@ This package contains development files needed to build applications that use the Alt-Ergo library. %prep -%autosetup -n %{name}-%{version}-free -p1 -a 1 +%autosetup -n %{name}-%{minorver}.0-free -N -a 2 +%if 0%{?patchrel} > 0 +# See above. Replace the minor release sources with the patch release sources. +rm -rf sources +tar xf %{SOURCE1} +%endif + +%autopatch -p1 cd sources -cp -p %{SOURCE2} com.ocamlpro.%{name}.desktop +cp -p %{SOURCE3} com.ocamlpro.%{name}.desktop # Unzip an example cd examples/AB-Why3-plugin @@ -119,7 +143,7 @@ cd - %build # This is not an autoconf-generated script. Do NOT use %%configure. cd sources -./configure --prefix=%{_prefix} --libdir=%{_libdir}/ocaml --sharedir=%{_datadir} +./configure --prefix=%{_prefix} --libdir=%{_libdir}/ocaml --sharedir=%{_libdir}/ocaml %make_build %make_build doc @@ -140,11 +164,10 @@ rm -fr %{buildroot}%{_prefix}/doc mkdir -p %{buildroot}%{_mandir}/man1 cp -p doc/alt-ergo.1 %{buildroot}%{_mandir}/man1 -# Make the plugins directory -mkdir -p %{buildroot}%{_libdir}/ocaml/%{name}/plugins - -# Install the preludes -cp -a preludes %{buildroot}%{_libdir}/ocaml/%{name} +# The install target in the Makefile puts these in the wrong place +mv %{buildroot}%{_datadir}/alt-ergo/{plugins,preludes} \ + %{buildroot}%{_libdir}/ocaml/alt-ergo +rmdir %{buildroot}%{_datadir}/alt-ergo # Install the gtksourceview file mkdir -p %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs @@ -158,7 +181,7 @@ desktop-file-install --dir %{buildroot}%{_datadir}/applications \ # Install the AppData file mkdir -p %{buildroot}%{_metainfodir} -install -pm 644 %{SOURCE3} \ +install -pm 644 %{SOURCE4} \ %{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml appstreamcli validate --no-net \ %{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml @@ -178,6 +201,7 @@ dune runtest --release %{_bindir}/%{name} %{_mandir}/man1/alt-ergo.1.* %{_libdir}/ocaml/%{name}/ +%{_libdir}/ocaml/%{name}-free/ %files gui %{_bindir}/altgr-ergo @@ -195,6 +219,7 @@ dune runtest --release %ifarch %{ocaml_native_compiler} %{_libdir}/ocaml/%{name}-parsers/*.cmxs %endif +%{_libdir}/ocaml/%{name}-parsers-free/ %files -n ocaml-%{name}-parsers-devel %{_libdir}/ocaml/%{name}-parsers/dune-package @@ -216,6 +241,7 @@ dune runtest --release %ifarch %{ocaml_native_compiler} %{_libdir}/ocaml/%{name}-lib/*.cmxs %endif +%{_libdir}/ocaml/%{name}-lib-free/ %files -n ocaml-%{name}-lib-devel %doc sources/_build/default/_doc/* @@ -231,6 +257,11 @@ dune runtest --release %{_libdir}/ocaml/%{name}-lib/*.cmti %changelog +* Mon Jun 20 2022 Jerry James - 2.3.3-1 +- Version 2.3.3 +- Add -menhir patch to fix FTBFS +- Add -stdlib-shims patch since Fedora does not need stdlib-shims + * Sun Jun 19 2022 Richard W.M. Jones - 2.3.0-5 - OCaml 4.14.0 rebuild diff --git a/sources b/sources index 56b9730..2e808e5 100644 --- a/sources +++ b/sources @@ -1,2 +1,3 @@ SHA512 (alt-ergo-free-2.3.0.tar.gz) = e15efc6bbde59065c6ccaf1ef2f8158b8b9be4b00b2c2365e5eeb7d7114be72c47c813fc06880a6278edd7e288f24ef4588c88e0630d9bda9378a3eda3fd07ca +SHA512 (alt-ergo-free-2.3.3.tar.gz) = 0dc056c02c8ffdeb9eeaa127dd204d30a0ee95ffe38aa3f1a608b17019f377ea6520ccfc9cb09b109deac5f19e7e695b7e6ec18db969843312cfb17f3950c9ba SHA512 (alt-ergo-icons.tar.xz) = cb2e93bab3359f6f198e80e3e68840ed4b25a213b61f388a2de8abc299fd3c89240f64f610290ac89e6005088c484b2718a68ec18063076f73d7871a38ee038f From cf1a6b7780edc8d55a1f7bf68a927c1efd1eab4d Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 5 Jul 2022 17:03:29 -0600 Subject: [PATCH 42/77] Patch out uses of the dune external-lib-deps command. - Patch out references to the seq forward compatibility module. - Use new OCaml macros. --- alt-ergo-dune3.patch | 29 ++++++ ...ims.patch => alt-ergo-forward-compat.patch | 32 ++++++- alt-ergo.spec | 91 +++++++++---------- 3 files changed, 101 insertions(+), 51 deletions(-) create mode 100644 alt-ergo-dune3.patch rename alt-ergo-stdlib-shims.patch => alt-ergo-forward-compat.patch (60%) diff --git a/alt-ergo-dune3.patch b/alt-ergo-dune3.patch new file mode 100644 index 0000000..cb875a4 --- /dev/null +++ b/alt-ergo-dune3.patch @@ -0,0 +1,29 @@ +--- alt-ergo-2.3.0-free/sources/configure.ml.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/configure.ml 2022-07-05 16:42:35.856375154 -0600 +@@ -139,26 +139,6 @@ let () = + Format.eprintf "ERROR: Couldn't find dune in env@."; + exit 1 + +-(* run dune to check that dependencies are installed *) +-let () = +- let p_opt = match !pkg with +- | "" -> "" +- | s -> Format.asprintf "-p %s" s +- in +- let cmd = Format.asprintf +- "dune external-lib-deps --display=quiet --missing %s @install" +- p_opt +- in +- let ch = Unix.open_process_in cmd in +- let _ = read_all ch in +- let res = Unix.close_process_in ch in +- match res with +- | Unix.WEXITED 0 -> +- Format.printf "All deps are installed.@." +- | _ -> +- (* dune already prints the missing libs on stderr *) +- exit 2 +- + let () = + Format.printf "Good to go !@." + diff --git a/alt-ergo-stdlib-shims.patch b/alt-ergo-forward-compat.patch similarity index 60% rename from alt-ergo-stdlib-shims.patch rename to alt-ergo-forward-compat.patch index 5f266df..b3be679 100644 --- a/alt-ergo-stdlib-shims.patch +++ b/alt-ergo-forward-compat.patch @@ -1,13 +1,25 @@ --- alt-ergo-2.3.0-free/sources/alt-ergo-lib-free.opam.orig 2022-05-20 03:15:57.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/alt-ergo-lib-free.opam 2022-06-18 16:35:11.569523676 -0600 -@@ -16,7 +16,6 @@ depends: [ ++++ alt-ergo-2.3.0-free/sources/alt-ergo-lib-free.opam 2022-07-05 16:40:03.983955825 -0600 +@@ -15,8 +15,6 @@ depends: [ + "num" "ocplib-simplex" {>= "0.4" } "zarith" - "seq" +- "seq" - "stdlib-shims" ] conflicts: [ "alt-ergo" +--- alt-ergo-2.3.0-free/sources/alt-ergo-lib.opam.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/alt-ergo-lib.opam 2022-07-05 16:47:56.113259397 -0600 +@@ -15,8 +15,6 @@ depends: [ + "num" + "ocplib-simplex" {>= "0.4" } + "zarith" +- "seq" +- "stdlib-shims" + ] + conflicts: [ + "alt-ergo-free" --- alt-ergo-2.3.0-free/sources/alt-ergo-parsers-free.opam.orig 2022-05-20 03:16:01.000000000 -0600 +++ alt-ergo-2.3.0-free/sources/alt-ergo-parsers-free.opam 2022-06-18 16:35:52.177624279 -0600 @@ -16,7 +16,6 @@ depends: [ @@ -18,14 +30,24 @@ ] conflicts: [ "alt-ergo-parsers" +--- alt-ergo-2.3.0-free/sources/alt-ergo-parsers.opam.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/alt-ergo-parsers.opam 2022-07-05 16:39:33.254870985 -0600 +@@ -16,7 +16,6 @@ depends: [ + "psmt2-frontend" { >= "0.2" } + "camlzip" + "menhir" +- "stdlib-shims" + ] + homepage: "http://alt-ergo.ocamlpro.com/" + dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git" --- alt-ergo-2.3.0-free/sources/lib/dune.orig 2022-05-20 01:34:55.000000000 -0600 -+++ alt-ergo-2.3.0-free/sources/lib/dune 2022-06-18 16:34:45.634456726 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/dune 2022-07-05 16:50:35.778700249 -0600 @@ -9,7 +9,7 @@ (public_name alt-ergo-lib) ; external dependencies - (libraries seq unix num str zarith dynlink ocplib-simplex stdlib-shims) -+ (libraries seq unix num str zarith dynlink ocplib-simplex) ++ (libraries unix num str zarith dynlink ocplib-simplex) ; .mli only modules *also* need to be in this field (modules_without_implementation matching_types numbersInterface sig sig_rel) diff --git a/alt-ergo.spec b/alt-ergo.spec index 79fa381..ecfba1b 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -16,7 +16,7 @@ Name: alt-ergo Version: %{minorver}.%{patchrel} -Release: 1%{?dist} +Release: 2%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -39,8 +39,10 @@ Patch1: %{name}-psmt2-frontend.patch # AB plugin. Menhir is unable to infer types with the current code and layout. # Check each new release to see if this is still necessary. Patch2: %{name}-menhir.patch -# Fedora does not have or need the forward compatibility stdlib-shims package -Patch3: %{name}-stdlib-shims.patch +# Fedora does not need the forward compatibility seq and stdlib-shims packages +Patch3: %{name}-forward-compat.patch +# Dune 3 eliminated the external-lib-deps command +Patch4: %{name}-dune3.patch BuildRequires: appstream BuildRequires: desktop-file-utils @@ -52,9 +54,7 @@ BuildRequires: ocaml-lablgtk-devel BuildRequires: ocaml-menhir BuildRequires: ocaml-num-devel BuildRequires: ocaml-ocplib-simplex-devel >= 0.4 -BuildRequires: ocaml-odoc BuildRequires: ocaml-psmt2-frontend-devel >= 0.2 -BuildRequires: ocaml-seq-devel BuildRequires: ocaml-zarith-devel BuildRequires: ocaml-zip-devel @@ -113,7 +113,6 @@ Summary: Development files for ocaml-alt-ergo-lib Requires: ocaml-alt-ergo-lib%{?_isa} = %{version}-%{release} Requires: ocaml-num-devel%{?_isa} Requires: ocaml-ocplib-simplex-devel%{?_isa} -Requires: ocaml-seq-devel%{?_isa} Requires: ocaml-zarith-devel%{?_isa} %description -n ocaml-alt-ergo-lib-devel %_desc @@ -143,19 +142,15 @@ cd - %build # This is not an autoconf-generated script. Do NOT use %%configure. cd sources -./configure --prefix=%{_prefix} --libdir=%{_libdir}/ocaml --sharedir=%{_libdir}/ocaml +./configure --prefix=%{_prefix} --libdir=%{ocamldir} --sharedir=%{ocamldir} %make_build -%make_build doc %install cd sources %make_install -# We do not want the dune markers -find _build/default/_doc/_html -name .dune-keep -delete - # We do not want the ml files -find %{buildroot}%{_libdir}/ocaml -name \*.ml -delete +find %{buildroot}%{ocamldir} -name \*.ml -delete # We install the documentation with the doc macro rm -fr %{buildroot}%{_prefix}/doc @@ -166,7 +161,7 @@ cp -p doc/alt-ergo.1 %{buildroot}%{_mandir}/man1 # The install target in the Makefile puts these in the wrong place mv %{buildroot}%{_datadir}/alt-ergo/{plugins,preludes} \ - %{buildroot}%{_libdir}/ocaml/alt-ergo + %{buildroot}%{ocamldir}/alt-ergo rmdir %{buildroot}%{_datadir}/alt-ergo # Install the gtksourceview file @@ -193,70 +188,74 @@ cp -a icons %{buildroot}%{_datadir}/icons/hicolor %check cd sources -dune runtest --release +%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.* -%{_libdir}/ocaml/%{name}/ -%{_libdir}/ocaml/%{name}-free/ +%{ocamldir}/%{name}/ +%{ocamldir}/%{name}-free/ %files gui %{_bindir}/altgr-ergo %{_datadir}/applications/com.ocamlpro.%{name}.desktop %{_datadir}/gtksourceview-2.0/language-specs/%{name}.lang %{_datadir}/icons/hicolor/*/apps/%{name}.png -%{_libdir}/ocaml/altgr-ergo/ +%{ocamldir}/altgr-ergo/ %{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml %files -n ocaml-%{name}-parsers -%dir %{_libdir}/ocaml/%{name}-parsers/ -%{_libdir}/ocaml/%{name}-parsers/META -%{_libdir}/ocaml/%{name}-parsers/*.cma -%{_libdir}/ocaml/%{name}-parsers/*.cmi +%dir %{ocamldir}/%{name}-parsers/ +%{ocamldir}/%{name}-parsers/META +%{ocamldir}/%{name}-parsers/*.cma +%{ocamldir}/%{name}-parsers/*.cmi %ifarch %{ocaml_native_compiler} -%{_libdir}/ocaml/%{name}-parsers/*.cmxs +%{ocamldir}/%{name}-parsers/*.cmxs %endif -%{_libdir}/ocaml/%{name}-parsers-free/ +%{ocamldir}/%{name}-parsers-free/ %files -n ocaml-%{name}-parsers-devel -%{_libdir}/ocaml/%{name}-parsers/dune-package -%{_libdir}/ocaml/%{name}-parsers/opam +%{ocamldir}/%{name}-parsers/dune-package +%{ocamldir}/%{name}-parsers/opam %ifarch %{ocaml_native_compiler} -%{_libdir}/ocaml/%{name}-parsers/*.a -%{_libdir}/ocaml/%{name}-parsers/*.cmx -%{_libdir}/ocaml/%{name}-parsers/*.cmxa +%{ocamldir}/%{name}-parsers/*.a +%{ocamldir}/%{name}-parsers/*.cmx +%{ocamldir}/%{name}-parsers/*.cmxa %endif -%{_libdir}/ocaml/%{name}-parsers/*.mli -%{_libdir}/ocaml/%{name}-parsers/*.cmt -%{_libdir}/ocaml/%{name}-parsers/*.cmti +%{ocamldir}/%{name}-parsers/*.mli +%{ocamldir}/%{name}-parsers/*.cmt +%{ocamldir}/%{name}-parsers/*.cmti %files -n ocaml-%{name}-lib -%dir %{_libdir}/ocaml/%{name}-lib/ -%{_libdir}/ocaml/%{name}-lib/META -%{_libdir}/ocaml/%{name}-lib/*.cma -%{_libdir}/ocaml/%{name}-lib/*.cmi +%dir %{ocamldir}/%{name}-lib/ +%{ocamldir}/%{name}-lib/META +%{ocamldir}/%{name}-lib/*.cma +%{ocamldir}/%{name}-lib/*.cmi %ifarch %{ocaml_native_compiler} -%{_libdir}/ocaml/%{name}-lib/*.cmxs +%{ocamldir}/%{name}-lib/*.cmxs %endif -%{_libdir}/ocaml/%{name}-lib-free/ +%{ocamldir}/%{name}-lib-free/ %files -n ocaml-%{name}-lib-devel -%doc sources/_build/default/_doc/* -%{_libdir}/ocaml/%{name}-lib/dune-package -%{_libdir}/ocaml/%{name}-lib/opam +%{ocamldir}/%{name}-lib/dune-package +%{ocamldir}/%{name}-lib/opam %ifarch %{ocaml_native_compiler} -%{_libdir}/ocaml/%{name}-lib/*.a -%{_libdir}/ocaml/%{name}-lib/*.cmx -%{_libdir}/ocaml/%{name}-lib/*.cmxa +%{ocamldir}/%{name}-lib/*.a +%{ocamldir}/%{name}-lib/*.cmx +%{ocamldir}/%{name}-lib/*.cmxa %endif -%{_libdir}/ocaml/%{name}-lib/*.mli -%{_libdir}/ocaml/%{name}-lib/*.cmt -%{_libdir}/ocaml/%{name}-lib/*.cmti +%{ocamldir}/%{name}-lib/*.mli +%{ocamldir}/%{name}-lib/*.cmt +%{ocamldir}/%{name}-lib/*.cmti %changelog +* Tue Jul 5 2022 Jerry James - 2.3.3-2 +- Patch out uses of the dune external-lib-deps command +- Patch out references to the seq forward compatibility module +- Use new OCaml macros + * Mon Jun 20 2022 Jerry James - 2.3.3-1 - Version 2.3.3 - Add -menhir patch to fix FTBFS From 43489678cad85bc82bbe1d3cec64e28fa9b6fbf4 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Wed, 20 Jul 2022 20:41:54 +0000 Subject: [PATCH 43/77] Rebuilt for https://fedoraproject.org/wiki/Fedora_37_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 ecfba1b..2f4e937 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -16,7 +16,7 @@ Name: alt-ergo Version: %{minorver}.%{patchrel} -Release: 2%{?dist} +Release: 3%{?dist} Summary: Automated theorem prover including linear arithmetic License: ASL 2.0 @@ -251,6 +251,9 @@ cd sources %{ocamldir}/%{name}-lib/*.cmti %changelog +* Wed Jul 20 2022 Fedora Release Engineering - 2.3.3-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild + * Tue Jul 5 2022 Jerry James - 2.3.3-2 - Patch out uses of the dune external-lib-deps command - Patch out references to the seq forward compatibility module From 61ce442efc897a263eb05d38a594e189056e5ca0 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 11 Aug 2022 09:24:41 -0600 Subject: [PATCH 44/77] 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 45/77] 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 46/77] 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 47/77] 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 48/77] 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 49/77] 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 50/77] 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 51/77] 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 52/77] 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 53/77] 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 54/77] 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 55/77] 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 56/77] 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 57/77] 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 58/77] 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 59/77] 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 60/77] 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 61/77] 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 62/77] 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 63/77] 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 64/77] 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 65/77] 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 66/77] 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 67/77] 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 68/77] 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 69/77] 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 70/77] 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 71/77] 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 72/77] 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 73/77] 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 74/77] 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 75/77] 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 76/77] 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 77/77] 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