Stream: VsCoq devs & users

Topic: Where does QuickChick output go?


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

view this post on Zulip Paolo Giarrusso (Mar 15 2022 at 19:17):

Have you found the drop-down with all the panes?
image.png

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

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

view this post on Zulip Paolo Giarrusso (Mar 15 2022 at 21:42):

they match the log levels used by Coq (and CoqIDE?) but I agree they’re annoying…

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

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

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (Mar 16 2022 at 14:58):

OTOH, Ltac1's idtac uses Info.

view this post on Zulip Paolo Giarrusso (Mar 16 2022 at 14:59):

and idtac AFAIK is the only "logging mechanism" in Ltac1...

view this post on Zulip Michael Soegtrop (Mar 16 2022 at 16:58):

And as I said: QuickChick also uses Info.

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

view this post on Zulip Maxime Dénès (Mar 16 2022 at 17:04):

I definitely agree we should give the QuickChick and Info feedback a better treatment.

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

view this post on Zulip Paolo Giarrusso (Mar 16 2022 at 17:10):

so personally I still think we should change Info back.

view this post on Zulip Paolo Giarrusso (Mar 16 2022 at 17:12):

but I like all the other proposals as well, and some might make this debate irrelevant :-)

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

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

view this post on Zulip Michael Soegtrop (Mar 16 2022 at 18:01):

My opinion is:

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

view this post on Zulip Michael Soegtrop (Mar 16 2022 at 18:10):

Ideally, yes :-) C'est le provisoire qui dure ...

view this post on Zulip Meven Lennon-Bertrand (Mar 17 2022 at 09:12):

Michael Soegtrop said:

My opinion is:

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.

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

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

view this post on Zulip Fabian Kunze (Mar 17 2022 at 09:18):

What does PG do if a query does not find any result?

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

view this post on Zulip Théo Winterhalter (Mar 17 2022 at 09:20):

Yeah, a separator is really what I'm missing.

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

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

view this post on Zulip Michael Soegtrop (Mar 17 2022 at 09:34):

I think the "append and scroll" method would be fine with these two additions:

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

view this post on Zulip Théo Winterhalter (Mar 17 2022 at 09:45):

Search "=":
foo : 0 = 0
----------------
Search thing_that_doesnt_exist:
----------------

view this post on Zulip Michael Soegtrop (Mar 17 2022 at 12:58):

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:
================================================================================

view this post on Zulip Maxime Dénès (Mar 17 2022 at 14:04):

It reminds me of MS-DOS interfaces :)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 17 2022 at 14:19):

dBase III, these were the times!

view this post on Zulip Théo Winterhalter (Mar 17 2022 at 14:50):

Maybe VSCode has API to print a beautiful separation.

view this post on Zulip Michael Soegtrop (Mar 17 2022 at 17:53):

I admit that I counted the equal signs to fit on a Holerith punch card :-)

view this post on Zulip Fabian Kunze (Mar 18 2022 at 12:59):

I always wondered why 80 characters was such a magical number, now I understand :)


Last updated: Jan 30 2023 at 18:04 UTC