# Rocq's plugin architecture requires cmxs files, so: ExclusiveArch: %{ocaml_native_compiler} # This package is installed into an archful location, but contains no ELF # objects. %global debug_package %{nil} # The documentation package cannot be built with ocaml-dune 3.8.2. Check later # releases of both rocq and dune to see if the issues have been resolved. %bcond doc 0 %global stdlibdir %{ocamldir}/coq/user-contrib/Stdlib %global coqver 9.1.0 %global giturl https://github.com/rocq-prover/stdlib Name: rocq-stdlib Version: 9.0.0 Release: %autorelease Summary: The Rocq proof assistant standard library License: LGPL-2.1-only URL: https://rocq-prover.org/ VCS: git:%{giturl}.git Source0: %{giturl}/archive/V%{version}/%{name}-%{version}.tar.gz BuildRequires: coq-core-compat = %{coqver} BuildRequires: ocaml >= 4.09.0 BuildRequires: ocaml-dune >= 3.6.1 BuildRequires: ocaml-findlib BuildRequires: antlr4 >= 4.7.1 BuildRequires: findutils BuildRequires: python3-devel %if %{with doc} # For documentation BuildRequires: hevea BuildRequires: %{py3_dist beautifulsoup4} BuildRequires: %{py3_dist pexpect} BuildRequires: %{py3_dist sphinx} BuildRequires: %{py3_dist sphinxcontrib-bibtex} BuildRequires: %{py3_dist sphinx-rtd-theme} BuildRequires: tex(latex) BuildRequires: tex(adjustbox.sty) BuildRequires: tex(capt-of.sty) BuildRequires: tex(comment.sty) BuildRequires: tex(epic.sty) BuildRequires: tex(fncychap.sty) BuildRequires: tex(framed.sty) BuildRequires: tex(fullpage.sty) BuildRequires: tex(moreverb.sty) BuildRequires: tex(multirow.sty) BuildRequires: tex(needspace.sty) BuildRequires: tex(stmaryrd.sty) BuildRequires: tex(tabulary.sty) BuildRequires: tex(upquote.sty) BuildRequires: tex(utf8x.def) BuildRequires: tex(wrapfig.sty) BuildRequires: tex(FreeSerif.otf) BuildRequires: tex-cm-super BuildRequires: tex-courier BuildRequires: tex-ec BuildRequires: tex-helvetic BuildRequires: tex-symbol BuildRequires: tex-times BuildRequires: tex-xindy BuildRequires: tex-zapfchan BuildRequires: tex-zapfding %else BuildRequires: texlive-base %endif Requires: rocq%{?_isa} = %{coqver} %global _desc %{expand: Rocq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching.} %description %_desc This package includes the Rocq Standard Library, that is to say, the set of modules usually bound to the Stdlib.* namespace. %package source Summary: Source files of the Rocq proof assistant standard library Requires: %{name}%{?_isa} = %{version}-%{release} %description source %_desc This package contains the source Rocq files for the standard library. These files are not needed to use the standard library. They are made available for informational purposes. %if %{with doc} %package doc Summary: Documentation for the Rocq proof assistant standard library # The documentation as a whole is OPUBL-1.0. # Some sphinx-installed files are LGPL-2.1-only. # Some sphinx-installed files are MIT. # # The OPUBL-1.0 license is not allowed for Fedora, but carries this usage note # (https://gitlab.com/fedora/legal/fedora-license-data/-/blob/main/data/OPUBL-1.0.toml): # "Allowed-for documentation if the copyright holder does not exercise any of # the “LICENSE OPTIONS” listed in Section VI". # # doc/sphinx/license.rst contains this note: "Options A and B are *not* elected." # # Therefore, this package falls under the Fedora exception. License: OPUBL-1.0 AND LGPL-2.1-only AND MIT BuildArch: noarch Requires: font(fontawesome) Requires: font(lato) Requires: font(robotoslab) %description doc %_desc This package provides documentation for the standard library. The main documentation comes in two parts: the main Library documentation, which describes all Stdlib.* modules, and the Reference Manual, which gives a more complete description of the library. Included are also HTML versions of both. %endif %prep %autosetup -n stdlib-%{version} -p1 %build %global stdlibdocdir %{?_pkgdocdir}%{!?_pkgdocdir:%{_docdir}/%{name}-%{version}} # Regenerate ANTLR files cd doc/tools/coqrst/notations antlr4 -Dlanguage=Python3 -visitor -no-listener TacticNotations.g cd - # Build the artifacts export SPHINXWARNOPT="-w$PWD/sphinx-warn.log" %dune_build %{!?with_doc:-p rocq-stdlib} %install %dune_install %{!?with_doc:rocq-stdlib} %if %{with doc} # Prepare the documentation for installation find doc/sphinx/_build/html -name .buildinfo -delete %endif %files %doc README.md CONTRIBUTING.md %license LICENSE %{ocamldir}/%{name}/ %{stdlibdir} %exclude %{stdlibdir}/*/*.v %files source %{stdlibdir}/*/*.v %if %{with doc} %files doc %license doc/LICENSE %{stdlibdocdir} %endif %changelog %autochangelog