Set up CI minimization run for ci-paco

coqbot · coqbot · commit 5942dbe86660 · 2025-12-11T21:45:24.000Z
At rocq-prover/rocq@fa138fc over rocq-prover/rocq@f2a0e56
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -21,7 +21,7 @@ jobs:
     - name: Run minimizer
       uses: coq-community/docker-coq-action@v1.5.2
       with:
-        #custom_image: 'registry.gitlab.com/coq/coq:CACHEKEY'
+        custom_image: 'registry.gitlab.inria.fr/coq/coq:edge_ubuntu-V2025-12-02-e6edb0cc32'
         #coq_version: 'latest'
         #ocaml_version: 'default'
         custom_script: ./timeout-run.sh
diff --git a/coqbot-request-stamp b/coqbot-request-stamp
@@ -1 +1 @@
-DUMMY
+PR_kwDOABUDh861ERWj <> rocq-community/run-coq-bug-minimizer run-coq-bug-minimizer-1067465257246 rocq-prover rocq 21356
diff --git a/coqbot.ci-target b/coqbot.ci-target
@@ -1 +1 @@
-TAKE FROM failing-log.log
+ci-paco
diff --git a/coqbot.ci-targets b/coqbot.ci-targets
@@ -0,0 +1 @@
+paco
diff --git a/coqbot.compiler b/coqbot.compiler
@@ -1 +1 @@
-4.10.0
+4.14.2+flambda
diff --git a/coqbot.failing-artifact-urls b/coqbot.failing-artifact-urls
@@ -1 +1 @@
-
+https://gitlab.inria.fr/coq/coq/-/jobs/6583825/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/6583793/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/6583827/artifacts/download
diff --git a/coqbot.failing-sha b/coqbot.failing-sha
@@ -1 +1 @@
-
+fa138fc84336e4c9af03c5eaca769bfacfd4c3a6
diff --git a/coqbot.issue-number b/coqbot.issue-number
@@ -0,0 +1 @@
+21356
diff --git a/coqbot.passing-artifact-urls b/coqbot.passing-artifact-urls
@@ -1 +1 @@
-
+https://gitlab.inria.fr/coq/coq/-/jobs/6583248/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/6583216/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/6583250/artifacts/download
diff --git a/coqbot.passing-sha b/coqbot.passing-sha
@@ -1 +1 @@
-
+f2a0e567c0448873df70443e2e86122bbb7f53b7
diff --git a/coqbot.resume-minimization-url 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
@@ -0,0 +1,9 @@
+registry.gitlab.inria.fr/coq/coq:edge_ubuntu-V2025-12-02-e6edb0cc32
+ci-paco
+paco
+4.14.2+flambda
+https://gitlab.inria.fr/coq/coq/-/jobs/6583825/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/6583793/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/6583827/artifacts/download
+https://gitlab.inria.fr/coq/coq/-/jobs/6583248/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/6583216/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/6583250/artifacts/download
+f2a0e567c0448873df70443e2e86122bbb7f53b7
+fa138fc84336e4c9af03c5eaca769bfacfd4c3a6
+
diff --git a/coqbot.url b/coqbot.url
@@ -0,0 +1 @@
+https://coqbot.herokuapp.com/ci-minimization

Original file line number	Diff line number	Diff line change
`@@ -1 +1 @@`
`1`		`-DUMMY`
	`1`	`+PR_kwDOABUDh861ERWj <> rocq-community/run-coq-bug-minimizer run-coq-bug-minimizer-1067465257246 rocq-prover rocq 21356`
Original file line number	Diff line number	Diff line change
`@@ -1 +1 @@`
`1`		`-`
	`1`	`+https://gitlab.inria.fr/coq/coq/-/jobs/6583825/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/6583793/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/6583827/artifacts/download`
Original file line number	Diff line number	Diff line change
`@@ -1 +1 @@`
`1`		`-`
	`1`	`+fa138fc84336e4c9af03c5eaca769bfacfd4c3a6`
Original file line number	Diff line number	Diff line change
`@@ -1 +1 @@`
`1`		`-`
	`1`	`+f2a0e567c0448873df70443e2e86122bbb7f53b7`