diff --git a/released/packages/coq-vcfloat/coq-vcfloat.2.2/opam b/released/packages/coq-vcfloat/coq-vcfloat.2.2/opam new file mode 100644 index 000000000..47a6a4518 --- /dev/null +++ b/released/packages/coq-vcfloat/coq-vcfloat.2.2/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 " +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" + ] diff --git a/released/packages/coq-vst-32/coq-vst-32.2.14/opam b/released/packages/coq-vst-32/coq-vst-32.2.14/opam new file mode 100644 index 000000000..35bdaeba4 --- /dev/null +++ b/released/packages/coq-vst-32/coq-vst-32.2.14/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.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" +} diff --git a/released/packages/coq-vst-lib/coq-vst-lib.2.13/opam b/released/packages/coq-vst-lib/coq-vst-lib.2.13/opam index ad313456b..a93b98565 100644 --- a/released/packages/coq-vst-lib/coq-vst-lib.2.13/opam +++ b/released/packages/coq-vst-lib/coq-vst-lib.2.13/opam @@ -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 { diff --git a/released/packages/coq-vst-lib/coq-vst-lib.2.14/opam b/released/packages/coq-vst-lib/coq-vst-lib.2.14/opam new file mode 100644 index 000000000..0a2fbc9a9 --- /dev/null +++ b/released/packages/coq-vst-lib/coq-vst-lib.2.14/opam @@ -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 " +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" + ] diff --git a/released/packages/coq-vst-zlist/coq-vst-zlist.2.13/opam b/released/packages/coq-vst-zlist/coq-vst-zlist.2.13/opam index d0e2bbc1f..0fae58da7 100644 --- a/released/packages/coq-vst-zlist/coq-vst-zlist.2.13/opam +++ b/released/packages/coq-vst-zlist/coq-vst-zlist.2.13/opam @@ -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" diff --git a/released/packages/coq-vst/coq-vst.2.14/opam b/released/packages/coq-vst/coq-vst.2.14/opam new file mode 100644 index 000000000..fad0b322f --- /dev/null +++ b/released/packages/coq-vst/coq-vst.2.14/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.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" +}