coqbot-app[bot]

Results 739 comments of coqbot-app[bot]

[auto] set use_metas_eagerly_in_conv_on_closed_terms = true

I have initiated minimization at commit 4474ce1a650a0ac2488d19784d7a9ec106f5eb48 for the suggested target ci-relation_algebra as requested.

[auto] set use_metas_eagerly_in_conv_on_closed_terms = true

Error: Could not minimize file /github/workspace/builds/coq/coq-failing/_build_ci/relation_algebra/theories/fhrel.v (from ci-relation_algebra) (full log [on GitHub Actions](https://github.com/coq-community/run-coq-bug-minimizer/actions/runs/3017896670), cc @JasonGross) build log (truncated to last 26KiB; full 2.5MiB file on GitHub Actions Artifacts under build.log)...

[auto] set use_metas_eagerly_in_conv_on_closed_terms = true

:checkered_flag: Bench results: ``` ┌──────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬─────────────────┐ │ │ user time [s] │ CPU cycles │ CPU instructions │ max resident mem [KB] │ mem faults │ │ │ │ │ │...

Fixes #16303: evar defined before its instance was checked, leading to error message trying to unexpectingly display an already defined evar

:red_circle: CI failures at commit 1ad2530ba95dc34d08b30b8b606c3fe9e126556c without any failure in the test-suite :heavy_check_mark: Corresponding jobs for the base commit 18cf00f4796df43adce6578c15752d839d83c071 succeeded :grey_question: Ask me to try to extract minimal test...

Fixes #16303: evar defined before its instance was checked, leading to error message trying to unexpectingly display an already defined evar

:red_circle: CI failures at commit 9bc7c1143cdce011e963f3012719f7fba64a96ca without any failure in the test-suite :heavy_check_mark: Corresponding jobs for the base commit 18cf00f4796df43adce6578c15752d839d83c071 succeeded :grey_question: Ask me to try to extract minimal test...

Fixes #16303: evar defined before its instance was checked, leading to error message trying to unexpectingly display an already defined evar

I have initiated minimization at commit 9bc7c1143cdce011e963f3012719f7fba64a96ca for the suggested targets ci-bedrock2, ci-jasmin as requested.

Fixes #16303: evar defined before its instance was checked, leading to error message trying to unexpectingly display an already defined evar

Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/bedrock2/deps/riscv-coq/src/riscv/Platform/Minimal.v (from ci-bedrock2) (full log [on GitHub Actions](https://github.com/coq-community/run-coq-bug-minimizer/actions/runs/2655605086)) We are collecting data on the user experience of the Coq Bug Minimizer. If you haven't already filled the survey...

Fixes #16303: evar defined before its instance was checked, leading to error message trying to unexpectingly display an already defined evar

Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/jasmin/proofs/compiler/tunneling_proof.v (from ci-jasmin) (interrupted by timeout, being automatically continued) (full log [on GitHub Actions](https://github.com/coq-community/run-coq-bug-minimizer/actions/runs/2655605113)) Minimized Coq File (consider adding this file to the test-suite) ```coq (* -*- mode:...

Fixes #16303: evar defined before its instance was checked, leading to error message trying to unexpectingly display an already defined evar

Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/jasmin/proofs/compiler/tunneling_proof.v (from ci-jasmin) (interrupted by timeout, being automatically continued) (full log [on GitHub Actions](https://github.com/coq-community/run-coq-bug-minimizer/actions/runs/2657451999)) Partially Minimized Coq File (could not inline CoqWord.word) ```coq (* -*- mode: coq; coq-prog-args:...

Fixes #16303: evar defined before its instance was checked, leading to error message trying to unexpectingly display an already defined evar

Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/jasmin/proofs/compiler/tunneling_proof.v (from ci-jasmin) (interrupted by timeout, being automatically continued) (full log [on GitHub Actions](https://github.com/coq-community/run-coq-bug-minimizer/actions/runs/2659163159)) Partially Minimized Coq File (could not inline CoqWord.word) ```coq (* -*- mode: coq; coq-prog-args:...