Stream: Coq devs & plugin devs

Topic: Best way to get output of dune exec


view this post on Zulip Ali Caglayan (Jul 23 2021 at 14:50):

How do I get the output of dune exec?

view this post on Zulip Gaëtan Gilbert (Jul 23 2021 at 14:51):

you run it?

view this post on Zulip Ali Caglayan (Jul 23 2021 at 14:51):

Yes, but on the shim its completely silent

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Jul 23 2021 at 14:52):

That prints an error

view this post on Zulip Ali Caglayan (Jul 23 2021 at 14:52):

Ok im doing something wrong I guess

view this post on Zulip Ali Caglayan (Jul 23 2021 at 14:53):

I'm trying to generate the .out file for a test

view this post on Zulip Ali Caglayan (Jul 23 2021 at 14:53):

whats the best way to do this

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Jul 23 2021 at 14:55):

OK, nevermind I think my file is just wrong

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Jul 23 2021 at 14:56):

Ah, that's why I'm confused

view this post on Zulip Ali Caglayan (Jul 23 2021 at 14:56):

How do I get those to print?

view this post on Zulip 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

view this post on Zulip 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


Last updated: Oct 21 2021 at 21:03 UTC