From 0a6ff7b573b5d9394d6c0c56da470d3e0f3c2040 Mon Sep 17 00:00:00 2001 From: Calvin Beck Date: Fri, 10 Jan 2025 13:22:23 -0500 Subject: [PATCH] Release coq-vellvm v2.0.20250110 --- .../coq-vellvm/coq-vellvm.v2.0.20250110/opam | 55 +++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 released/packages/coq-vellvm/coq-vellvm.v2.0.20250110/opam diff --git a/released/packages/coq-vellvm/coq-vellvm.v2.0.20250110/opam b/released/packages/coq-vellvm/coq-vellvm.v2.0.20250110/opam new file mode 100644 index 0000000000..6bc5e89ea8 --- /dev/null +++ b/released/packages/coq-vellvm/coq-vellvm.v2.0.20250110/opam @@ -0,0 +1,55 @@ +opam-version: "2.0" +maintainer: "stevez@cis.upenn.edu" +synopsis: "Coq library implementing (executable) semantics for LLVM IR" + +homepage: "https://github.com/vellvm/vellvm" +dev-repo: "git+https://github.com/vellvm/vellvm.git" +bug-reports: "https://github.com/vellvm/vellvm/issues" +authors: [ + "Steve Zdancewic " + "Yannick Zakowski " + "Calvin Beck " + "Irene Yoon " + "Gary (Hanxi) Chen " +] +license: "GPL-3.0-or-later" + + +build: [make "-C" "src" "all" "-j%{jobs}%"] +install: [make "-C" "src" "install"] + +depends: [ + "ocaml" {>= "4.14.0"} + "cppo" + "dune" {>= "3.14.0"} + "menhir" + "qcheck" + "coq" {>= "8.20.0" & < "8.21~"} + "coq-ext-lib" {>= "0.12.1" & < "0.13~"} + "coq-paco" + "coq-ceres" + "coq-flocq" {>= "4.2.0"} + "coq-mathcomp-ssreflect" + "coq-simple-io" + "coq-itree" {>= "5.2.0" & < "5.3~"} + "coq-quickchick" {>= "2.0.4" & < "2.0.5"} +] + +tags: [ + "date:2025-01-10" + + "category:Computer Science/Programming Languages/Formal Definitions and Theory" + "category:Computer Science/Semantics and Compilation/Compilation" + "category:Computer Science/Semantics and Compilation/Semantics" + + "keyword:semantics" + "keyword:interpreter" + "keyword:LLVM" + + "logpath:Vellvm" +] + +url { + src: "https://github.com/vellvm/vellvm/releases/download/v2.0.20250110/v2.0.20250110.tar.gz" + checksum: "sha256=28ed7b9e441507d679f9cea5efce7bc02cd2e5568c37b52ea2d52dd57baef022" +}