Version 2.2.0. Drop upstreamed -newline patch.

alt-ergo-2.0.0-newline.patch

@@ -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

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')

alt-ergo.spec

@@ -7,23 +7,20 @@
 %endif
 
 Name:		alt-ergo
-Version:	2.0.0
-Release:	10%{?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,48 +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
 
-%description
+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)\\\)
+
+%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
@@ -128,7 +146,6 @@ done
 %license COPYING.md LICENSE.md
 %{_bindir}/%{name}
 %{_mandir}/man1/alt-ergo.1.*
-%{_libdir}/%{name}/
 
 %files gui
 %{_bindir}/altgr-ergo
@@ -137,10 +154,41 @@ 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 <loganjerry@gmail.com> - 2.2.0-1
+- Version 2.2.0
+- Drop upstreamed -newline patch
+
+* Wed Apr  8 2020 Jerry James <loganjerry@gmail.com> - 2.0.0-11
+- Filter out Requires for private interfaces we do not Provide
+
 * Tue Mar 24 2020 Jerry James <loganjerry@gmail.com> - 2.0.0-10
 - Rebuild for ocaml-menhir 20200211
 
+* Fri Feb 28 2020 Richard W.M. Jones <rjones@redhat.com> - 2.0.0-9.1
+- OCaml 4.10.0 final (Fedora 32).
+
 * Wed Feb 26 2020 Richard W.M. Jones <rjones@redhat.com> - 2.0.0-9
 - OCaml 4.10.0 final.
 

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