Ali Caglayan (Jul 23 2021 at 14:50): Ali Caglayan (Jul 23 2021 at 14:50):How do I get the output of dune exec?
Gaëtan Gilbert (Jul 23 2021 at 14:51):you run it?
Ali Caglayan (Jul 23 2021 at 14:51):Yes, but on the shim its completely silent
Gaëtan Gilbert (Jul 23 2021 at 14:52):you mean dune exec -- dev/shim/coqc-prelude not-a-real-file doesn't print an error?
Ali Caglayan (Jul 23 2021 at 14:52):That prints an error
Ali Caglayan (Jul 23 2021 at 14:52):Ok im doing something wrong I guess
Ali Caglayan (Jul 23 2021 at 14:53):I'm trying to generate the .out file for a test
Ali Caglayan (Jul 23 2021 at 14:53):whats the best way to do this
Ali Caglayan (Jul 23 2021 at 14:54):My output should be a coq message not an error so it looks like it isn't printed
Ali Caglayan (Jul 23 2021 at 14:55):OK, nevermind I think my file is just wrong
Gaëtan Gilbert (Jul 23 2021 at 14:55):what sort of message? for instance coqc won't print the "foo is defined" messages but does print Check output
Ali Caglayan (Jul 23 2021 at 14:56):Ah, that's why I'm confused
Ali Caglayan (Jul 23 2021 at 14:56):How do I get those to print?
Gaëtan Gilbert (Jul 23 2021 at 14:57):if you want to test coqtop messages you have to run coqtop
eg coqtop < file.v
Ali Caglayan (Jul 23 2021 at 15:01):Is it easy to add a folder in sucess or fail or do I have to change the makefile
Gaëtan Gilbert (Jul 23 2021 at 15:03):not easy
what for?
Ali Caglayan (Jul 23 2021 at 15:07):I was thinking about grouping some related tests together
Ali Caglayan (Jul 23 2021 at 15:07):but I guess it's not really worth it
Guillaume Melquiond (Jul 23 2021 at 15:07):Just give them the same name prefix.
Notification Bot (Jul 23 2021 at 15:15):Ali Caglayan has marked this topic as resolved.
Ali Caglayan (Jul 23 2021 at 16:42):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?
Gaëtan Gilbert (Jul 23 2021 at 16:48):someone merge https://github.com/coq/coq/pull/14625 already
Gaëtan Gilbert (Jul 23 2021 at 16:49):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
Ali Caglayan (Jul 23 2021 at 18:12):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
Gaëtan Gilbert (Jul 23 2021 at 18:13):iirc failure/ works just like success/, you should just use success/ with Fail
Ali Caglayan (Jul 23 2021 at 18:13):oh
Ali Caglayan (Jul 23 2021 at 18:14):In that case I can stick them all in one file probably
Last updated: Jun 09 2023 at 07:01 UTC