From f174935b115df5536c3b0a554aec62295e245b7b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 1 Jul 2022 14:30:20 +0200 Subject: [PATCH 1/6] Set version in opam files --- coq-metacoq-erasure.opam | 2 +- coq-metacoq-pcuic.opam | 2 +- coq-metacoq-safechecker.opam | 2 +- coq-metacoq-template.opam | 4 ++-- coq-metacoq-translations.opam | 2 +- coq-metacoq.opam | 2 +- 6 files changed, 7 insertions(+), 7 deletions(-) diff --git a/coq-metacoq-erasure.opam b/coq-metacoq-erasure.opam index 187b2c510..e46424508 100644 --- a/coq-metacoq-erasure.opam +++ b/coq-metacoq-erasure.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.16.dev" +version: "1.0+8.16" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" diff --git a/coq-metacoq-pcuic.opam b/coq-metacoq-pcuic.opam index e3dda7f6a..aeeea9f95 100644 --- a/coq-metacoq-pcuic.opam +++ b/coq-metacoq-pcuic.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.16.dev" +version: "1.0+8.16" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" diff --git a/coq-metacoq-safechecker.opam b/coq-metacoq-safechecker.opam index dfc1027e5..0d16d9021 100644 --- a/coq-metacoq-safechecker.opam +++ b/coq-metacoq-safechecker.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.16.dev" +version: "1.0+8.16" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" diff --git a/coq-metacoq-template.opam b/coq-metacoq-template.opam index 476458d70..c6b9bb1a5 100644 --- a/coq-metacoq-template.opam +++ b/coq-metacoq-template.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.16.dev" +version: "1.0+8.16" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#master" @@ -29,7 +29,7 @@ depends: [ "stdlib-shims" "ocaml" {>= "4.07.1"} "coq" { > "8.16~" & < "8.17~" } - "coq-equations" { = "8.16.dev" } + "coq-equations" { = "1.0+8.16" } ] synopsis: "A quoting and unquoting library for Coq in Coq" description: """ diff --git a/coq-metacoq-translations.opam b/coq-metacoq-translations.opam index e62c00d55..de30cd086 100644 --- a/coq-metacoq-translations.opam +++ b/coq-metacoq-translations.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.16.dev" +version: "1.0+8.16" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" diff --git a/coq-metacoq.opam b/coq-metacoq.opam index f62d6e877..e80e836ef 100644 --- a/coq-metacoq.opam +++ b/coq-metacoq.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.16.dev" +version: "1.0+8.16" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" From 2db84ca6c9140acf5720d37e7fd9243e836ea5e7 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 1 Jul 2022 14:36:47 +0200 Subject: [PATCH 2/6] Fix equations dependency --- coq-metacoq-template.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq-metacoq-template.opam b/coq-metacoq-template.opam index c6b9bb1a5..ec229cf56 100644 --- a/coq-metacoq-template.opam +++ b/coq-metacoq-template.opam @@ -29,7 +29,7 @@ depends: [ "stdlib-shims" "ocaml" {>= "4.07.1"} "coq" { > "8.16~" & < "8.17~" } - "coq-equations" { = "1.0+8.16" } + "coq-equations" { = "1.3+8.16" } ] synopsis: "A quoting and unquoting library for Coq in Coq" description: """ From 566836107216abc80e174c093be6dd7d2b41178b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 1 Jul 2022 14:41:14 +0200 Subject: [PATCH 3/6] Fix build.yml --- .github/workflows/build.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index c691ee20c..1690e57cd 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -50,8 +50,6 @@ jobs: before_install: | startGroup "Print opam config" opam config list; opam repo list; opam list - opam pin -n coq-equations http://github.com/mattam82/Coq-Equations.git#8.16 - opam install --confirm-level=unsafe-yes coq-equations.8.16.dev endGroup script: | startGroup "Build project" From d28862920a094268e3a629852c5f805ef5229cc4 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 1 Jul 2022 15:35:40 +0200 Subject: [PATCH 4/6] Fix opam files and add make-opam-files script --- coq-metacoq-erasure.opam | 2 +- coq-metacoq-pcuic.opam | 2 +- coq-metacoq-safechecker.opam | 2 +- coq-metacoq-template.opam | 2 +- coq-metacoq-translations.opam | 2 +- coq-metacoq.opam | 2 +- make-opam-files.sh | 23 +++++++++++++++++++++++ 7 files changed, 29 insertions(+), 6 deletions(-) create mode 100755 make-opam-files.sh diff --git a/coq-metacoq-erasure.opam b/coq-metacoq-erasure.opam index e46424508..fffb25027 100644 --- a/coq-metacoq-erasure.opam +++ b/coq-metacoq-erasure.opam @@ -2,7 +2,7 @@ opam-version: "2.0" version: "1.0+8.16" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" -dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" bug-reports: "https://github.com/MetaCoq/metacoq/issues" authors: ["Abhishek Anand " "Danil Annenkov " diff --git a/coq-metacoq-pcuic.opam b/coq-metacoq-pcuic.opam index aeeea9f95..a27d9fb00 100644 --- a/coq-metacoq-pcuic.opam +++ b/coq-metacoq-pcuic.opam @@ -2,7 +2,7 @@ opam-version: "2.0" version: "1.0+8.16" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" -dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" bug-reports: "https://github.com/MetaCoq/metacoq/issues" authors: ["Abhishek Anand " "Danil Annenkov " diff --git a/coq-metacoq-safechecker.opam b/coq-metacoq-safechecker.opam index 0d16d9021..5a8e58c57 100644 --- a/coq-metacoq-safechecker.opam +++ b/coq-metacoq-safechecker.opam @@ -2,7 +2,7 @@ opam-version: "2.0" version: "1.0+8.16" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" -dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" bug-reports: "https://github.com/MetaCoq/metacoq/issues" authors: ["Abhishek Anand " "Danil Annenkov " diff --git a/coq-metacoq-template.opam b/coq-metacoq-template.opam index ec229cf56..89b744f4d 100644 --- a/coq-metacoq-template.opam +++ b/coq-metacoq-template.opam @@ -2,7 +2,7 @@ opam-version: "2.0" version: "1.0+8.16" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" -dev-repo: "git+https://github.com/MetaCoq/metacoq.git#master" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" bug-reports: "https://github.com/MetaCoq/metacoq/issues" authors: ["Abhishek Anand " "Danil Annenkov " diff --git a/coq-metacoq-translations.opam b/coq-metacoq-translations.opam index de30cd086..4650f21e6 100644 --- a/coq-metacoq-translations.opam +++ b/coq-metacoq-translations.opam @@ -2,7 +2,7 @@ opam-version: "2.0" version: "1.0+8.16" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" -dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" bug-reports: "https://github.com/MetaCoq/metacoq/issues" authors: ["Abhishek Anand " "Danil Annenkov " diff --git a/coq-metacoq.opam b/coq-metacoq.opam index e80e836ef..c3611df79 100644 --- a/coq-metacoq.opam +++ b/coq-metacoq.opam @@ -2,7 +2,7 @@ opam-version: "2.0" version: "1.0+8.16" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" -dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" bug-reports: "https://github.com/MetaCoq/metacoq/issues" authors: ["Abhishek Anand " "Danil Annenkov " diff --git a/make-opam-files.sh b/make-opam-files.sh new file mode 100755 index 000000000..be6bb62a5 --- /dev/null +++ b/make-opam-files.sh @@ -0,0 +1,23 @@ +#/usr/bin/env bash +echo "Target directory: " $1 +echo "Target version: " $2 +echo "Releases package: " $3 + +wget $3 +archive=`basename $3` +hash=`shasum -a 512 $archive | cut -f 1 -d " "` + +echo "Shasum = " $hash + +for f in *.opam; +do + opamf=${f/.opam/}; + target=$1/$opamf/$opamf.$2/opam; + echo $opamf; + mkdir $1/$opamf/$opamf.$2 + gsed -e "/^version:.*/d" $f > $target + echo url { >> $target + echo " src:" \"$3\" >> $target + echo " checksum:" \"sha512=$hash\" >> $target + echo } >> $target +done \ No newline at end of file From 79d92c4b7a9308f39ad17eda5d6fbda3c8932bbf Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 4 Jul 2022 10:18:35 +0200 Subject: [PATCH 5/6] Update version bounds --- coq-metacoq-template.opam | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/coq-metacoq-template.opam b/coq-metacoq-template.opam index 89b744f4d..3da933b4b 100644 --- a/coq-metacoq-template.opam +++ b/coq-metacoq-template.opam @@ -27,9 +27,8 @@ install: [ ] depends: [ "stdlib-shims" - "ocaml" {>= "4.07.1"} - "coq" { > "8.16~" & < "8.17~" } - "coq-equations" { = "1.3+8.16" } + "coq" { >= "8.16" & < "8.17~" } + "coq-equations" { >= "1.3" } ] synopsis: "A quoting and unquoting library for Coq in Coq" description: """ From 1095458218e2cdb41e2302ff0a85ae8c1ebf3e8d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 4 Jul 2022 10:43:46 +0200 Subject: [PATCH 6/6] Back to 8.16.dev versions --- coq-metacoq-erasure.opam | 2 +- coq-metacoq-pcuic.opam | 2 +- coq-metacoq-safechecker.opam | 2 +- coq-metacoq-template.opam | 2 +- coq-metacoq-translations.opam | 2 +- coq-metacoq.opam | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/coq-metacoq-erasure.opam b/coq-metacoq-erasure.opam index fffb25027..9b2959d38 100644 --- a/coq-metacoq-erasure.opam +++ b/coq-metacoq-erasure.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "1.0+8.16" +version: "8.16.dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" diff --git a/coq-metacoq-pcuic.opam b/coq-metacoq-pcuic.opam index a27d9fb00..c0936d524 100644 --- a/coq-metacoq-pcuic.opam +++ b/coq-metacoq-pcuic.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "1.0+8.16" +version: "8.16.dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" diff --git a/coq-metacoq-safechecker.opam b/coq-metacoq-safechecker.opam index 5a8e58c57..18918367e 100644 --- a/coq-metacoq-safechecker.opam +++ b/coq-metacoq-safechecker.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "1.0+8.16" +version: "8.16.dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" diff --git a/coq-metacoq-template.opam b/coq-metacoq-template.opam index 3da933b4b..8ab9c0b3e 100644 --- a/coq-metacoq-template.opam +++ b/coq-metacoq-template.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "1.0+8.16" +version: "8.16.dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" diff --git a/coq-metacoq-translations.opam b/coq-metacoq-translations.opam index 4650f21e6..9f930a7a5 100644 --- a/coq-metacoq-translations.opam +++ b/coq-metacoq-translations.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "1.0+8.16" +version: "8.16.dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" diff --git a/coq-metacoq.opam b/coq-metacoq.opam index c3611df79..5d2288035 100644 --- a/coq-metacoq.opam +++ b/coq-metacoq.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "1.0+8.16" +version: "8.16.dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16"