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

Accepting request 1156169 from science

Browse Source 
- Update to version 8.19.1.
  * Fixed incorrect abstraction of sort variables for opaque
    constants leading to an inconsistency.
  * Fixed memory corruption with `vm_compute` (rare but more
    likely with OCaml 5.1).
  * "Found no matching notation to enable or disable" is now a
    warning instead of an error.
  * Fixed undeclared universe with multiple uses of `abstract`.
  * Fixed incorrect printing of constructor values with multiple
    arguments, and over-parenthesizing of constructor printing.
  * Fixed incorrect declared type for Ltac2.FMap.fold.

OBS-URL: https://build.opensuse.org/request/show/1156169
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/coq?expand=0&rev=27
This commit is contained in:
Ana Guerrero 2024-03-08 17:09:09 +00:00 committed by Git OBS Bridge
commit 2c5836b4d9
9 changed files with 31 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
coq-8.19.0.tar.gz
View File

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

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

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

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

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

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

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

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

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

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

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

15
coq.changes
View File

@ -1,3 +1,18 @@
-------------------------------------------------------------------
Thu Mar 7 22:31:46 UTC 2024 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.19.1.
* Fixed incorrect abstraction of sort variables for opaque
constants leading to an inconsistency.
* Fixed memory corruption with `vm_compute` (rare but more
likely with OCaml 5.1).
* "Found no matching notation to enable or disable" is now a
warning instead of an error.
* Fixed undeclared universe with multiple uses of `abstract`.
* Fixed incorrect printing of constructor values with multiple
arguments, and over-parenthesizing of constructor printing.
* Fixed incorrect declared type for Ltac2.FMap.fold.
-------------------------------------------------------------------
Sun Jan 28 20:20:35 UTC 2024 - Aaron Puchert <aaronpuchert@alice-dsl.net>

6
coq.spec
View File

@ -26,7 +26,7 @@
%endif
Name: coq
Version: 8.19.0
Version: 8.19.1
Release: 0
Summary: Proof Assistant based on the Calculus of Inductive Constructions
License: LGPL-2.1-only
@ -185,10 +185,10 @@ find %{buildroot}%{_libdir} -name '*.a' \
# pushd doc
# git sparse-checkout add V%{version}
# cd V%{version}
# tar --sort=name --owner=0 --group=0 --mtime="@$(stat -c %%Y refman/index.html)" \
# tar --sort=name --owner=0 --group=0 --mtime="@${SOURCE_DATE_EPOCH}" \
# --pax-option=exthdr.name=%d/PaxHeaders/%f,delete=atime,delete=ctime \
# -cJf ../../coq-refman-%{version}.tar.xz refman
# tar --sort=name --owner=0 --group=0 --mtime="@$(stat -c %%Y stdlib/index.html)" \
# tar --sort=name --owner=0 --group=0 --mtime="@${SOURCE_DATE_EPOCH}" \
# --pax-option=exthdr.name=%d/PaxHeaders/%f,delete=atime,delete=ctime \
# -cJf ../../coq-stdlib-%{version}.tar.xz stdlib
# popd

4
fr.inria.coq.coqide.metainfo.xml
View File

@ -46,6 +46,10 @@
<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.19.1" date="2024-03-04"/>
<release version="8.19.0" date="2024-01-24"/>
<release version="8.18.0" date="2023-09-08"/>
<release version="8.17.1" date="2023-06-27"/>
<release version="8.17.0" date="2023-03-27"/>
<release version="8.16.1" date="2022-11-25"/>
<release version="8.16.0" date="2022-09-05"/>