Set Printing Xyz options are not honored

[thery]

I don't know if it is the intended behaviour. But when executing Set Printing All the command is valid only on the current goal.

Goal 1 = 1 -> 2 = 1.
Set Printing All.
intro.

[Blaisorblade]

Right now the command gives a warning (IIRC) and suggests using a vscode command (display basic low-level...), so this might be closable.

[Blaisorblade]

Also, I think this works the same way in CoqIDE and is intended...

[fakusb]

I find it very strange that setting printing flags does not effect Queries, e.g. "Print term.".

Every other CoqIDE does so and a lot of demos depend on that behaviour. We give a course on Coq an this inconsistent behaviour nearly is a dealbreaker for VSCode.

[Blaisorblade]

Flags do work, you must set them via IDE commands, like with CoqIDE — instead of Set Printing All., use > Display All Basic Low-level Contents. (from the command palette)
A separate (and annoying) problem is that this works when running Print term. but not for > Coq: Print (or Cmd/Ctrl-Shift-P).

[fakusb]

Ok, that is a workaround for me, but it still is hard for an beginner if he encounters this in a demo file, where the author of the demo wants to show something about implicit arguments for example, and the user wonders why he does not see any implicit arguments.

Is it a conscious design decision that "Set Printing" flags are not respected/"noticed" on the level of Vernacular-queries?

[thery]

Looking at implicit argument is such a frequent practice when proving in Coq that
in a modern ide like vscode it would be nice to have a dedicated tool, such that
a tool-tip when mousing-over term.

[maximedenes]

I agree there's a lot to improve there. Hopefully, it will be much easier to implement once we get #140.

[Blaisorblade]

@fakusb Good point on "demo files".

Is it a conscious design decision that "Set Printing" flags are not respected/"noticed" on the level of Vernacular-queries?

That's consistent with CoqIDE, which tells you to use the commands, so I assume it's intentional — but it might still be questionable.

[QinshiWang]

It seems > Coq: Print Implicit Arguments does not work properly. It should do Set Printing Implicit like CoqIDE, but it happens to open a menu.

[TheoWinterhalter]

It's > Coq: Display Implicit Arguments and it shows you a list of toggles, so I guess it does its job?

[QinshiWang]

@TheoWinterhalter Thanks for your reply. But implicit arguments refer to link (or link for examples). In CoqIDE, Display Implicit Arguments means to only display these implicit arguments, but not notations, coercions, etc. I hope VSCoq also has an option to display these arguments only.

[Blaisorblade]

@QinshiWang Selecting the "Implicit Arguments" toggle in the menu that appears should do the right thing.

@TheoWinterhalter However, that a list of toggles appears is a bug — none of the other completions of Coq: Display... do that.

[TheoWinterhalter]

Ah ok. I thought this was actually nice.

[fakusb]

For me, pressing enter ob the popping-up menu does also not do anything. But it works for you, theo?

[TheoWinterhalter]

Yes, it seems to work.

[QinshiWang]

@fakusb It seems also to do nothing for me. I am using VSCoq 0.3.2 from VS Code extension market.

[TheoWinterhalter]

Ok, it doesn't work for all of the toggles indeed. "Notation" works for me, but not "Implicit Arguments".

[fakusb]

I'm firing up my debugger and tryu to fix this

[fakusb]

That other issue is handled in #182. I have a build of my forks current master-branch, including other improvements, at https://github.com/fakusb/vscoq/releases/tag/0.3.3-alpha4-custom

[maxild]

I am a self-learner/beginner going through Basics.v from SF (first book)...

When I use Check on a defintion I would like to see the result in pretty-printed notation. Instead I see the actual low level terms. That is I would like to see

Check mult_n_O.
    : forall n : nat, 0 = n * 0   

Instead I see

Check mult_n_O.
    : forall n : nat, @eq nat O (Nat.mul n O)

I have tried Set Printing All. in the coq/gallina source, and various > Coq: Display... commands in the vscode IDE, but haven't found a solution. Using coqtop in my terminal works as expected.

Is this specific to VsCoq (and due to this issue)?

[SkySkimmer]

Set Printing All is the opposite of what you want.

[maxild]

Set Printing All is the opposite of what you want.

Really?

Coq < Unset Printing Notations.

Coq < Check ((0 + 1) + 1) : nat.
Nat.add (Nat.add 0 1) 1 : nat
     : nat

Coq < Set Printing Notations.

Coq < Check ((0 + 1) + 1) : nat.
0 + 1 + 1 : nat
     : nat

Coq < Unset Printing All.

Coq < Check ((0 + 1) + 1) : nat.
0 + 1 + 1 : nat
     : nat

Coq < Set Printing All.

Coq < Check ((0 + 1) + 1) : nat.
Nat.add (Nat.add O (S O)) (S O) : nat
     : nat

So Printing All works the opposite compared to Printing Notation...weird

[maxild]

Anyway

Set Printing Notations.
Check ((0 + 1) + 1) : nat.
Unset Printing Notations.
Check ((0 + 1) + 1) : nat.

prints without using notations from inside VsCoq (in the vscode output panel)...Is this because of this unresolved issue?

[TheoWinterhalter]

For me vscoq always prints notation unless I tell it not to.
Set Printing All is not to be understood as using all options but as printing everything that the term might be hiding so this removes notations, shows coercions and implicit arguments, etc.

[maxild]

Set Printing All is not to be understood as using all options but as printing everything that the term might be hiding so this removes notations, shows coercions and implicit arguments, etc.

Okay thanks. Consistent with above. I probably (blindly) executed vscoq/IDE commands for >Coq: Display All Low Level Contents (guess this is eq to Set Printing All) and Coq: Display Notations (guess this is eq to Set Printing Notation), and now I know, that those 2 work opposite wrt notations. After restaring vscode notations are printed.

Is the preferred way to "toggle" printing settings using the vscoq IDE commands, and where can I see the current settings? (just tried using coqide, and it has a view menu with visible radio/toggle widgets)

[Blaisorblade]

Is the preferred way to "toggle" printing settings using the vscoq IDE commands

Yes

and where can I see the current settings?

Good question 👍

[andreiburdusa]

I'm working through Imp.v from Software Foundations and Coq> Display Implicit Arguments seems to have no effect.
Interpreting the line

Check @ceval_example2.

always gives

ceval_example2
	 : empty_st =[ X := 0; Y := 1; Z := 2 ]=> (Z !-> 2; Y !-> 1; X !-> 0)

Also, interpreting the line Set Printing Implicit. has no effect either, but it looks like that's expected from what I read above.

[Blaisorblade]

@andreiburdusa Your example is printed as a notation*, so the Implicit setting will not have an effect; you must first disable notations via Coq: Display Notations, and then the Implicit setting will have an effect.

*EDIT: this is an educated guess, but =[ isn't Coq built-in syntax so there are not many alternatives.

[Blaisorblade]

Upstream issue: coq/coq#16080.

And coq/coq#5178 is a different but related one.