- Update to version 8.19.0. The most impactful changes:

* Sort polymorphism makes it possible to share common constructs
    over `Type`, `Prop` and `SProp`.
  * The notation `term%_scope` to set a scope only temporarily (in
    addition to `term%scope` for opening a scope applying to all
    subterms).
  * Tactics `lazy`, `simpl`, `cbn` and `cbv` and the associated
    `Eval` and `eval` reductions learned to do head reduction when
    given flag head.
  * New Ltac2 APIs, improved Ltac2 `exact` and dynamic building of
    Ltac2 term patterns.
  * New performance evaluation facilities: `Instructions` to count
    CPU instructions used by a command (Linux only) and Profiling
    system to produce trace files.
  * New command `Attributes` to assign attributes such as
    `deprecated` to a library file.
- Notable breaking changes:
  * `replace` with `by tac` does not automatically attempt to solve
    the generated equality subgoal using the hypotheses. Use `by
    first [assumption | symmetry;assumption | tac]` if you need the
    previous behaviour.
  * Removed old deprecated files from the standard library. 
- Use %fdupes in the documentation package.

OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=60

coq-8.18.0.tar.gz

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

coq-8.19.0.tar.gz

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

coq-refman-8.18.0.tar.xz

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

coq-refman-8.19.0.tar.xz

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

coq-stdlib-8.18.0.tar.xz

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

coq-stdlib-8.19.0.tar.xz

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

coq.changes

@@ -1,3 +1,30 @@
+-------------------------------------------------------------------
+Sun Jan 28 20:20:35 UTC 2024 - Aaron Puchert <aaronpuchert@alice-dsl.net>
+
+- Update to version 8.19.0. The most impactful changes:
+  * Sort polymorphism makes it possible to share common constructs
+    over `Type`, `Prop` and `SProp`.
+  * The notation `term%_scope` to set a scope only temporarily (in
+    addition to `term%scope` for opening a scope applying to all
+    subterms).
+  * `lazy`, `simpl`, `cbn` and `cbv` and the associated `Eval` and
+    `eval` reductions learned to do head reduction when given flag
+    `head`.
+  * New Ltac2 APIs, improved Ltac2 `exact` and dynamic building of
+    Ltac2 term patterns.
+  * New performance evaluation facilities: `Instructions` to count
+    CPU instructions used by a command and Profiling system to
+    produce trace files.
+  * New command `Attributes` to assign attributes such as
+    `deprecated` to a library file.
+- Notable breaking changes:
+  * `replace` with `by tac` does not automatically attempt to solve
+    the generated equality subgoal using the hypotheses. Use `by
+    first [assumption | symmetry;assumption | tac]` if you need the
+    previous behaviour.
+  * Removed old deprecated files from the standard library. 
+- Use %fdupes in the documentation package.
+
 -------------------------------------------------------------------
 Sun Nov 12 22:52:11 UTC 2023 - Aaron Puchert <aaronpuchert@alice-dsl.net>
 

coq.spec

@@ -1,9 +1,9 @@
 #
 # spec file for package coq
 #
-# Copyright (c) 2023 SUSE LLC
+# Copyright (c) 2024 SUSE LLC
 # Copyright (c) 2012-2018 Peter Trommler, peter.trommler at ohm-hochschule.de
-# Copyright (c) 2023 Aaron Puchert <aaronpuchert@alice-dsl.net>
+# Copyright (c) 2024 Aaron Puchert <aaronpuchert@alice-dsl.net>
 #
 # All modifications and additions to the file contributed by third parties
 # remain the property of their copyright owners, unless otherwise agreed
@@ -26,7 +26,7 @@
 %endif
 
 Name:           coq
-Version:        8.18.0
+Version:        8.19.0
 Release:        0
 Summary:        Proof Assistant based on the Calculus of Inductive Constructions
 License:        LGPL-2.1-only
@@ -40,6 +40,7 @@ Source50:       coq-refman-%{version}.tar.xz
 Source51:       coq-stdlib-%{version}.tar.xz
 Source100:      %{name}-rpmlintrc
 BuildRequires:  desktop-file-utils
+BuildRequires:  fdupes
 BuildRequires:  make >= 3.81
 BuildRequires:  ocaml >= 4.09.0
 BuildRequires:  ocaml-camlp5-devel >= 5.08
@@ -180,14 +181,17 @@ find %{buildroot}%{_libdir} -name '*.a' \
                 -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
-# svn export https://github.com/coq/doc/trunk/V%{version}/stdlib
+# git clone --filter=tree:0 --sparse https://github.com/coq/doc.git
+# pushd doc
+# git sparse-checkout add V%{version}
+# cd V%{version}
 # tar --sort=name --owner=0 --group=0 --mtime="@$(stat -c %%Y refman/index.html)" \
 #     --pax-option=exthdr.name=%d/PaxHeaders/%f,delete=atime,delete=ctime \
-#     -cJf coq-refman-%{version}.tar.xz refman
+#     -cJf ../../coq-refman-%{version}.tar.xz refman
 # tar --sort=name --owner=0 --group=0 --mtime="@$(stat -c %%Y stdlib/index.html)" \
 #     --pax-option=exthdr.name=%d/PaxHeaders/%f,delete=atime,delete=ctime \
-#     -cJf coq-stdlib-%{version}.tar.xz stdlib
+#     -cJf ../../coq-stdlib-%{version}.tar.xz stdlib
+# popd
 
 # Drop some CSS files and headers in stdlib documentation, add some margin directly.
 find stdlib/ -name '*.html' -exec sed -i '
@@ -201,6 +205,8 @@ mkdir -p %{buildroot}%{_docdir}/%{name}
 cp -r refman stdlib %{buildroot}%{_docdir}/%{name}
 rm -r %{buildroot}%{_docdir}/%{name}/refman/{.buildinfo,.doctrees,_sources}
 
+%fdupes %{buildroot}%{_docdir}/%{name}/refman
+
 %files -f dir.list -f runtime.list
 %license LICENSE CREDITS