From 9a639890ba280b1fa6efbab679512f384c688ebb Mon Sep 17 00:00:00 2001 From: Andrew Appel Date: Thu, 31 Aug 2023 15:39:36 -0400 Subject: [PATCH 1/2] Create vcfloat.2.1.1 opam file --- .../coq-vcfloat/coq-vcfloat.2.1.1/opam | 44 +++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 released/packages/coq-vcfloat/coq-vcfloat.2.1.1/opam diff --git a/released/packages/coq-vcfloat/coq-vcfloat.2.1.1/opam b/released/packages/coq-vcfloat/coq-vcfloat.2.1.1/opam new file mode 100644 index 000000000..f4e07adc5 --- /dev/null +++ b/released/packages/coq-vcfloat/coq-vcfloat.2.1.1/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"] +] +install: [ + [make "-C" "vcfloat" "-j%{jobs}%" "install" "INSTALLDIR=%{lib}%/coq/user-contrib/vcfloat"] +] +run-test: [ + [make "-C" "vcfloat" "-j%{jobs}%" "tests"] +] +depends: [ + "coq" {>= "8.16" & < "8.18~"} + "coq-flocq" {>= "4.1.1" & < "5.0"} + "coq-interval" {>= "4.8.0"} + "coq-compcert" {>= "3.12"} + "coq-bignums" +] +url { + src: "https://github.com/VeriNum/vcfloat/archive/refs/tags/2.1.1.tar.gz" + checksum: "sha256=cd0098a7448e13116f4bb1faa3d93c6f1a8b5a6fa83be979875b432aeb9eb27e" +} +tags: [ + "date:2023-08-31" + "keyword:decision procedure" + "keyword:floating-point arithmetic" + "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" + "logpath:VCFloat" + ] From bb26d03d30ff06fc83fd2a320bc0455f78f12f5a Mon Sep 17 00:00:00 2001 From: Andrew Appel Date: Thu, 31 Aug 2023 15:50:59 -0400 Subject: [PATCH 2/2] Update released/packages/coq-vcfloat/coq-vcfloat.2.1.1/opam Co-authored-by: Karl Palmskog --- released/packages/coq-vcfloat/coq-vcfloat.2.1.1/opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/released/packages/coq-vcfloat/coq-vcfloat.2.1.1/opam b/released/packages/coq-vcfloat/coq-vcfloat.2.1.1/opam index f4e07adc5..ac6a89500 100644 --- a/released/packages/coq-vcfloat/coq-vcfloat.2.1.1/opam +++ b/released/packages/coq-vcfloat/coq-vcfloat.2.1.1/opam @@ -32,7 +32,7 @@ depends: [ "coq-bignums" ] url { - src: "https://github.com/VeriNum/vcfloat/archive/refs/tags/2.1.1.tar.gz" + src: "https://github.com/VeriNum/vcfloat/archive/refs/tags/v2.1.1.tar.gz" checksum: "sha256=cd0098a7448e13116f4bb1faa3d93c6f1a8b5a6fa83be979875b432aeb9eb27e" } tags: [