Hello community,
here is the log from the commit of package coq for openSUSE:Factory checked in
at 2020-12-04 21:27:53
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Comparing /work/SRC/openSUSE:Factory/coq (Old)
and /work/SRC/openSUSE:Factory/.coq.new.5913 (New)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq"
Fri Dec 4 21:27:53 2020 rev:7 rq:849178 version:8.12.1
Changes:
--------
--- /work/SRC/openSUSE:Factory/coq/coq.changes 2020-08-06 10:43:00.054146505
+0200
+++ /work/SRC/openSUSE:Factory/.coq.new.5913/coq.changes 2020-12-04
21:27:55.806076799 +0100
@@ -1,0 +2,21 @@
+Tue Nov 17 22:09:12 UTC 2020 - Aaron Puchert <aaronpuch...@alice-dsl.net>
+
+- Update to version 8.12.1. This contains mostly bug fixes:
+ * Polymorphic side-effects inside monomorphic definitions were
+ incorrectly handled as not inlined. This allowed deriving an
+ inconsistency.
+ * Regression in error reporting after SSReflect's case tactic.
+ A generic error message "Could not fill dependent hole in
+ apply" was reported for any error following case or elim.
+ * Several bugs with Search.
+ * The details environment introduced in coqdoc in Coq 8.12 can
+ now be used as advertised in the reference manual.
+ * View menu "Display parentheses" introduced in CoqIDE in
+ Coq 8.12 now works correctly.
+
+-------------------------------------------------------------------
+Thu Aug 20 08:33:34 UTC 2020 - Martin Liška <mli...@suse.cz>
+
+- Use memoryperjob constraint instead of %limit_build macro.
+
+-------------------------------------------------------------------
Old:
----
coq-8.12.0.tar.gz
New:
----
_constraints
coq-8.12.1.tar.gz
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Other differences:
------------------
++++++ coq.spec ++++++
--- /var/tmp/diff_new_pack.8QKrYY/_old 2020-12-04 21:27:56.582077912 +0100
+++ /var/tmp/diff_new_pack.8QKrYY/_new 2020-12-04 21:27:56.586077918 +0100
@@ -18,7 +18,7 @@
Name: coq
-Version: 8.12.0
+Version: 8.12.1
Release: 0
Summary: Proof Assistant based on the Calculus of Inductive
Constructions
License: LGPL-2.1-only
@@ -29,7 +29,6 @@
Source2: coq.xml
Source100: %{name}-rpmlintrc
BuildRequires: desktop-file-utils
-BuildRequires: memory-constraints
# Required for standard coq:
BuildRequires: make >= 3.81
BuildRequires: ocaml >= 4.05.0
@@ -92,7 +91,6 @@
-natdynlink yes \
-browser "xdg-open %s"
-%limit_build -m 800
make %{?_smp_mflags} world
%install
++++++ _constraints ++++++
<?xml version="1.0" encoding="UTF-8"?>
<constraints>
<hardware>
<memoryperjob>
<size unit="M">800</size>
</memoryperjob>
</hardware>
</constraints>++++++ coq-8.12.0.tar.gz -> coq-8.12.1.tar.gz ++++++
/work/SRC/openSUSE:Factory/coq/coq-8.12.0.tar.gz
/work/SRC/openSUSE:Factory/.coq.new.5913/coq-8.12.1.tar.gz differ: char 28,
line 1
_______________________________________________
openSUSE Commits mailing list -- commit@lists.opensuse.org
To unsubscribe, email commit-le...@lists.opensuse.org
List Netiquette: https://en.opensuse.org/openSUSE:Mailing_list_netiquette
List Archives:
https://lists.opensuse.org/archives/list/commit@lists.opensuse.org
