Script 'mail_helper' called by obssrc
Hello community,
here is the log from the commit of package coq for openSUSE:Factory checked in
at 2021-02-08 11:47:41
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Comparing /work/SRC/openSUSE:Factory/coq (Old)
and /work/SRC/openSUSE:Factory/.coq.new.28504 (New)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq"
Mon Feb 8 11:47:41 2021 rev:9 rq:870152 version:8.13.0
Changes:
--------
--- /work/SRC/openSUSE:Factory/coq/coq.changes 2020-12-14 18:10:09.779687482
+0100
+++ /work/SRC/openSUSE:Factory/.coq.new.28504/coq.changes 2021-02-08
11:47:43.589739109 +0100
@@ -1,0 +2,36 @@
+Sun Feb 7 22:48:00 UTC 2021 - Aaron Puchert <aaronpuch...@alice-dsl.net>
+
+- Update to version 8.13.0.
+ * Introduction of primitive persistent arrays in the core
+ language, implemented using imperative persistent arrays.
+ * Introduction of definitional proof irrelevance for the equality
+ type defined in the SProp sort.
+ * Cumulative record and inductive type declarations can now
+ specify the variance of their universes.
+ * Various bugfixes and uniformization of behavior with respect to
+ the use of implicit arguments and the handling of existential
+ variables in declarations, unification and tactics.
+ * New warning for unused variables in catch-all match branches
+ that match multiple distinct patterns.
+ * New warning for Hint commands outside sections without a
+ locality attribute, whose goal is to eventually remove the
+ fragile default behavior of importing hints only when using
+ Require. The recommended fix is to declare hints as export,
+ instead of the current default global, meaning that they are
+ imported through Require Import only, not Require.
+ * General support for boolean attributes.
+ * Many improvements to the handling of notations, including
+ number notations, recursive notations and notations with
+ bindings. A new algorithm chooses the most precise notation
+ available to print an expression, which might introduce changes
+ in printing behavior.
+ * Tactic improvements in lia and its zify preprocessing step,
+ now supporting reasoning on boolean operators such as Z.leb and
+ supporting primitive integers Int63.
+ * Typing flags can now be specified per-constant / inductive.
+ * Improvements to the reference manual including updated syntax
+ descriptions that match Coq's grammar in several chapters, and
+ splitting parts of the tactics chapter to independent sections.
+- Add build flag to turn off building of the IDE.
+
+-------------------------------------------------------------------
Old:
----
coq-8.12.2.tar.gz
New:
----
coq-8.13.0.tar.gz
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Other differences:
------------------
++++++ coq.spec ++++++
--- /var/tmp/diff_new_pack.uIOOO9/_old 2021-02-08 11:47:44.329740309 +0100
+++ /var/tmp/diff_new_pack.uIOOO9/_new 2021-02-08 11:47:44.333740316 +0100
@@ -1,7 +1,7 @@
#
# spec file for package coq
#
-# Copyright (c) 2020 SUSE LLC
+# Copyright (c) 2021 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
@@ -17,8 +17,10 @@
#
+%bcond_without ide
+
Name: coq
-Version: 8.12.2
+Version: 8.13.0
Release: 0
Summary: Proof Assistant based on the Calculus of Inductive
Constructions
License: LGPL-2.1-only
@@ -29,25 +31,18 @@
Source2: coq.xml
Source100: %{name}-rpmlintrc
BuildRequires: desktop-file-utils
-# Required for standard coq:
BuildRequires: make >= 3.81
BuildRequires: ocaml >= 4.05.0
BuildRequires: ocaml-camlp5-devel >= 5.08
-# TODO: Build docs when antlr4-python3-runtime becomes available.
-#BuildRequires: python3-Sphinx
-#BuildRequires: python3-pexpect
-#BuildRequires: antlr4-python3-runtime
-#BuildRequires: python3-beautifulsoup4
-# Required for coq-ide:
-BuildRequires: update-desktop-files
BuildRequires: ocamlfind(findlib)
+BuildRequires: ocamlfind(zarith)
+%if %{with ide}
+BuildRequires: update-desktop-files
BuildRequires: ocamlfind(lablgtk3)
-BuildRequires: ocamlfind(num)
BuildRequires: pkgconfig(gdk-3.0)
BuildRequires: pkgconfig(gtk+-3.0)
BuildRequires: pkgconfig(gtksourceview-3.0)
-
-%global __requires_exclude
ocaml\\\((Interface|Sos_types|GtkSourceView2_types)\\\)
+%endif
%description
Proof assistant which allows to handle calculus assertions, check mechanically
@@ -76,9 +71,13 @@
%prep
%setup -q
+# META for ocamlfind doesn't contain a version, so configure.ml fails. We
patch that.
+sed -i 's/v, _ = tryrun camlexec.find \["query"; "-format"; "%v";
"lablgtk3"\]/v = "%{pkg_version ocamlfind(lablgtk3)}"/' \
+ configure.ml
%build
export CFLAGS='%{optflags}'
+# TODO: Add -with-doc yes
./configure \
-bindir %{_bindir} \
-libdir %{_libdir}/coq \
@@ -87,6 +86,11 @@
-docdir %{_docdir}/%{name} \
-configdir %{_sysconfdir}/xdg/%{name} \
-coqdocdir %{_datadir}/texmf/tex/latex/misc \
+%if %{with ide}
+ -coqide opt \
+%else
+ -coqide no \
+%endif
-native-compiler yes \
-natdynlink yes \
-browser "xdg-open %s"
@@ -94,16 +98,23 @@
make %{?_smp_mflags} world
%install
+%if %{with ide}
# Fixup dependencies before we install. Some are apparently not detected.
sed -i 's#^ide/ide_MLLIB_DEPENDENCIES:=.*$#& ide/configwin_types
ide/protocol/richpp#' \
.mllibfiles.d
+%endif
make COQINSTALLPREFIX=%{buildroot} install
+%if %{with ide}
%suse_update_desktop_file -i %{SOURCE1}
install -D -m 644 %{SOURCE1} %{buildroot}%{_datadir}/applications/coq.desktop
install -D -m 644 %{SOURCE2} %{buildroot}%{_datadir}/mime/packages/coq.xml
-install -D -m 644 ide/coq.png
%{buildroot}%{_datadir}/icons/hicolor/256x256/apps/coq.png
+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{,.opt} %{buildroot}%{_mandir}/man1/coqide.1
+%endif
# Sometimes we get identical x and x.opt files, replace by symlink x -> x.opt.
for bin in %{buildroot}%{_bindir}/*.opt
@@ -151,7 +162,6 @@
%files -f runtime.list
%license LICENSE CREDITS
%doc README.md
-%{_docdir}/%{name}/FAQ-CoqIde
%{_bindir}/coq-tex
%{_bindir}/coq_makefile
@@ -190,21 +200,24 @@
%{_mandir}/man1/coqtop.opt.1%{ext_man}
%{_mandir}/man1/coqwc.1%{ext_man}
-%{_datadir}/%{name}
%dir %{_datadir}/texmf
%dir %{_datadir}/texmf/tex
%dir %{_datadir}/texmf/tex/latex
%dir %{_datadir}/texmf/tex/latex/misc
%{_datadir}/texmf/tex/latex/misc/coqdoc.sty
+%if %{with ide}
%files ide
%{_bindir}/coqide
%{_bindir}/coqidetop
%{_bindir}/coqidetop.opt
%{_mandir}/man1/coqide.1%{ext_man}
+%{_datadir}/%{name}
%{_datadir}/applications/coq.desktop
%{_datadir}/icons/hicolor/256x256/apps/coq.png
%{_datadir}/mime/packages/coq.xml
+%{_docdir}/%{name}/FAQ-CoqIde
+%endif
%files devel -f devel.list
%{_libdir}/coq/tools/CoqMakefile.in
++++++ coq-8.12.2.tar.gz -> coq-8.13.0.tar.gz ++++++
/work/SRC/openSUSE:Factory/coq/coq-8.12.2.tar.gz
/work/SRC/openSUSE:Factory/.coq.new.28504/coq-8.13.0.tar.gz differ: char 12,
line 1
