Skip to content

Add proof general tests to CI#21929

Draft
SkySkimmer wants to merge 1 commit intorocq-prover:masterfrom
SkySkimmer:pg-ci
Draft

Add proof general tests to CI#21929
SkySkimmer wants to merge 1 commit intorocq-prover:masterfrom
SkySkimmer:pg-ci

Conversation

@SkySkimmer
Copy link
Copy Markdown
Contributor

No description provided.

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 20, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 20, 2026
@SkySkimmer
Copy link
Copy Markdown
Contributor Author

I get errors in

  • make tests:
Test 020_coq-test-definition passed unexpectedly
   PASSED   2/14  020_coq-test-definition (0.303142 sec) at ci/coq-tests.el:203
Test 090_coq-test-regression-Fail passed unexpectedly
   PASSED   9/14  090_coq-test-regression-Fail (0.284647 sec) at ci/coq-tests.el:400
Test 091_coq-test-regression-Fail passed unexpectedly
   PASSED  10/14  091_coq-test-regression-Fail (0.254256 sec) at ci/coq-tests.el:425
  • compile-tests:
   FAILED  1/1  cct-change-recompile (3.632111 sec) at runtest.el:84
  • simple-tests:
Test test-coq-par-job-needs-compilation-quick condition:
    (error "create files with same time stamp failed")
   FAILED  1/1  test-coq-par-job-needs-compilation-quick (13.129966 sec) at coq-test-par-job-needs-compilation-quick.el:983

cc @Matafou

@SkySkimmer SkySkimmer added the needs: progress Work in progress: awaiting action from the author. label Apr 20, 2026
@Matafou
Copy link
Copy Markdown
Contributor

Matafou commented Apr 22, 2026

Thank you very much for this addition. This is due to the .vo{,s,k} empty files that not generated anymore by rocq compile.

@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Apr 29, 2026
@coqbot-app coqbot-app Bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels May 5, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. needs: progress Work in progress: awaiting action from the author.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants