vscoq
vscoq copied to clipboard
Print Notices/Error messages etc. in same buffer
Similar to how to CoqIDE prints information, we should print all information in a buffer which refreshes on each print. We can also have another log of all past messages (or separate them if need be). But it is very confusing at the moment to switch between Notices etc.
To demonstrate how broken things are currently, when doing something like:
Fail Check (Set : Set).
Doesn't output anywhere I can find.
Odd, for me it opens directly the "Notice" panel (was closed before) and prints:
The command has indeed failed with message:
In environment
state : Type
The term "Set" has type "Type" while it is expected to have type
"Set" (universe inconsistency: Cannot enforce Set+1 <= Set).
which I think is the expected behaviour.
Hmm it seems to be working now that I restarted VSCoq. I am not sure what happened there.
Anyway, my point still stands. We should have a buffer that collects all of these and shows the newest and make that the default.
Adding this to the VsCoq 2 road map as it doesn't seem to work.