Merge pull request #3338 from andrew-appel/master

coq-vcfloat.2.3, coq-vst-lib.2.15.1

Author: palmskog

released/packages/coq-vcfloat/coq-vcfloat.2.3/opam

@@ -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 <[email protected]>"
+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"]
+]
+install: [
+  [make "-C" "vcfloat" "-j%{jobs}%" "install" "INSTALLDIR=%{lib}%/coq/user-contrib/vcfloat"]
+]
+run-test: [
+  [make "-C" "vcfloat" "-j%{jobs}%" "tests"]
+]
+depends: [
+  "coq" {>= "8.19" & < "8.21~"}
+  "coq-flocq" {>= "4.1.4" & < "5.0"}
+  "coq-interval" {>= "4.10.0"}
+  "coq-compcert" {>= "3.15"}
+  "coq-bignums"
+]
+url {
+  src: "https://github.com/VeriNum/vcfloat/archive/refs/tags/v2.3.tar.gz"
+  checksum: "sha256=daa5a26b65c086eb9014704f53f319594b9348c77d1add2b94437771ecd69ae0"
+}
+tags: [
+  "date:2025-02-10"
+  "keyword:decision procedure"
+  "keyword:floating-point arithmetic"
+  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
+  "logpath:VCFloat"
+  ]

released/packages/coq-vst-lib/coq-vst-lib.2.15.1/opam

@@ -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 <[email protected]>"
+homepage: "https://github.com/PrincetonUniversity/VST/tree/lib-2.15.1/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.3"}
+  "coq-vst" {>= "2.15"}
+]
+url {
+  src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/lib-2.15.1.tar.gz"
+  checksum: "sha256=b08762b1b250e3e351e179fbf82c8618148f3160c545daab9e3b2103cf9e0d4e"
+}
+
+tags: [
+  "date:2025-02-10"
+  "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"
+  ]