search

coq-community / reduction-effects

A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]
Mozilla Public License 2.0
6 stars 6 forks source link

add opam #2

Closed liyishuai closed 5 years ago

liyishuai commented 5 years ago

resolve #1

liyishuai commented 5 years ago

I managed to compile the example. Where should I find the output?

JasonGross commented 5 years ago

You should see the printing on stdout, I think. (If not, I'd call it a bug.) You should definitely see it if you do cat $file.v | coqtop. I haven't tested this personally though.

Once you get the output working, I think you should make the test check that the output of running coqc on the test file matches expected output, and check in a .out or .out.expected file with the expected output.

Why "reduction-effect" rather than "reduction-effects" like the repo name?