coq-vst: add new version 2.11.1

released/packages/coq-vst-32/coq-vst-32.2.11.1/opam

@@ -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.14" & < "8.17~"}
+  "coq-compcert-32" {= "3.11"}
+  "coq-vst-zlist" {= "2.11"}
+  "coq-flocq" {>= "4.1.0"}
+]
+conflicts: [
+  "coq-vst"
+]
+tags: [
+  "category:Computer Science/Semantics and Compilation/Semantics"
+  "keyword:C"
+  "logpath:VST"
+  "date:2022-08-19"
+]
+url {
+  src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.11.1.tar.gz"
+  checksum: "sha512=9d66a1a0f428199110d89a8b4e90d50ad9b6448c92b5ad0859a1bcae9bf1153ea016b5af1ab9f4dc441b5af307968445f4b134cdb80593a6e9a974be94cc5730"
+}

released/packages/coq-vst/coq-vst.2.11.1/opam

@@ -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.14" & < "8.17~"}
+  "coq-compcert" {= "3.11"}
+  "coq-vst-zlist" {= "2.11"}
+  "coq-flocq" {>= "4.1.0"}
+]
+tags: [
+  "category:Computer Science/Semantics and Compilation/Semantics"
+  "keyword:C"
+  "logpath:VST"
+  "date:2022-08-19"
+]
+url {
+  src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.11.1.tar.gz"
+  checksum: "sha512=9d66a1a0f428199110d89a8b4e90d50ad9b6448c92b5ad0859a1bcae9bf1153ea016b5af1ab9f4dc441b5af307968445f4b134cdb80593a6e9a974be94cc5730"
+}