Michael Soegtrop (Mar 15 2022 at 19:02): Michael Soegtrop (Mar 15 2022 at 19:02):I have an issue with QuickChick and VsCoq - I can't find where it writes its results.
Here is an example:
From QuickChick Require Import QuickChick.
Require Import ZArith.
Open Scope Z_scope.
Conjecture Test1: forall (a b : Z), a=b.
QuickChick Test1.
In CoqIDE this results in something like
QuickChecking Test1
0
-1
*** Failed after 2 tests and 1 shrinks. (0 discards)
In the Messages pane. I don't see where this goes on VsCoq. Since the QuickChick tactic always succeeds, this output is important.
Paolo Giarrusso (Mar 15 2022 at 19:17):Have you found the drop-down with all the panes?
image.png
Paolo Giarrusso (Mar 15 2022 at 19:18):Info, Queries, Notices and Debug belong to Coq; and Info messages don't activate the pane automatically.
Ali Caglayan (Mar 15 2022 at 21:33):I find multiple panes kind of useless and submitted an issue a while ago https://github.com/coq-community/vscoq/issues/281
Paolo Giarrusso (Mar 15 2022 at 21:42):they match the log levels used by Coq (and CoqIDE?) but I agree they’re annoying…
Paolo Giarrusso (Mar 15 2022 at 21:43):… if it’s right to call them log levels, then it doesn’t make sense to have multiple panes: if you select Debug you should still see messages from all levels, but correctly interleaved.
Ali Caglayan (Mar 15 2022 at 22:13):I don't mind them being collected in multiple windows but it would be very useful to have a single pane which collects all of them and doesn't accumulate them. Like CoqIDE has.
Ali Caglayan (Mar 15 2022 at 22:14):The "log levels" of Coq don't make a lot of sense, but that is a whole other cleanup job.
Paolo Giarrusso (Mar 15 2022 at 22:53):I mostly mind separate windows when a single command outputs to more than one window — so the last output hides everything else.
Michael Soegtrop (Mar 16 2022 at 08:00):I have seen the drop down but din't look under Info - this is where they are.
I tend to agree with @Ali Caglayan that it doesn't make a lot of sense to separate output by message category. I don't know any systems which do this. Usually one has such categories to control the amount of output - not the destination.
Having said that it doesn't make a lot of sense that QuickChick uses the "Info" category - it should more be treated like queries or notices.
Ali Caglayan (Mar 16 2022 at 11:05):Within Coq, queries, notices and info are treated somewhat inconsistency already. But I tend to agree that things can be made better when possible.
Paolo Giarrusso (Mar 16 2022 at 14:58):IIRC, @Maxime Dénès argued for hiding Info because it's not meant to be used for useful information.
Paolo Giarrusso (Mar 16 2022 at 14:58):OTOH, Ltac1's idtac uses Info.
Paolo Giarrusso (Mar 16 2022 at 14:59):and idtac AFAIK is the only "logging mechanism" in Ltac1...
Michael Soegtrop (Mar 16 2022 at 16:58):And as I said: QuickChick also uses Info.
Maxime Dénès (Mar 16 2022 at 17:04):Yes, the problem is probably the mix on the Coq / plugins side : IIRC Feedback.msg_info is meant to be used for feedback that makes sense only for the toplevel, e.g. Foo is defined. It is rather verbose.
Maxime Dénès (Mar 16 2022 at 17:04):I definitely agree we should give the QuickChick and Info feedback a better treatment.
Paolo Giarrusso (Mar 16 2022 at 17:10):@Maxime Dénès but AFAIK that's what we have in Proof General, and I haven't seen anybody complain about that.
Paolo Giarrusso (Mar 16 2022 at 17:10):so personally I still think we should change Info back.
Paolo Giarrusso (Mar 16 2022 at 17:12):but I like all the other proposals as well, and some might make this debate irrelevant :-)
Fabian Kunze (Mar 16 2022 at 17:14):Maybe having a scrollable panel on the bottom of the proof view, which contains a copy of all the 4 different output panels, would help?
Ali Caglayan (Mar 16 2022 at 17:53):I would also like something along this direction, perhaps adding another panel which shows the most recent message with no scroll back. The fact that I cannot open the terminal and the messages window at the same time bugs me a lot.
Michael Soegtrop (Mar 16 2022 at 18:01):My opinion is:
Ali Caglayan (Mar 16 2022 at 18:04):Ideally if we are to have our own window instead of the default VSCode output, we could configure all of this.
Michael Soegtrop (Mar 16 2022 at 18:10):Ideally, yes :-) C'est le provisoire qui dure ...
Meven Lennon-Bertrand (Mar 17 2022 at 09:12):Michael Soegtrop said:
My opinion is:
- the different panels for message categories (debug, info, warning, error I guess) should be merged
- this "messages" panel should be scrolling, but it wouldn't hurt to have a scrolling and a last one only variant
- the queries panel should be separate (and non scrolling, but again both might make sense or an option).
Re: scrolling vs non-scrolling, currently in the scrolling panels one can clear output, which is a cheap way to get the "last one only" behaviour when desired. This might be a way to go if one does not want to have an option to switch between both behaviours.
Théo Winterhalter (Mar 17 2022 at 09:14):I personally really like being able to have several results registered at the same time, in PG I sometimes would copy paste the result to keep it around, that's annoying.
Fabian Kunze (Mar 17 2022 at 09:18):I think there is great value in simply having the same behaviour as in proofgeneral (at least as a default), as many tools and users expect this behaviour. This would mean a single panel that is scrolling.
The problem of "Querys that fail to find don't print a notice that nothing was found" can be tackled differently, for instance by printing (no results) in the shared panel.
Fabian Kunze (Mar 17 2022 at 09:18):What does PG do if a query does not find any result?
Meven Lennon-Bertrand (Mar 17 2022 at 09:20):I agree that having a history around is often very nice (I hate it when trying to understand a notion hidden behind a notation and 3 definitions that I lose the output of the intermediate researches), but it also sometimes generates a lot of noise. For instance, when debugging typeclasses, it’s nice to have a blank state output to clearly know where a search starts.
Théo Winterhalter (Mar 17 2022 at 09:20):Yeah, a separator is really what I'm missing.
Théo Winterhalter (Mar 17 2022 at 09:21):Fabian Kunze said:
What does PG do if a query does not find any result?
If I recall, it's the same, you just don't know? But maybe you can start another query to see whether the other one is still busy.
Fabian Kunze (Mar 17 2022 at 09:24):Théo Winterhalter said:
If I recall, it's the same, you just don't know? But maybe you can start another query to see whether the other one is still busy.
That's also what I recall.
Michael Soegtrop (Mar 17 2022 at 09:34):I think the "append and scroll" method would be fine with these two additions:
Meven Lennon-Bertrand (Mar 17 2022 at 09:43):Regarding the header, I think a trade-off is that it should also not be too prominent, otherwise it might take a lot of space in the window and/or distract from the result of the query (which, after all, are the interesting part)
Théo Winterhalter (Mar 17 2022 at 09:45):Search "=":
foo : 0 = 0
----------------
Search thing_that_doesnt_exist:
----------------
I would do a longer separator line and maybe with a heavier character, since sometimes the ouput of Search can lengthy and one should see it when scrolling fast, but essentially this is what I had in mind. Maybe a double separator line like:
================================================================================
Search "=":
================================================================================
foo : 0 = 0
================================================================================
Search thing_that_doesnt_exist:
================================================================================
It reminds me of MS-DOS interfaces :)
Emilio Jesús Gallego Arias (Mar 17 2022 at 14:19):dBase III, these were the times!
Théo Winterhalter (Mar 17 2022 at 14:50):Maybe VSCode has API to print a beautiful separation.
Michael Soegtrop (Mar 17 2022 at 17:53):I admit that I counted the equal signs to fit on a Holerith punch card :-)
Fabian Kunze (Mar 18 2022 at 12:59):I always wondered why 80 characters was such a magical number, now I understand :)
Last updated: Jun 04 2023 at 23:30 UTC