diff --git a/_constraints b/_constraints
index e83f235..642c0fb 100644
--- a/_constraints
+++ b/_constraints
@@ -2,7 +2,10 @@
- 800
+ 900
+
+ 4
+
-
\ No newline at end of file
+
diff --git a/coq-8.13.2.tar.gz b/coq-8.13.2.tar.gz
deleted file mode 100644
index a0f6a7d..0000000
--- a/coq-8.13.2.tar.gz
+++ /dev/null
@@ -1,3 +0,0 @@
-version https://git-lfs.github.com/spec/v1
-oid sha256:1e7793d8483f1e939f62df6749f843df967a15d843a4a5acb024904b76e25a14
-size 6952855
diff --git a/coq-8.14.0.tar.gz b/coq-8.14.0.tar.gz
new file mode 100644
index 0000000..d6b68ca
--- /dev/null
+++ b/coq-8.14.0.tar.gz
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c
+size 7062331
diff --git a/coq-refman-8.13.2.tar.xz b/coq-refman-8.13.2.tar.xz
deleted file mode 100644
index e2a9613..0000000
--- a/coq-refman-8.13.2.tar.xz
+++ /dev/null
@@ -1,3 +0,0 @@
-version https://git-lfs.github.com/spec/v1
-oid sha256:209cf16781dc604271795e1c6eeab8662d3b5d3d887b9f2df78aa18959c54f66
-size 8992636
diff --git a/coq-refman-8.14.0.tar.xz b/coq-refman-8.14.0.tar.xz
new file mode 100644
index 0000000..496ca4a
--- /dev/null
+++ b/coq-refman-8.14.0.tar.xz
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:1eaffc8ea592cdfcab4a87750c42693739321f2aaf586ecf0d699f00e519a42e
+size 9055764
diff --git a/coq-rpmlintrc b/coq-rpmlintrc
index 1a0ddc9..7df8eb5 100644
--- a/coq-rpmlintrc
+++ b/coq-rpmlintrc
@@ -4,4 +4,4 @@ from Config import *
# Unfortunate choice, but we can't easily change that.
addFilter("hidden-file-or-dir .*/.coq-native")
# These are loaded manually by the OCaml runtime and need no dependency information.
-addFilter("shared-lib-without-dependency-information .*\.cmxs")
+addFilter("shared-library-without-dependency-information .*\.cmxs")
diff --git a/coq-stdlib-8.13.2.tar.xz b/coq-stdlib-8.13.2.tar.xz
deleted file mode 100644
index a1f2886..0000000
--- a/coq-stdlib-8.13.2.tar.xz
+++ /dev/null
@@ -1,3 +0,0 @@
-version https://git-lfs.github.com/spec/v1
-oid sha256:a238e81a0b18e06a2cb741f5dc2807cda491ac695a092eeec05301bd1f1fcf8c
-size 2801528
diff --git a/coq-stdlib-8.14.0.tar.xz b/coq-stdlib-8.14.0.tar.xz
new file mode 100644
index 0000000..666e561
--- /dev/null
+++ b/coq-stdlib-8.14.0.tar.xz
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:44f41036dff00953f7cfe6d24e1c9ca3948ba93d2dccb07e159a03c1388997c2
+size 2882516
diff --git a/coq.changes b/coq.changes
index 10b7b22..cb69850 100644
--- a/coq.changes
+++ b/coq.changes
@@ -1,3 +1,30 @@
+-------------------------------------------------------------------
+Wed Oct 20 21:31:46 UTC 2021 - Aaron Puchert
+
+- Update to version 8.14.0.
+ * The internal representation of match has changed to a more
+ space-efficient and cleaner structure, allowing the fix of a
+ completeness issue with cumulative inductive types in the type-
+ checker. The internal representation is now closer to the user-
+ level view of match, where the argument context of branches and
+ the inductive binders in and as do not carry type annotations.
+ * A new coqnative binary performs separate native compilation of
+ libraries, starting from a .vo file. It is supported by
+ coq_makefile.
+ * Improvements to typeclasses and canonical structure resolution,
+ allowing more terms to be considered as classes or keys.
+ * More control over notations declarations and support for
+ primitive types in string and number notations.
+ * Removal of deprecated tactics, notably omega, which has been
+ replaced by a greatly improved lia, along with many bug fixes.
+ * New Ltac2 APIs for interaction with Ltac1, manipulation of
+ inductive types and printing.
+ * Many changes and additions to the standard library in the
+ numbers, vectors and lists libraries. A new signed primitive
+ integers library Sint63 is available in addition to the
+ unsigned Uint63 library.
+ * For more details, see refman/changes.html in coq-doc.
+
-------------------------------------------------------------------
Sat Sep 4 12:51:43 UTC 2021 - Aaron Puchert
diff --git a/coq.spec b/coq.spec
index ee29d7b..9c4b697 100644
--- a/coq.spec
+++ b/coq.spec
@@ -20,7 +20,7 @@
%bcond_without ide
Name: coq
-Version: 8.13.2
+Version: 8.14.0
Release: 0
Summary: Proof Assistant based on the Calculus of Inductive Constructions
License: LGPL-2.1-only
@@ -36,14 +36,12 @@ BuildRequires: desktop-file-utils
BuildRequires: make >= 3.81
BuildRequires: ocaml >= 4.05.0
BuildRequires: ocaml-camlp5-devel >= 5.08
+BuildRequires: ocaml-dune >= 2.5.1
BuildRequires: ocamlfind(findlib)
BuildRequires: ocamlfind(zarith)
%if %{with ide}
BuildRequires: update-desktop-files
-BuildRequires: ocamlfind(lablgtk3)
-BuildRequires: pkgconfig(gdk-3.0)
-BuildRequires: pkgconfig(gtk+-3.0)
-BuildRequires: pkgconfig(gtksourceview-3.0)
+BuildRequires: ocamlfind(lablgtk3-sourceview3)
%endif
%description
@@ -57,7 +55,7 @@ For a graphical interface install %{name}-ide.
%package ide
Summary: IDE for The Coq Proof Assistant
Group: Productivity/Scientific/Math
-Requires: %{name} = %{version}-%{release}
+Requires: %{name} = %{version}
%description ide
The Coq Integrated Development Interface is a graphical interface for the Coq proof assistant.
@@ -65,7 +63,7 @@ The Coq Integrated Development Interface is a graphical interface for the Coq pr
%package devel
Summary: Development files for coq
Group: Development/Libraries/Other
-Requires: %{name} = %{version}-%{release}
+Requires: %{name} = %{version}
Requires: ocaml >= 4.05.0
Requires: ocamlfind(findlib)
@@ -82,14 +80,12 @@ HTML reference manual for Coq and full documentation of the standard library.
%prep
%setup -q -a 50 -a 51
-# META for ocamlfind doesn't contain a version, so configure.ml fails. We patch that.
-sed -i 's/v, _ = tryrun camlexec.find \["query"; "-format"; "%v"; "lablgtk3"\]/v = "%{pkg_version ocamlfind(lablgtk3)}"/' \
- configure.ml
%build
export CFLAGS='%{optflags}'
# TODO: Add -with-doc yes
./configure \
+ -prefix %{_prefix} \
-bindir %{_bindir} \
-libdir %{_libdir}/coq \
-mandir %{_mandir} \
@@ -109,13 +105,12 @@ export CFLAGS='%{optflags}'
make %{?_smp_mflags} world
%install
-%if %{with ide}
-# Fixup dependencies before we install. Some are apparently not detected.
-sed -i 's#^ide/ide_MLLIB_DEPENDENCIES:=.*$#& ide/configwin_types ide/protocol/richpp#' \
- .mllibfiles.d
-%endif
+make DESTDIR=%{buildroot} install
-make COQINSTALLPREFIX=%{buildroot} install
+# For some reason, some of the files are installed into /usr/lib.
+%if "${_libdir}" != "${_prefix}/lib"
+mv %{buildroot}%{_prefix}/lib/* %{buildroot}%{_libdir}
+%endif
%if %{with ide}
%suse_update_desktop_file -i %{SOURCE1}
@@ -124,7 +119,7 @@ install -D -m 644 %{SOURCE2} %{buildroot}%{_datadir}/mime/packages/coq.xml
mkdir -p %{buildroot}%{_datadir}/icons/hicolor/256x256/apps
ln -s %{_datadir}/coq/coq.png %{buildroot}%{_datadir}/icons/hicolor/256x256/apps/coq.png
%else
-rm %{buildroot}%{_bindir}/coqidetop{,.opt} %{buildroot}%{_mandir}/man1/coqide.1
+rm %{buildroot}%{_bindir}/coqidetop{.byte,.opt}
%endif
# Sometimes we get identical x and x.opt files, replace by symlink x -> x.opt.
@@ -139,9 +134,12 @@ done
# Fix executable bit and shebangs, preferring python3.
# (https://www.python.org/dev/peps/pep-0394/#for-python-runtime-distributors)
-chmod -x %{buildroot}%{_libdir}/%{name}/tools/TimeFileMaker.py
+chmod -x %{buildroot}%{_libdir}/coq-core/tools/TimeFileMaker.py
sed -i '1s|^#!/usr/bin/env *|#!/usr/bin/|;1s|^#!/usr/bin/python$|#!/usr/bin/python3|' \
- %{buildroot}%{_libdir}/%{name}/tools/make-{one-time-file,both-{time,single-timing}-files}.py
+ %{buildroot}%{_libdir}/coq-core/tools/make-{one-time-file,both-{time,single-timing}-files}.py
+
+# Remove /usr/doc that's not FHS-compliant, also we have the files elsewhere.
+rm -r %{buildroot}%{_prefix}/doc
# Remove superfluous man page.
rm %{buildroot}%{_mandir}/man1/coqtop.byte.1
@@ -151,24 +149,27 @@ find %{buildroot}%{_libdir}/coq -empty -name '*.vos' -delete
# Build lists of runtime and devel files by ending.
# Compiled theories and shared objects are needed at runtime.
-find %{buildroot}%{_libdir}/coq/{plugins,theories} -type d | \
- sed "s|%{buildroot}|%%dir |g" >runtime.list
-find %{buildroot}%{_libdir}/coq -name '*.cmxs' \
+find %{buildroot}%{_libdir} -type d | sed "s|%{buildroot}|%%dir |g" >dir.list
+sed -i '1d; /coq-core\/tools/d' dir.list
+find %{buildroot}%{_libdir} -name '*.cmxs' \
-or -name '*.so' \
- -or -name '*.vo' | sed "s|%{buildroot}||g" >>runtime.list
+ -or -name '*.vo' | sed "s|%{buildroot}||g" >runtime.list
# Object files, static libraries and import definitions are only needed for development.
# For now, we also put the standard library Coq sources here, since the runtime
# package contains the HTML documentation for the standard library.
-find %{buildroot}%{_libdir}/coq -type d | sed "s|%{buildroot}|%%dir |g" >devel.list
-find %{buildroot}%{_libdir}/coq -name '*.a' \
+find %{buildroot}%{_libdir} -name '*.a' \
-or -name '*.cma' \
-or -name '*.cmi' \
+ -or -name '*.cmt' \
+ -or -name '*.cmti' \
-or -name '*.cmx' \
-or -name '*.cmxa' \
-or -name '*.glob' \
+ -or -name '*.ml' \
+ -or -name '*.mli' \
-or -name '*.o' \
- -or -name '*.v' | sed "s|%{buildroot}||g" >>devel.list
+ -or -name '*.v' | sed "s|%{buildroot}||g" >devel.list
# Until we can build it, we fetch the documentation from the official website:
# svn export https://github.com/coq/doc/trunk/V%{version}/refman
@@ -182,45 +183,43 @@ find %{buildroot}%{_libdir}/coq -name '*.a' \
# Drop some CSS files and headers in stdlib documentation, add some margin directly.
find stdlib/ -name '*.html' -exec sed -i '
-s#//coq.inria.fr/sites/all/themes/coq/coqdoc.css#/usr/lib64/coq/tools/coqdoc/coqdoc.css#
+s#//coq.inria.fr/sites/all/themes/coq/coqdoc.css#%{_libdir}/coq-core/tools/coqdoc/coqdoc.css#
//d
/