From d5c3490221893e6307c71e737c7c3970ecb2df8e Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Mon, 16 Oct 2023 16:35:54 +0200 Subject: [PATCH 1/3] Package coq-compcert.3.13.1 --- .../coq-compcert/coq-compcert.3.13.1/opam | 55 +++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 released/packages/coq-compcert/coq-compcert.3.13.1/opam diff --git a/released/packages/coq-compcert/coq-compcert.3.13.1/opam b/released/packages/coq-compcert/coq-compcert.3.13.1/opam new file mode 100644 index 000000000..eff8b8781 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.13.1/opam @@ -0,0 +1,55 @@ +opam-version: "2.0" +name: "coq-compcert" +synopsis: "The CompCert C compiler (64 bit)" +maintainer: "Michael Soegtrop" +authors: "Xavier Leroy " +license: "INRIA Non-Commercial License Agreement" +tags: [ + "category:Computer Science/Semantics and Compilation/Compilation" + "category:Computer Science/Semantics and Compilation/Semantics" + "keyword:C" + "keyword:compiler" + "logpath:compcert" + "date:2022-11-25" +] +homepage: "http://compcert.inria.fr/" +bug-reports: "https://github.com/AbsInt/CompCert/issues" +depends: [ + "coq" {>= "8.12.0" & < "8.19~"} + "menhir" {>= "20190626" & != "dev"} + "ocaml" {>= "4.05.0" & < "5~"} + "coq-flocq" {>= "4.1.0" & < "5~"} + "coq-menhirlib" {>= "20190626"} +] +build: [ + [ + "./configure" + "amd64-linux" {os = "linux" & arch = "x86_64"} + "amd64-macosx" {os = "macos" & arch = "x86_64"} + "arm64-linux" {os = "linux" & (arch = "arm64" | arch = "aarch64")} + "arm64-macosx" {os = "macos" & (arch = "arm64" | arch = "aarch64")} + "amd64-cygwin" {os = "cygwin"} + "amd64-cygwin" {os = "win32" & os-distribution = "cygwinports"} + "-toolprefix" + {os = "win32" & os-distribution = "cygwinports" & arch = "i686"} + "x86_64-pc-cygwin-" + {os = "win32" & os-distribution = "cygwinports" & arch = "i686"} + "-prefix" + "%{prefix}%" + "-install-coqdev" + "-clightgen" + "-use-external-Flocq" + "-use-external-MenhirLib" + "-coqdevdir" + "%{lib}%/coq/user-contrib/compcert" + "-ignore-coq-version" + ] + [make "-j%{jobs}%" {ocaml:version >= "4.06"}] +] +install: [make "install"] +dev-repo: "git+https://github.com/AbsInt/CompCert.git" +url { + src: "https://github.com/AbsInt/CompCert/archive/v3.13.1.tar.gz" + checksum: + "sha512=828a2f700e32400fc9d3ad2265b67194c48b10fef7f4b6bc1ed5a35d556088cc7defb697faf38c8b871b5b55e58e05f563e827255d2fc9bb964ac5f2cc1024d0" +} From dbf6e745a1f29e600015293f0f0acd359acc06f2 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Mon, 16 Oct 2023 20:37:15 +0200 Subject: [PATCH 2/3] Update released/packages/coq-compcert/coq-compcert.3.13.1/opam --- released/packages/coq-compcert/coq-compcert.3.13.1/opam | 1 - 1 file changed, 1 deletion(-) diff --git a/released/packages/coq-compcert/coq-compcert.3.13.1/opam b/released/packages/coq-compcert/coq-compcert.3.13.1/opam index eff8b8781..ae54f50ac 100644 --- a/released/packages/coq-compcert/coq-compcert.3.13.1/opam +++ b/released/packages/coq-compcert/coq-compcert.3.13.1/opam @@ -1,5 +1,4 @@ opam-version: "2.0" -name: "coq-compcert" synopsis: "The CompCert C compiler (64 bit)" maintainer: "Michael Soegtrop" authors: "Xavier Leroy " From 82bb9b4f05651cc9c4bf36d6401c542b69635bf8 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Tue, 17 Oct 2023 08:03:30 +0200 Subject: [PATCH 3/3] Update released/packages/coq-compcert/coq-compcert.3.13.1/opam Co-authored-by: Guillaume Melquiond --- released/packages/coq-compcert/coq-compcert.3.13.1/opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/released/packages/coq-compcert/coq-compcert.3.13.1/opam b/released/packages/coq-compcert/coq-compcert.3.13.1/opam index ae54f50ac..70b7e60f7 100644 --- a/released/packages/coq-compcert/coq-compcert.3.13.1/opam +++ b/released/packages/coq-compcert/coq-compcert.3.13.1/opam @@ -9,7 +9,7 @@ tags: [ "keyword:C" "keyword:compiler" "logpath:compcert" - "date:2022-11-25" + "date:2023-07-04" ] homepage: "http://compcert.inria.fr/" bug-reports: "https://github.com/AbsInt/CompCert/issues"