Script 'mail_helper' called by obssrc
Hello community,
here is the log from the commit of package coq for openSUSE:Factory checked in
at 2023-03-29 23:27:14
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Comparing /work/SRC/openSUSE:Factory/coq (Old)
and /work/SRC/openSUSE:Factory/.coq.new.31432 (New)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq"
Wed Mar 29 23:27:14 2023 rev:21 rq:1075082 version:8.17.0
Changes:
--------
--- /work/SRC/openSUSE:Factory/coq/coq.changes 2023-01-27 10:26:39.466844577
+0100
+++ /work/SRC/openSUSE:Factory/.coq.new.31432/coq.changes 2023-03-29
23:27:32.683567528 +0200
@@ -1,0 +2,20 @@
+Tue Mar 28 21:18:57 UTC 2023 - Aaron Puchert <aaronpuch...@alice-dsl.net>
+
+- Update to version 8.17.0.
+ * Fixed a logical inconsistency due to `vm_compute` in presence
+ of side-effects in the enviroment (e.g. using Back or Fail).
+ * It is now possible to dynamically enable or disable notations.
+ * Support multiple scopes in `Arguments` and `Bind Scope`.
+ * The tactics chapter of the manual has many improvements in
+ presentation and wording. The documented grammar is semi-
+ automatically checked for consistency with the implementation.
+ * Fixes to the `auto` and `eauto` tactics, to respect hint
+ priorities and the documented use of simple apply. This is a
+ potentially breaking change.
+ * New Ltac2 APIs, deep pattern-matching with `as` clauses and
+ handling of literals, support for record types and preterms.
+ * Move from :> to :: syntax for declaring typeclass fields as
+ instances, fixing a confusion with declaration of coercions.
+ * Standard library improvements.
+
+-------------------------------------------------------------------
Old:
----
coq-8.16.1.tar.gz
coq-refman-8.16.1.tar.xz
coq-stdlib-8.16.1.tar.xz
New:
----
coq-8.17.0.tar.gz
coq-refman-8.17.0.tar.xz
coq-stdlib-8.17.0.tar.xz
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Other differences:
------------------
++++++ coq.spec ++++++
--- /var/tmp/diff_new_pack.aH37zm/_old 2023-03-29 23:27:33.471571739 +0200
+++ /var/tmp/diff_new_pack.aH37zm/_new 2023-03-29 23:27:33.475571761 +0200
@@ -20,8 +20,13 @@
%bcond_without ide
+%global dune_packages coq,coq-core,coq-stdlib
+%if %{with ide}
+%global dune_packages %{dune_packages},coqide,coqide-server
+%endif
+
Name: coq
-Version: 8.16.1
+Version: 8.17.0
Release: 0
Summary: Proof Assistant based on the Calculus of Inductive
Constructions
License: LGPL-2.1-only
@@ -38,7 +43,7 @@
BuildRequires: make >= 3.81
BuildRequires: ocaml >= 4.09.0
BuildRequires: ocaml-camlp5-devel >= 5.08
-BuildRequires: ocaml-dune >= 2.5.1
+BuildRequires: ocaml-dune >= 2.9
BuildRequires: ocaml-rpm-macros
BuildRequires: ocamlfind(findlib)
BuildRequires: ocamlfind(zarith)
@@ -87,7 +92,6 @@
%build
export CFLAGS='%{optflags}'
-# TODO: Add -with-doc yes
./configure \
-prefix %{_prefix} \
-libdir %{_libdir}/coq \
@@ -95,24 +99,18 @@
-datadir %{_datadir}/%{name} \
-docdir %{_docdir}/%{name} \
-configdir %{_sysconfdir}/xdg/%{name} \
-%if %{with ide}
- -coqide opt \
-%else
- -coqide no \
-%endif
-native-compiler yes \
-natdynlink yes \
-browser "xdg-open %s"
+make %{?_smp_mflags} dunestrap
-make %{?_smp_mflags} world
+dune_release_pkgs='%{dune_packages}'
+%ocaml_dune_setup
+%ocaml_dune_build
%install
-make DESTDIR=%{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
+%global ocaml_standard_library %{_libdir}
+%ocaml_dune_install
%if %{with ide}
%suse_update_desktop_file -i %{SOURCE1}
@@ -121,8 +119,6 @@
install -D -m 644 %{SOURCE3} %{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{.byte,.opt}
%endif
# Sometimes we get identical x and x.opt files, replace by symlink x -> x.opt.
@@ -141,9 +137,6 @@
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 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
@@ -208,13 +201,11 @@
%{_bindir}/coqdoc
%{_bindir}/coqnative
%{_bindir}/coqpp
-%{_bindir}/coqproofworker.opt
-%{_bindir}/coqqueryworker.opt
-%{_bindir}/coqtacticworker.opt
%{_bindir}/coqtop
%{_bindir}/coqtop.byte
%{_bindir}/coqtop.opt
%{_bindir}/coqwc
+%{_bindir}/coqworker.opt
%{_bindir}/coqworkmgr
%{_bindir}/csdpcert
%{_bindir}/ocamllibdep
@@ -240,9 +231,6 @@
%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
@@ -254,14 +242,11 @@
%{_datadir}/icons/hicolor/256x256/apps/coq.png
%{_datadir}/metainfo/fr.inria.coq.coqide.metainfo.xml
%{_datadir}/mime/packages/coq.xml
-%dir %{_docdir}/%{name}
-%{_docdir}/%{name}/coqide
-%{_docdir}/%{name}/coqide-server
%endif
%files devel -f dir.list -f devel.list
%{_libdir}/coq-core/revision
-%{_libdir}/{coq,coq-core,coq-stdlib,coqide,coqide-server}/{META,dune-package,opam}
+%{_libdir}/{%{dune_packages}}/{META,dune-package,opam}
%{_libdir}/coq-core/tools/CoqMakefile.in
%files doc
++++++ coq-8.16.1.tar.gz -> coq-8.17.0.tar.gz ++++++
/work/SRC/openSUSE:Factory/coq/coq-8.16.1.tar.gz
/work/SRC/openSUSE:Factory/.coq.new.31432/coq-8.17.0.tar.gz differ: char 14,
line 1
++++++ coq-refman-8.16.1.tar.xz -> coq-refman-8.17.0.tar.xz ++++++
/work/SRC/openSUSE:Factory/coq/coq-refman-8.16.1.tar.xz
/work/SRC/openSUSE:Factory/.coq.new.31432/coq-refman-8.17.0.tar.xz differ: char
26, line 1
++++++ coq-stdlib-8.16.1.tar.xz -> coq-stdlib-8.17.0.tar.xz ++++++
++++ 130655 lines of diff (skipped)
++++++ fr.inria.coq.coqide.metainfo.xml ++++++
--- /var/tmp/diff_new_pack.aH37zm/_old 2023-03-29 23:27:35.067580268 +0200
+++ /var/tmp/diff_new_pack.aH37zm/_new 2023-03-29 23:27:35.071580290 +0200
@@ -46,6 +46,7 @@
<url
type="contribute">https://github.com/coq/coq/blob/master/CONTRIBUTING.md</url>
<launchable type="desktop-id">fr.inria.coq.coqide.desktop</launchable>
<releases>
+ <release version="8.17.0" date="2023-03-27"/>
<release version="8.16.1" date="2022-11-25"/>
<release version="8.16.0" date="2022-09-05"/>
<release version="8.15.2" date="2022-05-31"/>
