Conversation
| ring/field expressions before applying the proof procedures.""" | ||
|
|
||
| build: [make "-j%{jobs}%"] | ||
| build: [make "-j%{jobs}%" "build"] |
There was a problem hiding this comment.
This is wrong for two reasons:
- This file is auto-generated from meta.yml.
- There is a
run-testfield below. What's written in thisbuildfield should not run the test suite.
There was a problem hiding this comment.
Oh, wait. Did you change the behavior of make to run the test suite? (Well, that looks wrong anyway.)
How does that run the test suite in the CI of MathComp and Rocq opam archive?
There was a problem hiding this comment.
This file is auto-generated from meta.yml.
Right, we have to set the make_target variable there apparently.
How does that run the test suite in the CI of MathComp and Rocq opam archive?
I don't know about the OPAM archive CI but we'll get it into Rocq's own CI and all the nix based one (including MC) which is the most important.
There was a problem hiding this comment.
Although I agree that we should run the test suite in Rocq and MathComp CI, that should be done on the CI side, not by tweaking the default make target.
There was a problem hiding this comment.
Unfortunately, doing this requires some non trivial work (otherwise it would already have been done for long). Meanwhile, I prefer having something that "looks wrong" than something potentially broken without us even noticing. Note that the proposed Makefile scheme is not so exotic, at least elpi and HB are doing something similar.
There was a problem hiding this comment.
I suggest discussing it tomorrow.
So that various CIs will run the tests.
It seems to break on some test: https://gitlab.inria.fr/coq/coq/-/jobs/5738407 ~~~ COQNATIVE examples/from_sander.vo Fatal error: exception Stack overflow ~~~ (I think the test wasn't run until math-comp/algebra-tactics#116)
It seems to break on some test: https://gitlab.inria.fr/coq/coq/-/jobs/5738407 ~~~ COQNATIVE examples/from_sander.vo Fatal error: exception Stack overflow ~~~ (I think the test wasn't run until math-comp/algebra-tactics#116)
2 participants
Once we work again on MC master, we should probably merge this so that various CIs do run the test-suite.