How do I get the output of dune exec?
you run it?
Yes, but on the shim its completely silent
dune exec -- dev/shim/coqc-prelude not-a-real-file doesn't print an error?
That prints an error
Ok im doing something wrong I guess
I'm trying to generate the .out file for a test
whats the best way to do this
My output should be a coq message not an error so it looks like it isn't printed
OK, nevermind I think my file is just wrong
what sort of message? for instance coqc won't print the "foo is defined" messages but does print Check output
Ah, that's why I'm confused
How do I get those to print?
if you want to test coqtop messages you have to run coqtop
coqtop < file.v
Is it easy to add a folder in
fail or do I have to change the makefile
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: Jun 09 2023 at 07:01 UTC