From d562401933ebc0b6a9fce48a0f0eeacfe85b621b Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Wed, 22 Jan 2020 09:24:15 -0700
Subject: [PATCH] Reenable coq support. Add coq-menhirlib subpackage, without
 which coq support is rather pointless.

---
 ocaml-menhir.rpmlintrc | 15 +++++++++++++++
 ocaml-menhir.spec      | 38 ++++++++++++++++++++++++++++++++++----
 2 files changed, 49 insertions(+), 4 deletions(-)
 create mode 100644 ocaml-menhir.rpmlintrc

diff --git a/ocaml-menhir.rpmlintrc b/ocaml-menhir.rpmlintrc
new file mode 100644
index 0000000..d283709
--- /dev/null
+++ b/ocaml-menhir.rpmlintrc
@@ -0,0 +1,15 @@
+# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON
+# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors
+
+# The dictionary is missing some technical terms
+addFilter(r'W: spelling-error .* (parsers|validator)')
+
+# OCaml does this to us.  We have no control over it.
+addFilter(r'ocaml-menhir[^:]+: E: missing-call-to-chdir-with-chroot')
+
+# Documentation is in the main package.
+addFilter(r'ocaml-menhir-devel\.[^:]+: W: no-documentation')
+
+# This package has no binary bits, but must be installed in an arch-specific
+# location.
+addFilter(r'coq-menhirlib\.[^:]+: W: only-non-binary-in-usr-lib')
diff --git a/ocaml-menhir.spec b/ocaml-menhir.spec
index 2e5f278..2d54c0e 100644
--- a/ocaml-menhir.spec
+++ b/ocaml-menhir.spec
@@ -5,11 +5,11 @@
 %global debug_package %{nil}
 %endif
 
-%global with_coq 0
+%bcond_without coq
 
 Name:           ocaml-menhir
 Version:        20190924
-Release:        6%{?dist}
+Release:        7%{?dist}
 Summary:        LR(1) parser generator for OCaml
 
 # The generator is GPLv2
@@ -17,7 +17,7 @@ License:        GPLv2
 URL:            http://gallium.inria.fr/~fpottier/menhir/
 Source0:        https://gitlab.inria.fr/fpottier/menhir/-/archive/%{version}/menhir-%{version}.tar.bz2
 
-%if %{with_coq}
+%if %{with coq}
 BuildRequires:  coq
 %endif
 BuildRequires:  hevea
@@ -46,6 +46,20 @@ Requires:       ocaml-findlib
 The %{name}-devel package contains libraries and signature files
 for developing applications that use %{name}.
 
+%if %{with coq}
+%package     -n coq-menhirlib
+Summary:        Support library for verified Coq parsers produced by Menhir
+License:        LGPLv3+
+Requires:       coq
+
+%description -n coq-menhirlib
+The Menhir parser generator, in --coq mode, can produce Coq parsers.
+These parsers must be linked against this library, which provides both an
+interpreter (which allows running the generated parser) and a validator
+(which allows verifying, at parser construction time, that the generated
+parser is correct and complete with respect to the grammar).
+%endif
+
 %prep
 %setup -q -n menhir-%{version}
 
@@ -57,7 +71,8 @@ rm -fr demos/obsolete
 
 %build
 make PREFIX=%{_prefix} TARGET=%{target}
-%if %{with_coq}
+%if %{with coq}
+make -C coq-menhirlib
 make -C demos clean
 %endif
 make -C doc
@@ -69,6 +84,10 @@ mkdir -p $OCAMLFIND_DESTDIR
 make install PREFIX=%{buildroot}%{_prefix} TARGET=%{target}
 rm -fr %{buildroot}%{_docdir}/menhir
 
+%if %{with coq}
+make -C coq-menhirlib install DESTDIR=%{buildroot}
+%endif
+
 # The need for this went away with version 20190924, but the makefile still
 # creates it.
 rmdir %{buildroot}%{_datadir}/menhir
@@ -101,7 +120,18 @@ find demos \( -name .merlin -o -name .gitignore \) -delete
 %{_libdir}/ocaml/menhirSdk/menhirSdk.cmx
 %{_libdir}/ocaml/menhirSdk/menhirSdk.o
 
+%if %{with coq}
+%files -n coq-menhirlib
+%doc coq-menhirlib/CHANGES.md coq-menhirlib/README.md
+%license coq-menhirlib/LICENSE
+%{_libdir}/coq/user-contrib/MenhirLib/
+%endif
+
 %changelog
+* Wed Jan 22 2020 Jerry James <loganjerry@gmail.com> - 20190924-7
+- Reenable coq support
+- Add coq-menhirlib subpackage, without which coq support is rather pointless
+
 * Sun Jan 19 2020 Richard W.M. Jones <rjones@redhat.com> - 20190924-6
 - OCaml 4.10.0+beta1 rebuild.