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-06-02 21:54:19 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.1548 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Thu Jun 2 21:54:19 2022 rev:17 rq:980409 version:8.15.2 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2022-03-25 21:54:38.630276516 +0100 +++ /work/SRC/openSUSE:Factory/.coq.new.1548/coq.changes 2022-06-02 21:54:28.988389493 +0200 @@ -1,0 +2,18 @@ +Wed Jun 1 21:41:11 UTC 2022 - Aaron Puchert <aaronpuch...@alice-dsl.net> + +- Update to version 8.15.2. + * Tactics `intuition` and `dintuition` use + `Tauto.intuition_solver` (defined as `auto with *`) instead of + hardcoding `auto with *`. This makes it possible to change the + default solver with `Ltac Tauto.intuition_solver ::= ...`. + * Fixed an uncaught exception `UnableToUnify` with + bidirectionality hints. + * Fixed multiple CoqIDE bugs. + * Fixed an incorrect implementation of `SFClassify`, allowing for + a proof of `False` since 8.11.0, due to Axioms present in + `Float.Axioms`. +- Rename coq.desktop to fr.inria.coq.coqide.desktop as the + documentation suggests, add an accompanying metainfo file. +- Declare documentation as noarch. + +------------------------------------------------------------------- Old: ---- coq-8.15.1.tar.gz coq-refman-8.15.1.tar.xz coq-stdlib-8.15.1.tar.xz coq.desktop New: ---- coq-8.15.2.tar.gz coq-refman-8.15.2.tar.xz coq-stdlib-8.15.2.tar.xz fr.inria.coq.coqide.desktop fr.inria.coq.coqide.metainfo.xml ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.AFkjHs/_old 2022-06-02 21:54:30.316391184 +0200 +++ /var/tmp/diff_new_pack.AFkjHs/_new 2022-06-02 21:54:30.320391190 +0200 @@ -20,15 +20,16 @@ %bcond_without ide Name: coq -Version: 8.15.1 +Version: 8.15.2 Release: 0 Summary: Proof Assistant based on the Calculus of Inductive Constructions License: LGPL-2.1-only Group: Productivity/Scientific/Math URL: https://coq.inria.fr/ Source: https://github.com/coq/coq/archive/V%{version}.tar.gz#/%{name}-%{version}.tar.gz -Source1: coq.desktop -Source2: coq.xml +Source1: fr.inria.coq.coqide.desktop +Source2: fr.inria.coq.coqide.metainfo.xml +Source3: coq.xml Source50: coq-refman-%{version}.tar.xz Source51: coq-stdlib-%{version}.tar.xz Source100: %{name}-rpmlintrc @@ -74,6 +75,7 @@ Summary: Documentation for coq Group: Documentation/HTML Requires: %{name} = %{version} +BuildArch: noarch %description doc HTML reference manual for Coq and full documentation of the standard library. @@ -112,8 +114,9 @@ %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 %{SOURCE1} %{buildroot}%{_datadir}/applications/fr.inria.coq.coqide.desktop +install -D -m 644 %{SOURCE2} %{buildroot}%{_datadir}/metainfo/fr.inria.coq.coqide.metainfo.xml +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 @@ -245,8 +248,9 @@ %{_bindir}/coqidetop.opt %{_mandir}/man1/coqide.1%{ext_man} %{_datadir}/%{name} -%{_datadir}/applications/coq.desktop +%{_datadir}/applications/fr.inria.coq.coqide.desktop %{_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 ++++++ coq-8.15.1.tar.gz -> coq-8.15.2.tar.gz ++++++ /work/SRC/openSUSE:Factory/coq/coq-8.15.1.tar.gz /work/SRC/openSUSE:Factory/.coq.new.1548/coq-8.15.2.tar.gz differ: char 27, line 1 ++++++ coq-refman-8.15.1.tar.xz -> coq-refman-8.15.2.tar.xz ++++++ /work/SRC/openSUSE:Factory/coq/coq-refman-8.15.1.tar.xz /work/SRC/openSUSE:Factory/.coq.new.1548/coq-refman-8.15.2.tar.xz differ: char 26, line 1 ++++++ coq-stdlib-8.15.1.tar.xz -> coq-stdlib-8.15.2.tar.xz ++++++ diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/stdlib/Coq.Floats.SpecFloat.html new/stdlib/Coq.Floats.SpecFloat.html --- old/stdlib/Coq.Floats.SpecFloat.html 2022-03-22 18:03:05.000000000 +0100 +++ new/stdlib/Coq.Floats.SpecFloat.html 2022-05-31 15:01:33.000000000 +0200 @@ -327,8 +327,8 @@ | <a class="idref" href="Coq.Floats.SpecFloat.html#S754_nan"><span class="id" title="constructor">S754_nan</span></a> => <a class="idref" href="Coq.Floats.FloatClass.html#NaN"><span class="id" title="constructor">NaN</span></a><br/> | <a class="idref" href="Coq.Floats.SpecFloat.html#S754_infinity"><span class="id" title="constructor">S754_infinity</span></a> <a class="idref" href="Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> => <a class="idref" href="Coq.Floats.FloatClass.html#PInf"><span class="id" title="constructor">PInf</span></a><br/> | <a class="idref" href="Coq.Floats.SpecFloat.html#S754_infinity"><span class="id" title="constructor">S754_infinity</span></a> <a class="idref" href="Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> => <a class="idref" href="Coq.Floats.FloatClass.html#NInf"><span class="id" title="constructor">NInf</span></a><br/> - | <a class="idref" href="Coq.Floats.SpecFloat.html#S754_zero"><span class="id" title="constructor">S754_zero</span></a> <a class="idref" href="Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> => <a class="idref" href="Coq.Floats.FloatClass.html#NZero"><span class="id" title="constructor">NZero</span></a><br/> - | <a class="idref" href="Coq.Floats.SpecFloat.html#S754_zero"><span class="id" title="constructor">S754_zero</span></a> <a class="idref" href="Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> => <a class="idref" href="Coq.Floats.FloatClass.html#PZero"><span class="id" title="constructor">PZero</span></a><br/> + | <a class="idref" href="Coq.Floats.SpecFloat.html#S754_zero"><span class="id" title="constructor">S754_zero</span></a> <a class="idref" href="Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> => <a class="idref" href="Coq.Floats.FloatClass.html#PZero"><span class="id" title="constructor">PZero</span></a><br/> + | <a class="idref" href="Coq.Floats.SpecFloat.html#S754_zero"><span class="id" title="constructor">S754_zero</span></a> <a class="idref" href="Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> => <a class="idref" href="Coq.Floats.FloatClass.html#NZero"><span class="id" title="constructor">NZero</span></a><br/> | <a class="idref" href="Coq.Floats.SpecFloat.html#S754_finite"><span class="id" title="constructor">S754_finite</span></a> <a class="idref" href="Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <span class="id" title="var">m</span> <span class="id" title="var">_</span> =><br/> <span class="id" title="keyword">if</span> (<a class="idref" href="Coq.Floats.SpecFloat.html#digits2_pos"><span class="id" title="definition">digits2_pos</span></a> <span class="id" title="var">m</span> <a class="idref" href="Coq.PArith.BinPos.html#73a7924686b773c85a4b58b44b86bc87"><span class="id" title="notation">=?</span></a> <a class="idref" href="Coq.ZArith.BinInt.html#Z.to_pos"><span class="id" title="definition">Z.to_pos</span></a> <a class="idref" href="Coq.Floats.SpecFloat.html#FloatOps.prec"><span class="id" title="variable">prec</span></a>)%<span class="id" title="var">positive</span> <span class="id" title="keyword">then</span> <a class="idref" href="Coq.Floats.FloatClass.html#PNormal"><span class="id" title="constructor">PNormal</span></a><br/> <span class="id" title="keyword">else</span> <a class="idref" href="Coq.Floats.FloatClass.html#PSubn"><span class="id" title="constructor">PSubn</span></a><br/> diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/stdlib/Coq.Init.Tauto.html new/stdlib/Coq.Init.Tauto.html --- old/stdlib/Coq.Init.Tauto.html 2022-03-22 18:03:05.000000000 +0100 +++ new/stdlib/Coq.Init.Tauto.html 2022-05-31 15:01:33.000000000 +0200 @@ -151,12 +151,15 @@ <span class="id" title="keyword">Ltac</span> <span class="id" title="var">dtauto</span> := <span class="id" title="var">with_power_flags</span> <span class="id" title="keyword">ltac</span>:(<span class="id" title="keyword">fun</span> <span class="id" title="var">flags</span> => <span class="id" title="var">tauto_gen</span> <span class="id" title="var">flags</span>).<br/> <br/> -<span class="id" title="keyword">Ltac</span> <span class="id" title="tactic">intuition</span> := <span class="id" title="var">with_uniform_flags</span> <span class="id" title="keyword">ltac</span>:(<span class="id" title="keyword">fun</span> <span class="id" title="var">flags</span> => <span class="id" title="var">intuition_gen</span> <span class="id" title="var">flags</span> <span class="id" title="keyword">ltac</span>:(<span class="id" title="tactic">auto</span> <span class="id" title="keyword">with</span> *)).<br/> +<span class="id" title="keyword">Ltac</span> <span class="id" title="var">intuition_solver</span> := <span class="id" title="tactic">auto</span> <span class="id" title="keyword">with</span> *.<br/> + +<br/> <span class="id" title="keyword">Local Ltac</span> <span class="id" title="var">intuition_then</span> <span class="id" title="var">tac</span> := <span class="id" title="var">with_uniform_flags</span> <span class="id" title="keyword">ltac</span>:(<span class="id" title="keyword">fun</span> <span class="id" title="var">flags</span> => <span class="id" title="var">intuition_gen</span> <span class="id" title="var">flags</span> <span class="id" title="var">tac</span>).<br/> +<span class="id" title="keyword">Ltac</span> <span class="id" title="tactic">intuition</span> := <span class="id" title="var">intuition_then</span> <span class="id" title="keyword">ltac</span>:(<span class="id" title="tactic">idtac</span>;<span class="id" title="var">intuition_solver</span>).<br/> <br/> -<span class="id" title="keyword">Ltac</span> <span class="id" title="var">dintuition</span> := <span class="id" title="var">with_power_flags</span> <span class="id" title="keyword">ltac</span>:(<span class="id" title="keyword">fun</span> <span class="id" title="var">flags</span> => <span class="id" title="var">intuition_gen</span> <span class="id" title="var">flags</span> <span class="id" title="keyword">ltac</span>:(<span class="id" title="tactic">auto</span> <span class="id" title="keyword">with</span> *)).<br/> <span class="id" title="keyword">Local Ltac</span> <span class="id" title="var">dintuition_then</span> <span class="id" title="var">tac</span> := <span class="id" title="var">with_power_flags</span> <span class="id" title="keyword">ltac</span>:(<span class="id" title="keyword">fun</span> <span class="id" title="var">flags</span> => <span class="id" title="var">intuition_gen</span> <span class="id" title="var">flags</span> <span class="id" title="var">tac</span>).<br/> +<span class="id" title="keyword">Ltac</span> <span class="id" title="var">dintuition</span> := <span class="id" title="var">dintuition_then</span> <span class="id" title="keyword">ltac</span>:(<span class="id" title="tactic">idtac</span>;<span class="id" title="var">intuition_solver</span>).<br/> <br/> <span class="id" title="keyword">Tactic Notation</span> "intuition" := <span class="id" title="tactic">intuition</span>.<br/> ++++++ fr.inria.coq.coqide.desktop ++++++ [Desktop Entry] Encoding=UTF-8 Type=Application Name=Coq IDE GenericName=Proof Assistant Comment=Proof Assistant based on the Calculus of Inductive Constructions Categories=Education;Science;Math; MimeType=text/x-coqsrc; Exec=coqide %F Icon=coq ++++++ fr.inria.coq.coqide.metainfo.xml ++++++ <?xml version="1.0" encoding="UTF-8"?> <component> <id type="desktop">fr.inria.coq.coqide</id> <metadata_license>CC0-1.0</metadata_license> <name>Coq IDE</name> <summary>Graphical frontend for the Coq formal proof management system</summary> <description> <p> Coq implements a program specification and mathematical higher-level language called <em>Gallina</em> that is based on an expressive formal language called the <em>Calculus of Inductive Constructions</em> that itself combines both a higher-order logic and a richly-typed functional programming language. Through a <em>vernacular</em> language of commands, Coq allows: </p> <ul> <li>to define functions or predicates, that can be evaluated efficiently;</li> <li>to state mathematical theorems and software specifications;</li> <li>to interactively develop formal proofs of these theorems;</li> <li>to machine-check these proofs by a relatively small certification "kernel";</li> <li>to extract certified programs to languages like OCaml, Haskell or Scheme.</li> </ul> <p> As a proof development system, Coq provides interactive proof methods, decision and semi-decision algorithms, and a <em>tactic</em> language for letting the user define its own proof methods. Connection with external computer algebra system or theorem provers is available. </p> <p> As a platform for the formalization of mathematics or the development of programs, Coq provides support for high-level notations, implicit contents and various other useful kinds of macros. </p> </description> <categories> <category>Development</category> <category>IDE</category> <category>Science</category> <category>ComputerScience</category> <category>Math</category> </categories> <keywords> <keyword>dependent-types</keyword> <keyword>coq</keyword> <keyword>theorem-proving</keyword> <keyword>proof-assistant</keyword> </keywords> <url type="homepage">https://coq.inria.fr/</url> <url type="bugtracker">https://github.com/coq/coq/issues</url> <url type="faq">https://github.com/coq/coq/wiki/The-Coq-FAQ</url> <url type="help">https://coq.inria.fr/documentation</url> <url type="donation">https://coq.inria.fr/consortium</url> <url type="vcs-browser">https://github.com/coq/coq</url> <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.15.2" date="2022-05-31"/> <release version="8.15.1" date="2022-03-22"/> </releases> <provides> <binary>coqide</binary> </provides> <project_license>LGPL-2.1-only</project_license> <content_rating type="oars-1.1"/> </component>
