Script 'mail_helper' called by obssrc
Hello community,
here is the log from the commit of package coq for openSUSE:Factory checked in
at 2022-01-16 23:18:05
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Comparing /work/SRC/openSUSE:Factory/coq (Old)
and /work/SRC/openSUSE:Factory/.coq.new.1892 (New)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq"
Sun Jan 16 23:18:05 2022 rev:15 rq:946708 version:8.15.0
Changes:
--------
--- /work/SRC/openSUSE:Factory/coq/coq.changes 2021-12-13 20:50:32.988640810
+0100
+++ /work/SRC/openSUSE:Factory/.coq.new.1892/coq.changes 2022-01-16
23:19:03.502371383 +0100
@@ -1,0 +2,21 @@
+Sat Jan 15 18:03:24 UTC 2022 - Aaron Puchert <aaronpuch...@alice-dsl.net>
+
+- Update to version 8.15.0.
+ * The `apply with` tactic no longer renames arguments unless
+ the compatibility flag `Apply With Renaming` is set.
+ * Improvements to the `auto` tactic family, fixing `Hint Unfold`
+ behavior, and generalizing the use of discrimination nets.
+ * The `typeclasses eauto` tactic has a new `best_effort` option
+ allowing it to return partial solutions to a proof search
+ problem, depending on the mode declarations associated to each
+ constraint. This mode is used by typeclass resolution during
+ type inference to provide more precise error messages.
+ * Many commands and options were deprecated or removed after
+ deprecation and more consistently support locality attributes.
+ * The `Import` command is extended with `import_categories` to
+ select the components of a module to import or not, including
+ features such as hints, coercions, and notations.
+ * A visual Ltac debugger is now available in CoqIDE.
+ * For more details, see refman/changes.html in coq-doc.
+
+-------------------------------------------------------------------
Old:
----
coq-8.14.1.tar.gz
coq-refman-8.14.1.tar.xz
coq-stdlib-8.14.1.tar.xz
New:
----
coq-8.15.0.tar.gz
coq-refman-8.15.0.tar.xz
coq-stdlib-8.15.0.tar.xz
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Other differences:
------------------
++++++ coq.spec ++++++
--- /var/tmp/diff_new_pack.Xx1syp/_old 2022-01-16 23:19:04.202371728 +0100
+++ /var/tmp/diff_new_pack.Xx1syp/_new 2022-01-16 23:19:04.206371730 +0100
@@ -1,7 +1,7 @@
#
# spec file for package coq
#
-# Copyright (c) 2021 SUSE LLC
+# Copyright (c) 2022 SUSE LLC
# Copyright (c) 2012-2018 Peter Trommler, peter.trommler at ohm-hochschule.de
#
# All modifications and additions to the file contributed by third parties
@@ -20,7 +20,7 @@
%bcond_without ide
Name: coq
-Version: 8.14.1
+Version: 8.15.0
Release: 0
Summary: Proof Assistant based on the Calculus of Inductive
Constructions
License: LGPL-2.1-only
@@ -86,13 +86,11 @@
# TODO: Add -with-doc yes
./configure \
-prefix %{_prefix} \
- -bindir %{_bindir} \
-libdir %{_libdir}/coq \
-mandir %{_mandir} \
-datadir %{_datadir}/%{name} \
-docdir %{_docdir}/%{name} \
-configdir %{_sysconfdir}/xdg/%{name} \
- -coqdocdir %{_datadir}/texmf/tex/latex/misc \
%if %{with ide}
-coqide opt \
%else
@@ -138,8 +136,8 @@
sed -i '1s|^#!/usr/bin/env
*|#!/usr/bin/|;1s|^#!/usr/bin/python$|#!/usr/bin/python3|' \
%{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 installed LICENSE, we put it elsewhere.
+rm %{buildroot}%{_docdir}/%{name}/coq{-core,ide,ide-server}/LICENSE
# Remove superfluous man page.
rm %{buildroot}%{_mandir}/man1/coqtop.byte.1
@@ -195,7 +193,6 @@
%files -f dir.list -f runtime.list
%license LICENSE CREDITS
-%doc README.md
%{_bindir}/coq-tex
%{_bindir}/coq_makefile
@@ -238,6 +235,9 @@
%dir %{_datadir}/texmf/tex/latex/misc
%{_datadir}/texmf/tex/latex/misc/coqdoc.sty
+%dir %{_docdir}/%{name}
+%{_docdir}/%{name}/coq-core
+
%if %{with ide}
%files ide
%{_bindir}/coqide
@@ -248,6 +248,9 @@
%{_datadir}/applications/coq.desktop
%{_datadir}/icons/hicolor/256x256/apps/coq.png
%{_datadir}/mime/packages/coq.xml
+%dir %{_docdir}/%{name}
+%{_docdir}/%{name}/coqide
+%{_docdir}/%{name}/coqide-server
%endif
%files devel -f dir.list -f devel.list
@@ -256,6 +259,7 @@
%{_libdir}/coq-core/tools/CoqMakefile.in
%files doc
+%dir %{_docdir}/%{name}
%{_docdir}/%{name}/refman
%{_docdir}/%{name}/stdlib
++++++ coq-8.14.1.tar.gz -> coq-8.15.0.tar.gz ++++++
/work/SRC/openSUSE:Factory/coq/coq-8.14.1.tar.gz
/work/SRC/openSUSE:Factory/.coq.new.1892/coq-8.15.0.tar.gz differ: char 12,
line 1
++++++ coq-refman-8.14.1.tar.xz -> coq-refman-8.15.0.tar.xz ++++++
/work/SRC/openSUSE:Factory/coq/coq-refman-8.14.1.tar.xz
/work/SRC/openSUSE:Factory/.coq.new.1892/coq-refman-8.15.0.tar.xz differ: char
26, line 1
++++++ coq-stdlib-8.14.1.tar.xz -> coq-stdlib-8.15.0.tar.xz ++++++
++++ 142122 lines of diff (skipped)
