Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update several packages for Coq 8.19 and recent releases #2993

Merged
merged 5 commits into from
Mar 21, 2024
Merged

Update several packages for Coq 8.19 and recent releases #2993

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
c76dfac
Update several packages for Coq 8.19 and recent releases
andrew-appel Mar 20, 2024
1c7eb68
Apply suggestions from code review
palmskog Mar 21, 2024
1ec0be2
Fix issues related to zlist and stable .gz downloads
andrew-appel Mar 21, 2024
7d3d770
fix coq-vst-32 as well
andrew-appel Mar 21, 2024
a287f07
I was wrong, a new coq-vst-lib.2.14 is required after all
andrew-appel Mar 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 44 additions & 0 deletions released/packages/coq-vcfloat/coq-vcfloat.2.2/opam
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
opam-version: "2.0"
synopsis: "VCFloat: Floating Point Round-off Error Analysis"
description: "VCFloat is a tool for Coq proofs about floating-point round-off error."
authors: [
"Andrew W. Appel"
"Ariel E. Kellison"
"Tahina Ramananandro"
"Paul Mountcastle"
"Benoit Meister"
"Richard Lethin"
]
homepage: "https://verinum.org/vcfloat/"
maintainer: "Andrew W. Appel <appel@princeton.edu>"
dev-repo: "git+https://github.com/VeriNum/vcfloat"
bug-reports: "https://github.com/VeriNum/vcfloat/issues"
license: "LGPL-3.0-or-later"

build: [
[ make "-C" "vcfloat" "-j%{jobs}%" "vcfloat2" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed & coq-compcert:version < "3.14~"}]
]
install: [
[make "-C" "vcfloat" "-j%{jobs}%" "install" "INSTALLDIR=%{lib}%/coq/user-contrib/vcfloat" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed & coq-compcert:version < "3.14~"}]
]
run-test: [
[make "-C" "vcfloat" "-j%{jobs}%" "tests" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed & coq-compcert:version < "3.14~"}]
]
depends: [
"coq" {>= "8.19" & < "8.20~"}
"coq-flocq" {>= "4.1.4" & < "5.0"}
"coq-interval" {>= "4.10.0"}
"coq-compcert" {>= "3.13"}
"coq-bignums"
]
url {
src: "https://github.com/VeriNum/vcfloat/releases/download/v2.2/vcfloat-2.2.tar.gz"
checksum: "sha256=5d57a3f0e69453460e729f26f00597e456a4ee2502f0886acf11d7908692af46"
}
tags: [
"date:2024-03-20"
"keyword:decision procedure"
"keyword:floating-point arithmetic"
"category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
"logpath:VCFloat"
]
53 changes: 53 additions & 0 deletions released/packages/coq-vst-32/coq-vst-32.2.14/opam
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
opam-version: "2.0"
synopsis: "Verified Software Toolchain"
description: "The software toolchain includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program. The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context."
authors: [
"Andrew W. Appel"
"Lennart Beringer"
"Josiah Dodds"
"Qinxiang Cao"
"Aquinas Hobor"
"Gordon Stewart"
"Qinshi Wang"
"Sandrine Blazy"
"Santiago Cuellar"
"Robert Dockins"
"Nick Giannarakis"
"Samuel Gruetter"
"Jean-Marie Madiot"
]
maintainer: "VST team"
homepage: "http://vst.cs.princeton.edu/"
dev-repo: "git+https://github.com/PrincetonUniversity/VST.git"
bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
license: "BSD-2-Clause"

