Skip to content

Commit

Permalink
Merge pull request #3286 from andrew-appel/master
Browse files Browse the repository at this point in the history
Opam packages for coq-vst.2.15 and coq-vst-lib.2.15
palmskog authored Jan 8, 2025
2 parents a17237a + fc1d754 commit b2cfdc3
Showing 2 changed files with 96 additions and 0 deletions.
46 changes: 46 additions & 0 deletions released/packages/coq-vst-lib/coq-vst-lib.2.15/opam
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
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.15/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.19" & < "8.21~"}
"coq-compcert" {>= "3.15"}
"coq-flocq" {>= "4.1.0" & < "5.0"}
"coq-vcfloat" {>= "2.2"}
"coq-vst" {>= "2.15"}
]
url {
src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.15.tar.gz"
checksum: "sha256=44873919ee077b2ce4eb2b7a83c663d3fd673fd7d89c6fc578c46cf10efb4465"
}

tags: [
"date:2025-01-08"
"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"
]
50 changes: 50 additions & 0 deletions released/packages/coq-vst/coq-vst.2.15/opam
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.19" & < "8.21~"}
"coq-compcert" {= "3.15"}
"coq-vst-zlist" {= "2.13"}
"coq-flocq" {>= "4.2.0"}
]
tags: [
"category:Computer Science/Semantics and Compilation/Semantics"
"keyword:C"
"logpath:VST"
"date:2025-01-08"
]
url {
src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.15.tar.gz"
checksum: "sha256=44873919ee077b2ce4eb2b7a83c663d3fd673fd7d89c6fc578c46cf10efb4465"
}

0 comments on commit b2cfdc3

Please sign in to comment.