# Rocq's plugin architecture requires cmxs files, so: ExclusiveArch: %{ocaml_native_compiler} # ANTLR is unavailable on i686 # See https://fedoraproject.org/wiki/Changes/Drop_i686_JDKs # # This is commented for out now because ocaml_native_compiler is # narrower, and apparently if you have two ExclusiveArch lines in a # spec file, RPM ignores the first one and uses the second one! # ExclusiveArch: %%{java_arches} %ifarch %{ocaml_native_compiler} %global camlsuffix opt %else %global camlsuffix byte %endif # .coqide-gtk2rc produces an rpmlint warning due to its name, # however, this name is proper as per the Rocq documentation # Rocq installs python files into nonstandard places %global _python_bytecompile_extra 0 # 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 giturl https://github.com/rocq-prover/rocq Name: rocq Version: 9.1.0 Release: %autorelease Summary: Proof management system # The project as a whole is LGPL-2.1-only. Exceptions: # - clib/diff2.ml is MIT # - gramlib is BSD-3-Clause License: LGPL-2.1-only AND MIT AND BSD-3-Clause URL: https://rocq-prover.org/ VCS: git:%{giturl}.git Source0: %{giturl}/archive/V%{version}/%{name}-%{version}.tar.gz Source1: fr.inria.rocqide.desktop Source2: rocq.xml Source3: fr.inria.rocqide.metainfo.xml # Expose a dependency on the math library so rpm can see it Patch: %{name}-mathlib.patch BuildRequires: ocaml >= 4.09.0 BuildRequires: ocaml-cairo-devel >= 0.6.4 BuildRequires: ocaml-dune >= 3.6.1 BuildRequires: ocaml-findlib-devel >= 1.8.1 BuildRequires: ocaml-lablgtk3-sourceview3-devel >= 3.1.2 BuildRequires: ocaml-ocamldoc BuildRequires: ocaml-ounit-devel BuildRequires: ocaml-zarith-devel >= 1.11 BuildRequires: adwaita-icon-theme BuildRequires: antlr4 >= 4.7.1 BuildRequires: libappstream-glib BuildRequires: csdp-tools BuildRequires: desktop-file-utils BuildRequires: findutils BuildRequires: git-core BuildRequires: java BuildRequires: make BuildRequires: python3-devel BuildRequires: %{py3_dist antlr4-python3-runtime} BuildRequires: rsync BuildRequires: time %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: coq-core-compat%{_isa} = %{version}-%{release} Requires: csdp-tools Requires: ocaml-findlib Requires: texlive-base Recommends: rocq-stdlib Recommends: emacs-proofgeneral Provides: coq = %{version}-%{release} Obsoletes: coq < 9.1.0 %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.} %description %_desc 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. %package core Summary: Core components of the Rocq proof management system Requires: %{name}%{?_isa} = %{version}-%{release} Provides: coq-core = %{version}-%{release} Obsoletes: coq-core < 9.1.0 %description core %_desc This package includes the Coq core binaries, plugins, and tools, but not the vernacular standard library. %package -n coq-core-compat Summary: Compatibility binaries for Coq after the Rocq renaming Requires: %{name}-core%{?_isa} = %{version}-%{release} %description -n coq-core-compat %_desc This package includes compatibility binaries to call Rocq through previous Coq commands like coqc coqtop,... %package coqide-server Summary: The coqidetop language server Requires: %{name}-core%{?_isa} = %{version}-%{release} Provides: coq-coqide-server = %{version}-%{release} Obsoletes: coq-coqide-server < 9.1.0 %description coqide-server %_desc This package provides the coqidetop language server, an implementation of Rocq's XML protocol which allows clients, such as RocqIDE, to interact with Rocq in a structured way. %package rocqide Summary: RocqIDE for the Rocq proof management system Requires: %{name}-coqide-server%{?_isa} = %{version}-%{release} Requires: adwaita-icon-theme Requires: hicolor-icon-theme Requires: xdg-utils Provides: coq-coqide = %{version}-%{release} Obsoletes: coq-coqide < 9.1.0 %description rocqide %_desc This package provides RocqIDE, a graphical user interface for the development of interactive proofs. %if %{with doc} %package doc Summary: Documentation for the Rocq proof management system # 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/LICENSE 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) Provides: coq-doc = %{version}-%{release} Obsoletes: coq-doc < 9.1.0 %description doc %_desc This package provides documentation and tutorials for the system. The main documentation comes in two parts: the main Library documentation, which describes all Corelib.* modules, and the Reference Manual, which gives a more complete description of the whole system. Included are also HTML versions of both. Furthermore, there are two tutorials, the main one, and one specifically on recursive types. The example code for the latter is also included. %endif %prep %autosetup -p1 %conf fixtimestamp() { touch -r $1.orig $1 rm -f $1.orig } # Use Fedora flags sed -e 's|-Wall.*-O2|%{build_cflags} %{build_ldflags} -Wno-unused|' \ -e 's| -march=native||' \ -i tools/configure/configure.ml # Make sure debuginfo is generated sed -i 's,-shared,& -g,g' tools/CoqMakefile.in # Do not invoke env for f in doc/tools/coqrst/notations/fontsupport.py; do sed -i.orig 's,/usr/bin/env python2,%{python3},' $f fixtimestamp $f done for f in $(grep -Frl '%{_bindir}/env'); do sed -r -i.orig 's,(%{_bindir}/)env[[:blank:]]+([[:alnum:]]+),\1\2,g' $f fixtimestamp $f done %build %global rocqdocdir %{?_pkgdocdir}%{!?_pkgdocdir:%{_docdir}/rocq-%{version}} # Regenerate ANTLR files cd doc/tools/coqrst/notations antlr4 -Dlanguage=Python3 -visitor -no-listener TacticNotations.g cd - # Set our configuration options # NOTE: Keep libdir `coq', it's hard-coded in Dune's `coq.theory' stanzas. ./configure -prefix %{_prefix} \ -libdir %{ocamldir}/coq \ -configdir %{_sysconfdir}/xdg/%{name} \ -mandir %{_mandir} \ -docdir %{rocqdocdir} \ %ifarch %{ocaml_natdynlink} -natdynlink yes \ %else -natdynlink no \ %endif -browser "xdg-open %s" \ -bytecode-compiler yes \ -native-compiler no # As of coq 8.17.0, the native compiler cannot be build with OCaml 5.x #%%ifarch %%{ocaml_native_compiler} # -native-compiler yes #%%else # -native-compiler no #%%endif # Build the binary artifacts export SPHINXWARNOPT="-w$PWD/sphinx-warn.log" make dunestrap VERBOSE=1 DUNEOPT="--verbose --profile=release" %dune_build %{!?with_doc:-p rocq-core,coq-core,rocq-runtime,coqide-server,rocqide} %install %dune_install %{!?with_doc:rocq-core coq-core rocq-runtime coqide-server rocqide} # Install the LaTeX style file mkdir -p %{buildroot}%{_texmf_main}/tex/latex/misc mv %{buildroot}%{_datadir}/texmf/tex/latex/misc/coqdoc.sty \ %{buildroot}%{_texmf_main}/tex/latex/misc rm -fr %{buildroot}%{_datadir}/texmf # FIXME: dune ignores the configdir argument to configure mkdir -p %{buildroot}%{_sysconfdir}/xdg/%{name} %if %{with doc} # Prepare the documentation for installation find doc/sphinx/_build/html -name .buildinfo -delete %endif # Install desktop and file type icons # NOTE: https://github.com/rocq-prover/rocq/commit/e7074f14e5ade674080acf7c475bf940c418b57b mkdir -p %{buildroot}%{_datadir}/icons/hicolor/256x256/apps mkdir -p %{buildroot}%{_datadir}/icons/hicolor/256x256/mimetypes cp --preserve=timestamps ide/rocqide/coq.png \ %{buildroot}%{_datadir}/icons/hicolor/256x256/apps/rocq.png cp --preserve=timestamps ide/rocqide/coq.png \ %{buildroot}%{_datadir}/icons/hicolor/256x256/mimetypes/rocqfile.png # Make a MIME type for .v files mkdir -p %{buildroot}%{_datadir}/mime/packages cp -p %{SOURCE2} %{buildroot}%{_datadir}/mime/packages # Install desktop file desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE1} # Install AppData file mkdir -p %{buildroot}%{_metainfodir} install -pm 644 %{SOURCE3} %{buildroot}%{_metainfodir} appstream-util validate-relax --nonet \ %{buildroot}%{_metainfodir}/fr.inria.rocqide.metainfo.xml # Install the language bindings # NOTE: Must still be installed in a dir named `coq'. mkdir -p %{buildroot}%{_datadir}/gtksourceview-3.0/language-specs for fil in coq.lang coq-ssreflect.lang; do ln -s ../../coq/$fil %{buildroot}%{_datadir}/gtksourceview-3.0/language-specs done # Install the style file # NOTE: Must still be installed in a dir named `coq'. mkdir -p %{buildroot}%{_datadir}/gtksourceview-3.0/styles ln -s ../../coq/coq_style.xml %{buildroot}%{_datadir}/gtksourceview-3.0/styles # Byte compile the tools %py_byte_compile %{python3} %{buildroot}%{ocamldir}/coq-core/tools %files %{ocamldir}/coq/ %{ocamldir}/rocq-runtime/ %files core %doc README.md %license LICENSE %{ocamldir}/rocq-core/ %{ocamldir}/stublibs/dllcoqperf_stubs.so %{ocamldir}/stublibs/dllcoqrun_stubs.so %{_bindir}/rocq %{_bindir}/rocq.byte %{_bindir}/rocqchk %{_bindir}/csdpcert %{_bindir}/ocamllibdep %{_bindir}/votour %{_mandir}/man1/rocq.1* %{_mandir}/man1/rocqchk.1* %{_texmf_main}/tex/latex/misc/ %files -n coq-core-compat %{ocamldir}/coq-core/ %{_bindir}/coqc* %{_bindir}/coqdep %{_bindir}/coqdoc %{_bindir}/coq_makefile %{_bindir}/coqnative %{_bindir}/coqpp %{_bindir}/coq-tex %{_bindir}/coqtop* %{_bindir}/coqwc %{_bindir}/coqworkmgr %{_mandir}/man1/coqc.1* %{_mandir}/man1/coqchk.1* %{_mandir}/man1/coqdep.1* %{_mandir}/man1/coqdoc.1* %{_mandir}/man1/coq_makefile.1* %{_mandir}/man1/coqnative.1* %{_mandir}/man1/coq-tex.1* %{_mandir}/man1/coqtop.1* %{_mandir}/man1/coqtop.byte.1* %{_mandir}/man1/coqwc.1* %files coqide-server %{_bindir}/coqidetop* %{ocamldir}/coqide-server/ %files rocqide %doc ide/rocqide/FAQ %{_bindir}/rocqide # NOTE: Arch independent data is still stored in a dir named `coq'. %{_datadir}/coq/ %{_datadir}/icons/hicolor/256x256/apps/rocq.png %{_datadir}/icons/hicolor/256x256/mimetypes/rocqfile.png %{_mandir}/man1/rocqide.1* %{ocamldir}/rocqide/ %{_metainfodir}/fr.inria.rocqide.metainfo.xml %{_datadir}/applications/fr.inria.rocqide.desktop %{_datadir}/gtksourceview-3.0/language-specs/coq*.lang %{_datadir}/gtksourceview-3.0/styles/coq_style.xml %{_datadir}/mime/packages/rocq.xml %{_sysconfdir}/xdg/rocq/ %if %{with doc} %files doc %license doc/LICENSE %{rocqdocdir} %endif %changelog %autochangelog