Accepting request 1199381 from science

- Update to version 8.20.0. The most impactful changes are:
  * A mechanism to add user-defined rewrite rules to Coq's reduction
    mechanisms; see chapter "User-defined rewrite rules".
  * Support for primitive strings in terms.
  * Reduction of the bytecode segment size, which in turn means
    that `.vo` files might now be considerably smaller.
- Notable breaking changes:
  * Syntactic global references passed through the `using` clauses
    of `auto`-like tactics are now handled as plain references
    rather than interpreted terms. In particular, their typeclass
    arguments will not be inferred. In general, the previous
    behaviour can be emulated by replacing `auto using foo` with
    `pose proof foo; auto`.
  * Argument order for the Ltac2 combinators `List.fold_left2` and
    `List.fold_right2` changed to be the same as in OCaml.
  * Importing a module containing a mutable Ltac2 definition does
    not undo its mutations. Replace `Ltac2 mutable foo :=
    some_expr.` with `Ltac2 mutable foo := some_expr. Ltac2 Set foo
    := some_expr.` to recover the previous behaviour.
  * Some renaming in the standard library. Deprecations are
    provided for a smooth transition.
- For more details, see the change log in coq-doc.

OBS-URL: https://build.opensuse.org/request/show/1199381
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/coq?expand=0&rev=29

coq-8.19.2.tar.gz

@@ -1,3 +0,0 @@
-version https://git-lfs.github.com/spec/v1
-oid sha256:18035624bcda4f8cffe5f348e02f0ae2503af1c40de165788d7d45578e6c5725
-size 7678311

coq-8.20.0.tar.gz

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:b08b364e6d420c58578d419247c5a710f4248bab962a46e542d452edac9e7914
+size 7839432

coq-refman-8.19.2.tar.xz

@@ -1,3 +0,0 @@
-version https://git-lfs.github.com/spec/v1
-oid sha256:d192cf2fd441f441cd4bd91672cd46ed1d8744bff132bace7aae3741ec4941de
-size 7665520

coq-refman-8.20.0.tar.xz

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:7ff1da16e6483c7ea2ffc75b7254690041b206f4330b0ea02ef74b567a57fcf3
+size 7788608

coq-stdlib-8.19.2.tar.xz

@@ -1,3 +0,0 @@
-version https://git-lfs.github.com/spec/v1
-oid sha256:9f0a46efc7ec7365ebb03937ab25a6994eb4f405853a28122f7c55859afb290f
-size 2176420

coq-stdlib-8.20.0.tar.xz

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:d0d9b5b24489633aa72fcaaddc462eb2d6f46ff55574c50fd520efb188dcfe7a
+size 2203608

coq.changes

@@ -1,3 +1,29 @@
+-------------------------------------------------------------------
+Thu Sep  5 20:49:31 UTC 2024 - Aaron Puchert <aaronpuchert@alice-dsl.net>
+
+- Update to version 8.20.0. The most impactful changes are:
+  * A mechanism to add user-defined rewrite rules to Coq's reduction
+    mechanisms; see chapter "User-defined rewrite rules".
+  * Support for primitive strings in terms.
+  * Reduction of the bytecode segment size, which in turn means
+    that `.vo` files might now be considerably smaller.
+- Notable breaking changes:
+  * Syntactic global references passed through the `using` clauses
+    of `auto`-like tactics are now handled as plain references
+    rather than interpreted terms. In particular, their typeclass
+    arguments will not be inferred. In general, the previous
+    behaviour can be emulated by replacing `auto using foo` with
+    `pose proof foo; auto`.
+  * Argument order for the Ltac2 combinators `List.fold_left2` and
+    `List.fold_right2` changed to be the same as in OCaml.
+  * Importing a module containing a mutable Ltac2 definition does
+    not undo its mutations. Replace `Ltac2 mutable foo :=
+    some_expr.` with `Ltac2 mutable foo := some_expr. Ltac2 Set foo
+    := some_expr.` to recover the previous behaviour.
+  * Some renaming in the standard library. Deprecations are
+    provided for a smooth transition.
+- For more details, see the change log in coq-doc.
+
 -------------------------------------------------------------------
 Sun Jun 30 17:20:06 UTC 2024 - Aaron Puchert <aaronpuchert@alice-dsl.net>
 

coq.spec

@@ -26,7 +26,7 @@
 %endif
 
 Name:           coq
-Version:        8.19.2
+Version:        8.20.0
 Release:        0
 Summary:        Proof Assistant based on the Calculus of Inductive Constructions
 License:        LGPL-2.1-only
@@ -44,7 +44,7 @@ BuildRequires:  fdupes
 BuildRequires:  make >= 3.81
 BuildRequires:  ocaml >= 4.09.0
 BuildRequires:  ocaml-camlp5-devel >= 5.08
-BuildRequires:  ocaml-dune >= 2.9
+BuildRequires:  ocaml-dune >= 3.6.1
 BuildRequires:  ocaml-rpm-macros
 BuildRequires:  ocamlfind(findlib)
 BuildRequires:  ocamlfind(zarith)
@@ -222,7 +222,6 @@ rm -r %{buildroot}%{_docdir}/%{name}/refman/{.buildinfo,.doctrees,_sources}
 %{_bindir}/coqtimelog2html
 %{_bindir}/coqtop
 %{_bindir}/coqtop.byte
-%{_bindir}/coqtop.opt
 %{_bindir}/coqwc
 %{_bindir}/coqworker.opt
 %{_bindir}/coqworkmgr
@@ -241,7 +240,6 @@ rm -r %{buildroot}%{_docdir}/%{name}/refman/{.buildinfo,.doctrees,_sources}
 %{_mandir}/man1/coqdoc.1%{ext_man}
 %{_mandir}/man1/coqnative.1%{ext_man}
 %{_mandir}/man1/coqtop.1%{ext_man}
-%{_mandir}/man1/coqtop.opt.1%{ext_man}
 %{_mandir}/man1/coqwc.1%{ext_man}
 
 %dir %{_datadir}/texmf
@@ -265,6 +263,7 @@ rm -r %{buildroot}%{_docdir}/%{name}/refman/{.buildinfo,.doctrees,_sources}
 
 %files devel -f dir.list -f devel.list
 %{_libdir}/coq-core/revision
+%{_libdir}/coq-core/dev/ml_toplevel
 %{_libdir}/{%{dune_packages}}/{META,dune-package,opam}
 %{_libdir}/coq-core/tools/CoqMakefile.in