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
Last updated: Oct 21 2021 at 21:03 UTC