Reenable coq support.
Add coq-menhirlib subpackage, without which coq support is rather pointless.
This commit is contained in:
parent
3b6c1d9171
commit
d562401933
|
@ -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')
|
|
@ -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.
|
||||
|
||||
|
|
Loading…
Reference in New Issue