Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package coq for openSUSE:Factory checked in at 2024-01-29 22:28:51 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.1815 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Mon Jan 29 22:28:51 2024 rev:26 rq:1142140 version:8.19.0 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2023-11-13 22:25:33.233848136 +0100 +++ /work/SRC/openSUSE:Factory/.coq.new.1815/coq.changes 2024-01-29 22:29:30.502515231 +0100 @@ -1,0 +2,27 @@ +Sun Jan 28 20:20:35 UTC 2024 - Aaron Puchert <[email protected]> + +- 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. + +------------------------------------------------------------------- Old: ---- coq-8.18.0.tar.gz coq-refman-8.18.0.tar.xz coq-stdlib-8.18.0.tar.xz New: ---- coq-8.19.0.tar.gz coq-refman-8.19.0.tar.xz coq-stdlib-8.19.0.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.8U7lAF/_old 2024-01-29 22:29:31.446549400 +0100 +++ /var/tmp/diff_new_pack.8U7lAF/_new 2024-01-29 22:29:31.450549544 +0100 @@ -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 <[email protected]> +# Copyright (c) 2024 Aaron Puchert <[email protected]> # # 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 @@ 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 @@ -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 @@ cp -r refman stdlib %{buildroot}%{_docdir}/%{name} rm -r %{buildroot}%{_docdir}/%{name}/refman/{.buildinfo,.doctrees,_sources} +%fdupes %{buildroot}%{_docdir}/%{name} + %files -f dir.list -f runtime.list %license LICENSE CREDITS ++++++ coq-8.18.0.tar.gz -> coq-8.19.0.tar.gz ++++++ /work/SRC/openSUSE:Factory/coq/coq-8.18.0.tar.gz /work/SRC/openSUSE:Factory/.coq.new.1815/coq-8.19.0.tar.gz differ: char 29, line 1 ++++++ coq-refman-8.18.0.tar.xz -> coq-refman-8.19.0.tar.xz ++++++ /work/SRC/openSUSE:Factory/coq/coq-refman-8.18.0.tar.xz /work/SRC/openSUSE:Factory/.coq.new.1815/coq-refman-8.19.0.tar.xz differ: char 25, line 1 ++++++ coq-stdlib-8.18.0.tar.xz -> coq-stdlib-8.19.0.tar.xz ++++++ ++++ 107967 lines of diff (skipped)
