I was thinking about grouping some related tests together
but I guess it's not really worth it
Just give them the same name prefix.
Ali Caglayan has marked this topic as resolved.
When running the test-suite I keep getting this error:
File "unit-tests/lib/coqProject.ml", line 23, characters 6-13: 23 | docroot = None; ^^^^^^^ Error: This record expression is expected to have type CoqProject_file.project The field docroot does not belong to type CoqProject_file.project make: *** [Makefile:331: unit-tests/lib/coqProject.ml.log] Error 2
is that normal?
someone merge https://github.com/coq/coq/pull/14625 already
the test suite currently has bugs with the unit test setup, I'm guessing it's picking up your installed coq instead of the development coq
I'm confused. I added some tests that will fail to failure but the CI says they "should be rejected"? https://github.com/coq/coq/pull/14699/checks?check_run_id=3145593030
iirc failure/ works just like success/, you should just use success/ with Fail
In that case I can stick them all in one file probably
Last updated: Oct 21 2021 at 21:03 UTC