From f15fa9f51b8c39d5639144d7e5514fe78f2e4dab Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 22 Sep 2023 07:59:23 -0700 Subject: [PATCH 1/4] Restrict rewriter OCaml version on ARM Fixes https://github.com/mit-plv/rewriter/issues/97 --- extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam | 1 + released/packages/coq-rewriter/coq-rewriter.0.0.2/opam | 3 ++- released/packages/coq-rewriter/coq-rewriter.0.0.6/opam | 1 + released/packages/coq-rewriter/coq-rewriter.0.0.7/opam | 1 + released/packages/coq-rewriter/coq-rewriter.0.0.8/opam | 1 + 5 files changed, 6 insertions(+), 1 deletion(-) diff --git a/extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam b/extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam index 08713ed6b4..97698b596a 100644 --- a/extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam +++ b/extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam @@ -13,6 +13,7 @@ build: [ install: [make "install"] depends: [ "ocaml" {build} + "ocaml" {build & >= "4.14.0" & (arch != "arm64" | arch != "aarch64")} "coq" {>= "8.15~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam index 81dfb8bdb8..a2bcc2761e 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam @@ -12,7 +12,8 @@ build: [ ] install: [make "install"] depends: [ - "ocaml" + "ocaml" {build} + "ocaml" {build & >= "4.14.0" & (arch != "arm64" | arch != "aarch64")} "coq" {>= "8.9~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam index 47230d64c6..8714889a95 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam @@ -14,6 +14,7 @@ install: [make "install"] depends: [ "conf-findutils" {build} "ocaml" {build} + "ocaml" {build & >= "4.14.0" & (arch != "arm64" | arch != "aarch64")} "coq" {>= "8.15~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam index 9e5b2ae9b8..878cab134e 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam @@ -14,6 +14,7 @@ install: [make "install"] depends: [ "conf-findutils" {build} "ocaml" {build} + "ocaml" {build & >= "4.14.0" & (arch != "arm64" | arch != "aarch64")} "coq" {>= "8.15~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam index 5fb5e28b91..61747e6638 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam @@ -14,6 +14,7 @@ install: [make "install"] depends: [ "conf-findutils" {build} "ocaml" {build} + "ocaml" {build & >= "4.14.0" & (arch != "arm64" | arch != "aarch64")} "coq" {>= "8.15~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" From b24b664504ab001c84f764acd9a8216a50095c09 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 22 Sep 2023 08:17:07 -0700 Subject: [PATCH 2/4] Drop aarch64 to comply with opam-lint --- extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam | 2 +- released/packages/coq-rewriter/coq-rewriter.0.0.2/opam | 2 +- released/packages/coq-rewriter/coq-rewriter.0.0.6/opam | 2 +- released/packages/coq-rewriter/coq-rewriter.0.0.7/opam | 2 +- released/packages/coq-rewriter/coq-rewriter.0.0.8/opam | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam b/extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam index 97698b596a..714ec1f114 100644 --- a/extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam +++ b/extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam @@ -13,7 +13,7 @@ build: [ install: [make "install"] depends: [ "ocaml" {build} - "ocaml" {build & >= "4.14.0" & (arch != "arm64" | arch != "aarch64")} + "ocaml" {build & >= "4.14.0" & arch != "arm64"} "coq" {>= "8.15~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam index a2bcc2761e..6b1534bfdf 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam @@ -13,7 +13,7 @@ build: [ install: [make "install"] depends: [ "ocaml" {build} - "ocaml" {build & >= "4.14.0" & (arch != "arm64" | arch != "aarch64")} + "ocaml" {build & >= "4.14.0" & arch != "arm64"} "coq" {>= "8.9~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam index 8714889a95..c3542bca1f 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam @@ -14,7 +14,7 @@ install: [make "install"] depends: [ "conf-findutils" {build} "ocaml" {build} - "ocaml" {build & >= "4.14.0" & (arch != "arm64" | arch != "aarch64")} + "ocaml" {build & >= "4.14.0" & arch != "arm64"} "coq" {>= "8.15~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam index 878cab134e..ceea88b98a 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam @@ -14,7 +14,7 @@ install: [make "install"] depends: [ "conf-findutils" {build} "ocaml" {build} - "ocaml" {build & >= "4.14.0" & (arch != "arm64" | arch != "aarch64")} + "ocaml" {build & >= "4.14.0" & arch != "arm64"} "coq" {>= "8.15~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam index 61747e6638..67256286a1 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam @@ -14,7 +14,7 @@ install: [make "install"] depends: [ "conf-findutils" {build} "ocaml" {build} - "ocaml" {build & >= "4.14.0" & (arch != "arm64" | arch != "aarch64")} + "ocaml" {build & >= "4.14.0" & arch != "arm64"} "coq" {>= "8.15~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" From 36d1b79627d20849296da08234a285ac115abb26 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 22 Sep 2023 09:31:03 -0700 Subject: [PATCH 3/4] Add upper Coq version bounds for coq-rewriter released --- released/packages/coq-rewriter/coq-rewriter.0.0.2/opam | 2 +- released/packages/coq-rewriter/coq-rewriter.0.0.6/opam | 2 +- released/packages/coq-rewriter/coq-rewriter.0.0.7/opam | 2 +- released/packages/coq-rewriter/coq-rewriter.0.0.8/opam | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam index 6b1534bfdf..ff3d295953 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam @@ -14,7 +14,7 @@ install: [make "install"] depends: [ "ocaml" {build} "ocaml" {build & >= "4.14.0" & arch != "arm64"} - "coq" {>= "8.9~"} + "coq" {>= "8.9~" & < "8.17~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" synopsis: "Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam index c3542bca1f..11c82d638b 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam @@ -15,7 +15,7 @@ depends: [ "conf-findutils" {build} "ocaml" {build} "ocaml" {build & >= "4.14.0" & arch != "arm64"} - "coq" {>= "8.15~"} + "coq" {>= "8.15~" & < "8.18~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" synopsis: "Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam index ceea88b98a..50bae16407 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam @@ -15,7 +15,7 @@ depends: [ "conf-findutils" {build} "ocaml" {build} "ocaml" {build & >= "4.14.0" & arch != "arm64"} - "coq" {>= "8.15~"} + "coq" {>= "8.15~" & < "8.18~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" synopsis: "Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam index 67256286a1..6071168b4e 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam @@ -15,7 +15,7 @@ depends: [ "conf-findutils" {build} "ocaml" {build} "ocaml" {build & >= "4.14.0" & arch != "arm64"} - "coq" {>= "8.15~"} + "coq" {>= "8.15~" & < "8.18~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" synopsis: "Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography" From 781dace0c3e4ef6f8d741f5361ec647727dd8181 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 23 Sep 2023 00:41:43 -0700 Subject: [PATCH 4/4] [coq-rewriter] Use disjunctions As per https://github.com/coq/opam/pull/2734#discussion_r1334915279 --- extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam | 3 +-- released/packages/coq-rewriter/coq-rewriter.0.0.2/opam | 3 +-- released/packages/coq-rewriter/coq-rewriter.0.0.6/opam | 3 +-- released/packages/coq-rewriter/coq-rewriter.0.0.7/opam | 3 +-- released/packages/coq-rewriter/coq-rewriter.0.0.8/opam | 3 +-- released/packages/coq-rewriter/coq-rewriter.0.0.9/opam | 3 +-- 6 files changed, 6 insertions(+), 12 deletions(-) diff --git a/extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam b/extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam index 714ec1f114..85efc43bb0 100644 --- a/extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam +++ b/extra-dev/packages/coq-rewriter/coq-rewriter.dev/opam @@ -12,8 +12,7 @@ build: [ ] install: [make "install"] depends: [ - "ocaml" {build} - "ocaml" {build & >= "4.14.0" & arch != "arm64"} + "ocaml" {build & (arch = "x86_32" | arch = "x86_64" | >= "4.14.0")} "coq" {>= "8.15~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam index ff3d295953..910e347175 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.2/opam @@ -12,8 +12,7 @@ build: [ ] install: [make "install"] depends: [ - "ocaml" {build} - "ocaml" {build & >= "4.14.0" & arch != "arm64"} + "ocaml" {build & (arch = "x86_32" | arch = "x86_64" | >= "4.14.0")} "coq" {>= "8.9~" & < "8.17~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam index 11c82d638b..93e85531a9 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam @@ -13,8 +13,7 @@ build: [ install: [make "install"] depends: [ "conf-findutils" {build} - "ocaml" {build} - "ocaml" {build & >= "4.14.0" & arch != "arm64"} + "ocaml" {build & (arch = "x86_32" | arch = "x86_64" | >= "4.14.0")} "coq" {>= "8.15~" & < "8.18~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam index 50bae16407..f59d6f2dff 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.7/opam @@ -13,8 +13,7 @@ build: [ install: [make "install"] depends: [ "conf-findutils" {build} - "ocaml" {build} - "ocaml" {build & >= "4.14.0" & arch != "arm64"} + "ocaml" {build & (arch = "x86_32" | arch = "x86_64" | >= "4.14.0")} "coq" {>= "8.15~" & < "8.18~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam index 6071168b4e..aefd31bb1d 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.8/opam @@ -13,8 +13,7 @@ build: [ install: [make "install"] depends: [ "conf-findutils" {build} - "ocaml" {build} - "ocaml" {build & >= "4.14.0" & arch != "arm64"} + "ocaml" {build & (arch = "x86_32" | arch = "x86_64" | >= "4.14.0")} "coq" {>= "8.15~" & < "8.18~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" diff --git a/released/packages/coq-rewriter/coq-rewriter.0.0.9/opam b/released/packages/coq-rewriter/coq-rewriter.0.0.9/opam index 735dec4fc7..841041843a 100644 --- a/released/packages/coq-rewriter/coq-rewriter.0.0.9/opam +++ b/released/packages/coq-rewriter/coq-rewriter.0.0.9/opam @@ -13,8 +13,7 @@ build: [ install: [make "install"] depends: [ "conf-findutils" {build} - "ocaml" {build} - "ocaml" {build & >= "4.14.0" & arch != "arm64"} + "ocaml" {build & (arch = "x86_32" | arch = "x86_64" | >= "4.14.0")} "coq" {>= "8.15~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git"