9:50 a.m.
The package rpms/coq.git has added or updated architecture specific content in its
spec file (ExclusiveArch/ExcludeArch or %ifarch/%ifnarch) in commit(s):
https://src.fedoraproject.org/cgit/rpms/coq.git/commit/?id=0e164ec5d36796....
Change:
-%ifarch %{ocaml_native_compiler}
Thanks.
Full change:
============
commit 0e164ec5d3679677f62c9ad3dd30470d6dc3fb65
Author: Jerry James <loganjerry(a)gmail.com>
Date: Mon Aug 31 08:50:18 2020 -0600
Version 8.12.0.
- Build with dune.
- Add coqide-server subpackage.
- Unbundle fonts from the documentation.
diff --git a/0001-Sphinx-3-support.patch b/0001-Sphinx-3-support.patch
index adb2625..aba5c89 100644
--- a/0001-Sphinx-3-support.patch
+++ b/0001-Sphinx-3-support.patch
@@ -1,33 +1,6 @@
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
-@@ -21,6 +21,7 @@ from itertools import chain
- from collections import defaultdict
-
- from docutils import nodes, utils
-+from docutils.nodes import math_block
- from docutils.transforms import Transform
- from docutils.parsers.rst import Directive, directives
- from docutils.parsers.rst.roles import code_role #, set_classes
-@@ -34,7 +35,6 @@ from sphinx.util.logging import getLogge
- from sphinx.directives import ObjectDescription
- from sphinx.domains import Domain, ObjType, Index
- from sphinx.domains.std import token_xrefs
--from sphinx.ext import mathbase
-
- from . import coqdoc
- from .repl import ansicolors
-@@ -74,8 +74,8 @@ def make_target(objtype, targetid):
- return "coq:{}.{}".format(objtype, targetid)
-
- def make_math_node(latex, docname, nowrap):
-- node = mathbase.displaymath()
-- node['latex'] = latex
-+ node = math_block()
-+ node['text'] = latex
- node['label'] = None # Otherwise equations are numbered
- node['nowrap'] = nowrap
- node['docname'] = docname
-@@ -1249,11 +1249,11 @@ def setup(app):
+@@ -1418,11 +1418,11 @@ def setup(app):
app.connect('doctree-resolved',
CoqtopBlocksTransform.merge_consecutive_coqtop_blocks)
# Add extra styles
diff --git a/coq.spec b/coq.spec
index a922966..4e9e94a 100644
--- a/coq.spec
+++ b/coq.spec
@@ -2,7 +2,6 @@
%global camlsuffix opt
%else
%global camlsuffix byte
-%global debug_package %{nil}
%endif
# .coqide-gtk2rc produces an rpmlint warning due to its name,
@@ -12,8 +11,8 @@
%global _python_bytecompile_extra 0
Name: coq
-Version: 8.11.2
-Release: 5%{?dist}
+Version: 8.12.0
+Release: 1%{?dist}
Summary: Proof management system
License: LGPLv2
@@ -27,17 +26,22 @@ Source3: coqide.appdata.xml
Patch0: 0001-Sphinx-3-support.patch
BuildRequires: ocaml >= 4.08.0
+BuildRequires: ocaml-dune
BuildRequires: ocaml-findlib
BuildRequires: ocaml-lablgtk3-devel >= 3.0
BuildRequires: ocaml-lablgtk3-sourceview3-devel >= 3.0
BuildRequires: ocaml-num-devel
+BuildRequires: ocaml-ocamldoc
+BuildRequires: ocaml-ounit-devel
BuildRequires: csdp-tools
BuildRequires: desktop-file-utils
BuildRequires: libicns-utils
+BuildRequires: rsync
BuildRequires: time
# For documentation
BuildRequires: antlr4
+BuildRequires: fontconfig
BuildRequires: hevea
BuildRequires: latexmk
BuildRequires: python3-devel
@@ -79,9 +83,6 @@ Requires: texlive-base
Recommends: emacs-proofgeneral
-# Exclude 3 private ocaml interfaces that we don't Provide
-%global __requires_exclude ocaml\\\((Configwin_types|Interface|Richpp)\\\)
-
# These can be removed when Fedora 30 reaches EOL
Obsoletes: %{name}-emacs < 8.9.0-1
Provides: %{name}-emacs = %{version}-%{release}
@@ -93,15 +94,26 @@ 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.
+
+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 coqide-server
+Summary: The coqidetop language server
+Requires: %{name}%{?_isa} = %{version}-%{release}
+
+%description coqide-server %_desc
+
+This package provides the coqidetop language server, an implementation of
+Coq's XML protocol which allows clients, such as CoqIDE, to interact with
+Coq in a structured way.
%package coqide
Summary: Coqide IDE for Coq proof management system
-Requires: %{name} = %{version}-%{release}
+Requires: %{name}-coqide-server%{?_isa} = %{version}-%{release}
Requires: hicolor-icon-theme
Requires: xdg-utils
@@ -114,6 +126,10 @@ development of interactive proofs.
Summary: Documentation for Coq proof management system
License: Open Publication and LGPLv2+
BuildArch: noarch
+Requires: fontawesome-fonts-web
+Requires: font(fontawesome)
+Requires: font(lato)
+Requires: font(robotoslab)
%description doc %_desc
@@ -133,20 +149,16 @@ fixtimestamp() {
rm -f $1.orig
}
-# Fix a Makefile rule that causes installation to fail
-sed -ri '/FULLCONFIGDIR/s/OLDROOT|COQINSTALLPREFIX/&2/g' Makefile.install
-
-# Use Fedora compiler and linker flags. Fix broken CAML_LD_LIBRARY_PATH.
+# Use Fedora compiler and linker flags
sed -e 's|-Wall.*-O2|%{optflags} -Wno-unused|' \
-e "s|-lunix|& -ccopt '$RPM_LD_FLAGS'|" \
- -e "s|'%s/kernel/byterun'|%s/kernel/byterun|" \
-i configure.ml
# Make sure debuginfo is generated
sed -i 's,-shared,& -g,g' tools/CoqMakefile.in Makefile.build
# Do not invoke env
-for f in dev/tools/update-compat.py doc/tools/coqrst/notations/fontsupport.py;
+for f in doc/tools/coqrst/notations/fontsupport.py;
do
sed -i.orig 's,/usr/bin/env python2,%{python3},' $f
fixtimestamp $f
@@ -156,7 +168,13 @@ for f in $(grep -Frl '%{_bindir}/env'); do
fixtimestamp $f
done
-%build
+# Update the oUnit name
+sed -i 's/oUnit/ounit2/' test-suite/Makefile
+
+# Work around a bad path
+sed -i.orig "s,-q,& --coqlib_path $PWD/_build/default," doc/stdlib/dune
+
+# Change dune's configure invocation
%ifarch %{ocaml_native_compiler}
%global opt_option -native-compiler yes -natdynlink yes -coqide opt
%else
@@ -164,50 +182,80 @@ done
%endif
%global coqdocdir %{?_pkgdocdir}%{!?_pkgdocdir:%{_docdir}/coq-%{version}}
-%global coqdatadir %{_libdir}/coq
-
-./configure -prefix %{_prefix} \
- -libdir %{coqdatadir} \
- -bindir %{_bindir} \
- -mandir %{_mandir} \
- -docdir %{coqdocdir} \
- -configdir %{_sysconfdir}/xdg/%{name} \
- -coqdocdir %{_texmf_main}/tex/latex \
- %{opt_option} \
- -browser "xdg-open %s" \
- -with-doc yes
+sed -i 's,-native-compiler no,-prefix %{_prefix} -libdir %{_libdir}/ocaml/coq -docdir
%{coqdocdir} -configdir %{_sysconfdir}/xdg/%{name} -coqdocdir
%{_texmf_main}/tex/latex/misc %{opt_option} -browser "xdg-open %s" -with-doc
yes,' config/dune
+
+%build
# Regenerate ANTLR files
cd doc/tools/coqrst/notations
antlr4 -Dlanguage=Python3 -visitor -no-listener TacticNotations.g
cd -
-export LD_LIBRARY_PATH=%{_libdir}/ocaml/stublibs
-export CAML_LD_LIBRARY_PATH=$PWD/kernel/byterun:${CAML_LD_LIBRARY_PATH}
-export SPHINXWARNERROR=0
+export SPHINXWARNOPT="-w$PWD/sphinx-warn.log"
+dune build %{?_smp_mflags}
+
+# Relink the stublib with RPM_LD_FLAGS
+cd _build/default/kernel/byterun
+ocamlmklib -g -ldopt "$RPM_LD_FLAGS" -o byterun_stubs $(ar t
libbyterun_stubs.a)
+cd -
-# Gross hack to work around intermittent build failures. See
-#
https://lists.fedoraproject.org/archives/list/devel@lists.fedoraproject.o...
-# for details. Revert to a single make invocation once the problem is
-# identified and fixed.
-make world VERBOSE=1 || make world VERBOSE=1 || make world VERBOSE=1
+# Undo the bad path workaround now that we're done
+mv doc/stdlib/dune.orig doc/stdlib/dune
%install
-make COQINSTALLPREFIX="%{buildroot}%{_prefix}" OLDROOT="%{_prefix}"
\
- COQINSTALLPREFIX2="%{buildroot}%{_sysconfdir}"
OLDROOT2="%{_sysconfdir}" \
- install
+# Installing with dune fails due to https://github.com/ocaml/dune/issues/1868.
+# We fake dune out by telling it not to install documentation, install, then
+# put the original file back.
+cp -p _build/default/coq-doc.install _build/default/coq-doc.install.orig
+chmod u+w _build/default/coq-doc.install
+sed -ri '/(html|pdf)/d' _build/default/coq-doc.install
+dune install --destdir=%{buildroot}
+mv _build/default/coq-doc.install.orig _build/default/coq-doc.install
# Fix permissions
-if [ -e %{buildroot}%{coqdatadir}/kernel/byterun/dllcoqrun.so ]; then
- chmod a+x %{buildroot}%{coqdatadir}/kernel/byterun/dllcoqrun.so
-fi
+%ifarch %{ocaml_native_compiler}
+find %{buildroot}%{_libdir}/ocaml -name \*.cmxs -exec chmod a+x {} \+
+%endif
+chmod a+x %{buildroot}%{_libdir}/ocaml/coq/tools/make*.py
+
+# Install the LaTeX style file
+mkdir -p %{buildroot}%{_texmf_main}/tex/latex/misc
+cp -p tools/coqdoc/coqdoc.sty %{buildroot}%{_texmf_main}/tex/latex/misc
+
+# Make a directory for site-wide configuration files
+mkdir -p %{buildroot}%{_sysconfdir}/xdg/coq
-# Use hardlinks rather than copying binaries
+# We install the documentation with the doc macro
+rm -fr %{buildroot}%{_prefix}/doc
+
+# Prepare the documentation for installation
+cp -Lpr _build/install/default/doc/coq-doc/html html
+find html -name .buildinfo -o -name .doctrees -exec rm -fr {} \+
+
+# Do not bundle fonts into the documentation
+cd html/refman/_static/fonts
+for suffix in eot svg ttf woff woff2; do
+ rm fontawesome-webfont.$suffix
+ ln -s %{_datadir}/fonts/fontawesome/fontawesome-webfont.$suffix .
+done
+rm {Lato,RobotoSlab}/*.ttf
+ln -s $(fc-match -f "%%{file}" "lato:bold") Lato/lato-bold.ttf
+ln -s $(fc-match -f "%%{file}" "lato:bold:italic")
Lato/lato-bolditalic.ttf
+ln -s $(fc-match -f "%%{file}" "lato:italic") Lato/lato-italic.ttf
+ln -s $(fc-match -f "%%{file}" "lato") Lato/lato-regular.ttf
+ln -s $(fc-match -f "%%{file}" "robotoslab:bold")
RobotoSlab/roboto-slab-v7-bold.ttf
+ln -s $(fc-match -f "%%{file}" "robotoslab")
RobotoSlab/roboto-slab-v7-regular.ttf
+cd -
+
+# Use links rather than copying binaries
%ifarch %{ocaml_native_compiler}
-for fil in coqtop coqidetop; do
+for fil in coqtop; do
rm -f %{buildroot}%{_bindir}/$fil
- ln %{buildroot}%{_bindir}/$fil.opt %{buildroot}%{_bindir}/$fil
+ ln %{buildroot}%{_bindir}/$fil.%{camlsuffix} %{buildroot}%{_bindir}/$fil
done
+rm %{buildroot}%{_libdir}/ocaml/coq/user-contrib/Ltac2/ltac2_plugin.cmxs
+ln -s ../../plugins/ltac2/ltac2_plugin.cmxs \
+ %{buildroot}%{_libdir}/ocaml/coq/user-contrib/Ltac2
%endif
# Install desktop icons
@@ -231,57 +279,38 @@ install -pm 644 %{SOURCE3} %{buildroot}%{_datadir}/appdata
mkdir -p %{buildroot}%{_datadir}/mime/packages
cp -p %{SOURCE2} %{buildroot}%{_datadir}/mime/packages
-# Install main Coq .v files
-for f in `find plugins theories -name '*.v' -type f`; do
-mkdir -p %{buildroot}%{coqdatadir}/`dirname $f` && cp -p $f
%{buildroot}%{coqdatadir}/`dirname $f`
-done
-
-# Install Ltac2 files missed by the makefiles
-cp -a user-contrib/Ltac2/.coq-native \
- %{buildroot}%{coqdatadir}/user-contrib/Ltac2
-
-# Install tutorial code
-%global tutorialcodedir %{coqdatadir}/RecTutorial
-if [ ! -d %{buildroot}%{tutorialcodedir} ]; then
- mkdir -p %{buildroot}%{tutorialcodedir}
-fi
-cp -p test-suite/success/RecTutorial.v %{buildroot}%{tutorialcodedir}
-
-# Install documentation not installed by install-doc in Makefile
-for f in dev/doc/changes.md CREDITS README.md;
-do cp -p $f %{buildroot}%{coqdocdir};
+# Install the language bindings
+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
-# We don't need both PostScript and PDF documentation
-rm -fr %{buildroot}%{coqdocdir}/ps
-
-# We don't need a hidden Sphinx marker
-rm -f %{buildroot}%{coqdocdir}/sphinx/html/.buildinfo
+# Install the style file
+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}%{coqdatadir}/tools
+%py_byte_compile %{python3} %{buildroot}%{_libdir}/ocaml/coq/tools
%files
-# DON'T use the doc macro here or else it wipes out all the other documentation
installed!
+%doc CREDITS README.md dev/doc/changes.md
%license LICENSE
-%{coqdatadir}/
-%{_datadir}/%{name}/
-%{_bindir}/coqc
-%{_bindir}/coqchk
+%{_libdir}/ocaml/coq/
+%{_libdir}/ocaml/stublibs/dllbyterun_stubs.so
+%{_bindir}/coqc*
%{_bindir}/coqdep
%{_bindir}/coqdoc
-%{_bindir}/coqidetop
-%{_bindir}/coqidetop.%{camlsuffix}
%{_bindir}/coq_makefile
%{_bindir}/coqpp
%{_bindir}/coqproofworker.%{camlsuffix}
%{_bindir}/coqqueryworker.%{camlsuffix}
%{_bindir}/coqtacticworker.%{camlsuffix}
%{_bindir}/coq-tex
-%{_bindir}/coqtop
-%{_bindir}/coqtop.%{camlsuffix}
+%{_bindir}/coqtop*
%{_bindir}/coqwc
%{_bindir}/coqworkmgr
+%{_bindir}/csdpcert
+%{_bindir}/ocamllibdep
%{_bindir}/votour
%{_mandir}/man1/coqc.1*
%{_mandir}/man1/coqchk.1*
@@ -293,44 +322,44 @@ rm -f %{buildroot}%{coqdocdir}/sphinx/html/.buildinfo
%{_mandir}/man1/coqtop.byte.1*
%{_mandir}/man1/coqtop.opt.1*
%{_mandir}/man1/coqwc.1*
-%exclude %{coqdatadir}/ide/
-%ifarch %{ocaml_native_compiler}
-%exclude %{coqdatadir}/*/*.cmxa
-%exclude %{coqdatadir}/*/*.a
-%endif
-%{_texmf_main}/tex/latex/coqdoc.sty
-# A few documentation files here should stay in the main package (and
-# are excluded from doc), but the bulk of the documentation is in the
-# doc subpackage
-%dir %{coqdocdir}
-%{coqdocdir}/changes.md
-%{coqdocdir}/CREDITS
-%{coqdocdir}/README.md
+%{_texmf_main}/tex/latex/misc/
+# This should really go in the doc subpackage, but because it is installed in
+# an arch-specific path, it cannot be part of a noarch package.
+%{_libdir}/ocaml/coq-doc/
+
+%files coqide-server
+%{_bindir}/coqidetop*
+%{_bindir}/fake_ide
+%{_libdir}/ocaml/coqide-server/
%files coqide
%doc ide/FAQ
%{_bindir}/coqide
+%{_datadir}/%{name}/
%{_datadir}/icons/hicolor/16x16/apps/coq.png
%{_datadir}/icons/hicolor/32x32/apps/coq.png
%{_datadir}/icons/hicolor/256x256/apps/coq.png
%{_datadir}/icons/hicolor/512x512/apps/coq.png
%{_mandir}/man1/coqide.1*
-%{coqdatadir}/ide/
-%exclude %{coqdatadir}/ide/ide.cmxa
-%exclude %{coqdatadir}/ide/ide.a
+%{_libdir}/ocaml/coqide/
%{_datadir}/appdata/coqide.appdata.xml
%{_datadir}/applications/coqide.desktop
+%{_datadir}/gtksourceview-3.0/language-specs/coq*.lang
+%{_datadir}/gtksourceview-3.0/styles/coq_style.xml
%{_datadir}/mime/packages/coq.xml
%{_sysconfdir}/xdg/coq/
%files doc
+%doc doc/README.md html
%license doc/LICENSE
-%{coqdocdir}/*
-%exclude %{coqdocdir}/changes.md
-%exclude %{coqdocdir}/CREDITS
-%exclude %{coqdocdir}/README.md
%changelog
+* Mon Aug 31 2020 Jerry James <loganjerry(a)gmail.com> - 8.12.0-1
+- Version 8.12.0
+- Build with dune
+- Add coqide-server subpackage
+- Unbundle fonts from the documentation
+
* Fri Aug 21 2020 Richard W.M. Jones <rjones(a)redhat.com> - 8.11.2-5
- OCaml 4.11.0 rebuild
diff --git a/sources b/sources
index eeadba7..649943c 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-SHA512 (coq-8.11.2.tar.gz) =
f8ab307b8e39ffda5f6984e187c1f8de1cb6dec5c322726dbbe535ee611683cfeeb9cee3e11ad83f5e44e843fc51e7e2d50b4ea69ab42fde38aaf3d0cf2dea3c
+SHA512 (coq-8.12.0.tar.gz) =
8a64624c578ce0ab781fb3b1f162bd8b095735ad891fdad2fb7c40849afbdc7c1360187c6b62a5ef2982566f4c6c78029240c611ae769943a5250af300eb1240