Pierre Courtieu
Pierre Courtieu
Actually I just checked and "Show" does print the info messages too. I was not aware of that (although I implemented these messages...). So maybe being completely silent and only...
OK I will first make a branch a test with several versions of coq to see if we need backward compatibility checks. Basically this is a variant of @cpitclaudel workaround:...
In fine we may still need a specific pseudo-silent mode anyway.
> I will move these missing messages to remain outside silent. Another thing we could do is to have `-emacs` set silent. Is it reasonable to change the behaviour of...
> Can we make sure that this doesn't break company-coq? I think it uses `xxx defined` as a sign that it needs to reload completion lists. Indeed this probably breaks...
> So maybe the better plan is just to make `-emacs` not to print goals, we let PG use the default not silent mode. OK but this must wait for...
OK this breaks a few other things anyway: commands like "Fail xxx." "Show Intros." etc do not display anything. Lots a features of both pg and company-coq depend on this.
Yes it breaks these features currently.
Hi, indeed this is a bug of the detection of "goal openers" of coq. I'll try to fix this scary pieace of code but meanwhile there is a workaround: put...
Hi there, Maybe we can patch coq_makefile with an option to output the command line options it has computed? That would make the whole thing more robust to changes in...