build: [
[make "-j%{jobs}%" "vst" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=32"]
]
install: [
[make "install" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=32"]
]
run-test: [
[make "-j%{jobs}%" "test" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=32"]
]
depends: [
"ocaml"
"coq" {>= "8.17" & < "8.20~"}
"coq-compcert-32" {= "3.13.1"}
"coq-vst-zlist" {= "2.13"}
"coq-flocq" {>= "4.1.0"}
]
conflicts: [
"coq-vst"
]
tags: [
"category:Computer Science/Semantics and Compilation/Semantics"
"keyword:C"
"logpath:VST"
"date:2024-03-20"
]
url {
src: "https://github.com/PrincetonUniversity/VST/releases/download/v2.14/VST-2.14.tar.gz"
checksum: "sha256=c11551c454057b8a6c7a958534f3ec783e09450ff7e373bfb7c3d6c009d46c06"
}
4 changes: 2 additions & 2 deletions released/packages/coq-vst-lib/coq-vst-lib.2.13/opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,10 +22,10 @@ run-test: [
[ make "-C" "lib" "-j%{jobs}%" "test-only"]
]
depends: [
"coq" {>= "8.16" & < "8.19~"}
"coq" {>= "8.16" & < "8.20~"}
"coq-compcert" {>= "3.11"}
"coq-flocq" {>= "4.1.0" & < "5.0"}
"coq-vcfloat" {>= "2.1"}
"coq-vcfloat" {>= "2.1" & < "2.2~"}
"coq-vst" {>= "2.11.1"}
]
url {
Expand Down
45 changes: 45 additions & 0 deletions released/packages/coq-vst-lib/coq-vst-lib.2.14/opam
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
opam-version: "2.0"
synopsis: "VSTlib: VST-verified C library for VST-verified clients"
description: "These program modules, in the form of Verified Software Units,
may be linked with client-module code (at the .c/.o level) and proofs (at the .v level)."
authors: [
"Andrew W. Appel"
"William Mansky"
]
maintainer: "Andrew W. Appel <appel@princeton.edu>"
homepage: "https://github.com/PrincetonUniversity/VST/tree/v2.13/lib#readme"
dev-repo: "git+https://github.com/PrincetonUniversity/VST"
bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
license: "BSD-2-Clause"

build: [
[ make "-C" "lib" "-j%{jobs}%" "proof-only"]
]
install: [
[ make "-C" "lib" "install" "INSTALLDIR=%{lib}%/coq/user-contrib/VSTlib"]
]
run-test: [
[ make "-C" "lib" "-j%{jobs}%" "test-only"]
]
depends: [
"coq" {>= "8.17" & < "8.20~"}
"coq-compcert" {>= "3.13"}
"coq-flocq" {>= "4.1.0" & < "5.0"}
"coq-vcfloat" {>= "2.2"}
"coq-vst" {>= "2.13"}
]
url {
src: "https://github.com/PrincetonUniversity/VST/releases/download/v2.14/VST-2.14.tar.gz"
checksum: "sha256=c11551c454057b8a6c7a958534f3ec783e09450ff7e373bfb7c3d6c009d46c06"
}
tags: [
"date:2024-03-20"
"keyword:VST"
"keyword:library"
"keyword:malloc"
"keyword:threads"
"keyword:floating-point arithmetic"
"category:Miscellaneous/Coq Extensions"
"category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
"logpath:VSTlib"
]
2 changes: 1 addition & 1 deletion released/packages/coq-vst-zlist/coq-vst-zlist.2.13/opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ build: [
]
install: [make "-C" "zlist" "install"]
depends: [
"coq" {>= "8.16.1" & < "8.19~"}
"coq" {>= "8.16.1" & < "8.20~"}
]
url {
src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.13.tar.gz"
Expand Down
50 changes: 50 additions & 0 deletions released/packages/coq-vst/coq-vst.2.14/opam
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
opam-version: "2.0"
synopsis: "Verified Software Toolchain"
description: "The software toolchain includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program. The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context."
authors: [
"Andrew W. Appel"
"Lennart Beringer"
"Josiah Dodds"
"Qinxiang Cao"
"Aquinas Hobor"
"Gordon Stewart"
"Qinshi Wang"
"Sandrine Blazy"
"Santiago Cuellar"
"Robert Dockins"
"Nick Giannarakis"
"Samuel Gruetter"
"Jean-Marie Madiot"
]
maintainer: "VST team"
homepage: "http://vst.cs.princeton.edu/"
dev-repo: "git+https://github.com/PrincetonUniversity/VST.git"
bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
license: "BSD-2-Clause"

build: [
[make "-j%{jobs}%" "vst" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
]
install: [
[make "install" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
]
run-test: [
[make "-j%{jobs}%" "test" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
]
depends: [
"ocaml"
"coq" {>= "8.17" & < "8.20~"}
"coq-compcert" {= "3.13.1"}
"coq-vst-zlist" {= "2.13"}
"coq-flocq" {>= "4.1.0"}
]
tags: [
"category:Computer Science/Semantics and Compilation/Semantics"
"keyword:C"
"logpath:VST"
"date:2024-03-20"
]
url {
src: "https://github.com/PrincetonUniversity/VST/releases/download/v2.14/VST-2.14.tar.gz"
checksum: "sha256=c11551c454057b8a6c7a958534f3ec783e09450ff7e373bfb7c3d6c009d46c06"
}
Loading