From ae8a4092dcfca5403c41ff194808c60b33b9df20 Mon Sep 17 00:00:00 2001 From: coqbot Date: Tue, 14 Nov 2023 07:11:21 +0000 Subject: [PATCH] Set up CI minimization run for ci-metacoq At coq/coq@a6df8f61caaa26b1df354402e503a4f5ebe56ffa over coq/coq@b10573deb4f3e0aecf74692af95f84127576c8d9 --- .github/workflows/main.yml | 2 +- coqbot-request-stamp | 2 +- coqbot.ci-target | 2 +- coqbot.compiler | 2 +- coqbot.failing-artifact-urls | 2 +- coqbot.failing-sha | 2 +- coqbot.issue-number | 1 + coqbot.passing-artifact-urls | 2 +- coqbot.passing-sha | 2 +- coqbot.resume-minimization-url | 1 + coqbot.resumption-args | 8 ++++++++ coqbot.url | 1 + 12 files changed, 19 insertions(+), 8 deletions(-) create mode 100644 coqbot.resume-minimization-url create mode 100644 coqbot.resumption-args diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 55a353e..d62d72b 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -20,7 +20,7 @@ jobs: - name: Run minimizer uses: coq-community/docker-coq-action@v1.4.1 with: - #custom_image: 'registry.gitlab.com/coq/coq:CACHEKEY' + custom_image: 'registry.gitlab.inria.fr/coq/coq:old_ubuntu_lts-V2023-06-30-8ca33f9dfd' #coq_version: 'latest' #ocaml_version: 'default' custom_script: ./timeout-run.sh diff --git a/coqbot-request-stamp b/coqbot-request-stamp index f747925..f404531 100644 --- a/coqbot-request-stamp +++ b/coqbot-request-stamp @@ -1 +1 @@ -DUMMY +PR_kwDOABUDh85fUEP4 <> coq-community/run-coq-bug-minimizer run-coq-bug-minimizer-391899341207 coq coq 18305 \ No newline at end of file diff --git a/coqbot.ci-target b/coqbot.ci-target index 2359f92..7569121 100644 --- a/coqbot.ci-target +++ b/coqbot.ci-target @@ -1 +1 @@ -TAKE FROM failing-log.log +ci-metacoq diff --git a/coqbot.compiler b/coqbot.compiler index 2da4316..92c3b40 100644 --- a/coqbot.compiler +++ b/coqbot.compiler @@ -1 +1 @@ -4.10.0 +4.09.0 diff --git a/coqbot.failing-artifact-urls b/coqbot.failing-artifact-urls index 8b13789..d5677f5 100644 --- a/coqbot.failing-artifact-urls +++ b/coqbot.failing-artifact-urls @@ -1 +1 @@ - +https://gitlab.inria.fr/coq/coq/-/jobs/3591790/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3592598/artifacts/download diff --git a/coqbot.failing-sha b/coqbot.failing-sha index 8b13789..de8e971 100644 --- a/coqbot.failing-sha +++ b/coqbot.failing-sha @@ -1 +1 @@ - +a6df8f61caaa26b1df354402e503a4f5ebe56ffa diff --git a/coqbot.issue-number b/coqbot.issue-number index e69de29..f3b2dc7 100644 --- a/coqbot.issue-number +++ b/coqbot.issue-number @@ -0,0 +1 @@ +18305 diff --git a/coqbot.passing-artifact-urls b/coqbot.passing-artifact-urls index 8b13789..7cea5b9 100644 --- a/coqbot.passing-artifact-urls +++ b/coqbot.passing-artifact-urls @@ -1 +1 @@ - +https://gitlab.inria.fr/coq/coq/-/jobs/3591527/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3591611/artifacts/download diff --git a/coqbot.passing-sha b/coqbot.passing-sha index 8b13789..f190949 100644 --- a/coqbot.passing-sha +++ b/coqbot.passing-sha @@ -1 +1 @@ - +b10573deb4f3e0aecf74692af95f84127576c8d9 diff --git a/coqbot.resume-minimization-url b/coqbot.resume-minimization-url new file mode 100644 index 0000000..4f09f09 --- /dev/null +++ b/coqbot.resume-minimization-url @@ -0,0 +1 @@ +https://coqbot.herokuapp.com/resume-ci-minimization diff --git a/coqbot.resumption-args b/coqbot.resumption-args new file mode 100644 index 0000000..69f192a --- /dev/null +++ b/coqbot.resumption-args @@ -0,0 +1,8 @@ +registry.gitlab.inria.fr/coq/coq:old_ubuntu_lts-V2023-06-30-8ca33f9dfd +ci-metacoq +4.09.0 +https://gitlab.inria.fr/coq/coq/-/jobs/3591790/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3592598/artifacts/download +https://gitlab.inria.fr/coq/coq/-/jobs/3591527/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3591611/artifacts/download +b10573deb4f3e0aecf74692af95f84127576c8d9 +a6df8f61caaa26b1df354402e503a4f5ebe56ffa + diff --git a/coqbot.url b/coqbot.url index e69de29..fa1cbeb 100644 --- a/coqbot.url +++ b/coqbot.url @@ -0,0 +1 @@ +https://coqbot.herokuapp.com/ci-minimization