Hello community, here is the log from the commit of package coq for openSUSE:Factory checked in at 2020-02-15 22:26:16 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.26092 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Sat Feb 15 22:26:16 2020 rev:2 rq:774603 version:8.11.0 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2019-11-30 10:37:29.484171396 +0100 +++ /work/SRC/openSUSE:Factory/.coq.new.26092/coq.changes 2020-02-15 22:26:17.867338191 +0100 @@ -1,0 +2,52 @@ +Thu Feb 6 16:38:09 UTC 2020 - Aaron Puchert <aaronpuch...@alice-dsl.net> + +- Update to version 8.11.0. + * Ltac2, a new tactic language for writing more robust larger + scale tactics, with built-in support for datatypes and the + multi-goal tactic monad. + * Primitive floats are integrated in terms and follow the binary64 + format of the IEEE 754 standard, as specified in the + Coq.Float.Floats library. + * Many other cleanups and improvements have been performed and + are further described in the changelog. + * Special note on compatibility: Fixed bugs of Export and Import + that can have a significant impact on user developments. +- Drop unneeded empty *.vos files. + +------------------------------------------------------------------- +Sat Nov 30 16:40:21 UTC 2019 - Aaron Puchert <aaronpuch...@alice-dsl.net> + +- Update to version 8.10.2. + * Fixed a critical bug of template polymorphism and nonlinear + universes; + * Fixed a few anomalies; + * Fixed an 8.10 regression related to the printing of coercions + associated to notations; + * Fixed uneven dimensions of CoqIDE panels when window has been + resized; + * Fixed queries in CoqIDE. + +------------------------------------------------------------------- +Tue Nov 12 22:46:34 UTC 2019 - Aaron Puchert <aaronpuch...@alice-dsl.net> + +- Update to version 8.10.0. + * some quality-of-life bug fixes; + * a critical bug fix related to template polymorphism; + * native 63-bit machine integers; + * a new sort of definitionally proof-irrelevant propositions: SProp; + * private universes for opaque polymorphic constants; + * string notations and numeral notations; + * a new simplex-based proof engine for the tactics lia, nia, lra + and nra; + * new introduction patterns for SSReflect; + * a tactic to rewrite under binders: under; + * easy input of non-ASCII symbols in CoqIDE, which now uses GTK3. +- Update to version 8.10.1. + * Fix proof of False when using SProp + * Fix an anomaly when unsolved evar in Add Ring + * Fix Ltac regression in binding free names in uconstr + * Fix handling of unicode input before space + * Fix custom extraction of inductives to JSON +- Update version requirements. + +------------------------------------------------------------------- Old: ---- coq-8.9.1.tar.gz New: ---- coq-8.11.0.tar.gz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.VmkCQJ/_old 2020-02-15 22:26:18.399338479 +0100 +++ /var/tmp/diff_new_pack.VmkCQJ/_new 2020-02-15 22:26:18.399338479 +0100 @@ -1,7 +1,7 @@ # # spec file for package coq # -# Copyright (c) 2019 SUSE LINUX GmbH, Nuernberg, Germany. +# Copyright (c) 2019 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 @@ -16,8 +16,9 @@ # Please submit bugfixes or comments via https://bugs.opensuse.org/ # + Name: coq -Version: 8.9.1 +Version: 8.11.0 Release: 0 Summary: Proof Assistant based on the Calculus of Inductive Constructions License: LGPL-2.1-only @@ -31,7 +32,7 @@ BuildRequires: memory-constraints # Required for standard coq: BuildRequires: make >= 3.81 -BuildRequires: ocaml >= 3.10.2 +BuildRequires: ocaml >= 4.05.0 BuildRequires: ocaml-camlp5-devel >= 5.08 # TODO: Build docs when antlr4-python3-runtime becomes available. #BuildRequires: python3-Sphinx @@ -39,9 +40,12 @@ #BuildRequires: antlr4-python3-runtime #BuildRequires: python3-beautifulsoup4 # Required for coq-ide: -BuildRequires: ocamlfind(findlib) -BuildRequires: ocamlfind(lablgtk2) BuildRequires: update-desktop-files +BuildRequires: ocamlfind(findlib) +BuildRequires: ocamlfind(lablgtk3) +BuildRequires: pkgconfig(gdk-3.0) +BuildRequires: pkgconfig(gtk+-3.0) +BuildRequires: pkgconfig(gtksourceview-3.0) %global __requires_exclude ocaml\\\((Interface|Sos_types|GtkSourceView2_types)\\\) @@ -65,7 +69,7 @@ Summary: Development files for coq Group: Development/Libraries/Other Requires: %{name} = %{version}-%{release} -Requires: ocaml >= 3.10.2 +Requires: ocaml >= 4.05.0 %description devel This package contains development files for Coq. @@ -121,6 +125,9 @@ # Remove superfluous man page. rm %{buildroot}%{_mandir}/man1/coqtop.byte.1 +# Remove unneeded empty *.vos files. +find %{buildroot}%{_libdir}/coq -empty -name '*.vos' -delete + # Build lists of runtime and devel files by ending. # Compiled theories and shared objects are needed at runtime. find %{buildroot}%{_libdir}/coq/{plugins,theories} -type d | \ @@ -144,7 +151,7 @@ %files -f runtime.list %license LICENSE CREDITS -%doc CHANGES.md README.md +%doc README.md %{_docdir}/%{name}/FAQ-CoqIde %{_bindir}/coq-tex @@ -161,9 +168,12 @@ %{_bindir}/coqtop.opt %{_bindir}/coqwc %{_bindir}/coqworkmgr +%{_bindir}/doc_grammar +%{_bindir}/votour %dir %{_libdir}/coq %{_libdir}/coq/META +%{_libdir}/coq/revision %dir %{_libdir}/coq/kernel %dir %{_libdir}/coq/kernel/byterun %{_libdir}/coq/plugins/micromega/csdpcert ++++++ coq-8.9.1.tar.gz -> coq-8.11.0.tar.gz ++++++ /work/SRC/openSUSE:Factory/coq/coq-8.9.1.tar.gz /work/SRC/openSUSE:Factory/.coq.new.26092/coq-8.11.0.tar.gz differ: char 13, line 1
