rpm/coq
SHA256
1
0
Fork 0
forked from pool/coq
Code Pull Requests Activity

- Update to version 8.15.2.

Browse Source 
* 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.

OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=40
This commit is contained in:
Aaron Puchert 2022-06-01 21:48:29 +00:00 committed by Git OBS Bridge
parent 660b7caabf
commit 9b2016e937
10 changed files with 94 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
coq-8.15.1.tar.gz
View File

@ -1,3 +0,0 @@
version https://git-lfs.github.com/spec/v1
oid sha256:513e953b7183d478acb75fd6e80e4dc32ac1a918cf4343ac31a859cfb4e9aad2
size 7221470

3
coq-8.15.2.tar.gz Normal file
View File

@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926
size 7222794

3
coq-refman-8.15.1.tar.xz
View File

@ -1,3 +0,0 @@
version https://git-lfs.github.com/spec/v1
oid sha256:fbd7ca409c1077f042c2916e8a57e5c0d36c8624aa308a12e9f73c947e76c258
size 9213172

3
coq-refman-8.15.2.tar.xz Normal file
View File

@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:775f1681c1c33f41b2af314af021035f399d4aba410701d7b10dfc670aac0eec
size 9221052

3
coq-stdlib-8.15.1.tar.xz
View File

@ -1,3 +0,0 @@
version https://git-lfs.github.com/spec/v1
oid sha256:156b28c55673b1cf7c91d47de09f1042ad8ec6621894a6f90322184320aeec46
size 2892604

3
coq-stdlib-8.15.2.tar.xz Normal file
View File

@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:724b65c21a3f55fecbd6eea94509af2cc3fe797e854b366fbee76d69cb7d39ad
size 2892408

18
coq.changes
View File

@ -1,3 +1,21 @@
-------------------------------------------------------------------
Wed Jun 1 21:41:11 UTC 2022 - Aaron Puchert <aaronpuchert@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.
-------------------------------------------------------------------
Thu Mar 24 22:56:21 UTC 2022 - Aaron Puchert <aaronpuchert@alice-dsl.net>

16
coq.spec
View File

@ -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 @@ This package contains development files for Coq.
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 @@ mv %{buildroot}%{_prefix}/lib/* %{buildroot}%{_libdir}
%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 @@ rm -r %{buildroot}%{_docdir}/%{name}/refman/{.buildinfo,.doctrees,_sources}
%{_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

0
coq.desktop → fr.inria.coq.coqide.desktop
View File

57
fr.inria.coq.coqide.metainfo.xml Normal file
View File

@ -0,0 +1,57 @@
<?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>