Bug in Pretty Printing

[mukeshtiwari]

I recently switched to Coq-8.18.0 and VsCoq2. The following code does not parse very well.

From Coq Require Import NArith Utf8
    Bool Init.Byte Psatz Strings.Byte. 

Open Scope N_scope.
Definition np_total (np : N):  (np <? 256 = true) ->  byte.
Proof.
  intros H.
  refine(match (np <? 256) as b return ∀ mp, np = mp -> 
      (mp <? 256) = b -> _ with 
   | true => fun mp Hmp Hmpt => 
      match of_N mp as npt return _ = npt -> _ with 
      | Some x => fun _ => x
      | None => fun Hf => _  
      end eq_refl
   | false => fun mp Hmp Hmf => _
  end np eq_refl eq_refl).
  abstract(
  apply of_N_None_iff in Hf;
  apply N.ltb_lt in Hmpt; intuition nia).
  abstract (subst; congruence).
Defined.

Lemma np_true_tmp : forall np (Ha : np <? 256 = true) x, 
  of_N np = Some x -> np_total np Ha = x.
Proof.
  intros * Hb; unfold np_total.

[mukeshtiwari]

Never mind. I uninstalled all the plugins related to Coq and reinstalled VsCoq2 and it seems to work. Apologies for the noise. I am closing the issue.

[mukeshtiwari]

I removed my coq-lsp [1] (I am not sure if I need this or not) and proof-general keybindings. When I am searching for a relevant theorem, the message pane shows a list of theorems that matches the query.

However, if I try to do something which is an error, then message pane shows nothing. Is this an intended behaviour?

The only plugins I have installed right now are VsCoq2.0.1 and Coq Elpi lang v0.0.5.

[1] https://github.com/ejgallego/coq-lsp

[maximedenes]

I removed my coq-lsp [1]

You don't need coq-lsp for VsCoq to work. They are two independent projects.

When I am searching for a relevant theorem, the message pane shows a list of theorems that matches the query.

Note that you also have a dedicated query panel (you'll see a Coq icon if you activate the activity bar on the left). It may be more convenient than typing your queries in the Coq document.

However, if I try to do something which is an error, then message pane shows nothing. Is this an intended behaviour?

No, the errors are indeed expected to show up in the messages pane. Where is your cursor at, in the second screenshot?

[mukeshtiwari]

Note that you also have a dedicated query panel (you'll see a Coq icon if you activate the activity bar on the left). It may be more convenient than typing your queries in the Coq document.

Oh, that is nice! I will give it another shot, probably next week again.

No, the errors are indeed expected to show up in the messages pane. Where is your cursor at, in the second screenshot?

The cursor was just before the dot (.) but I tried to move along the command (rewrite Ha) as well, e.g., in the beginning or in the middle but I didn't get anything.

[mukeshtiwari]

I tried again and I think there is some bug in displaying the error messages. As you can see from the picture, my cursor is just before the dot (.) but there is no error message in the message pane.

I am using VsCoq v2.0.1 on Apple M1 Pro (macOS Sonoma 14.0)

[mukeshtiwari]

Some more issues: same file is opened in Vscode and Emacs.

[rtetley]

Concerning the errors, could it be that they are disabled in your user settings ? They are actually disabled by default. In settings check that Vscoq > Goals > Messages: Full is ticked. Concerning your latest issue it will be solved in the upcoming release (I plan to start the process today), see #664

[mukeshtiwari]

Concerning the errors, could it be that they are disabled in your user settings ? They are actually disabled by default. In settings check that Vscoq > Goals > Messages: Full is ticked.

Thanks! This worked for me.

More info on the previous Coq code. I typed the whole things and after some time, it crashed (see the output)

Then I restarted and it worked. I don't know what is going on but hopefully, it is helpful for you :)

[rtetley]

I think if you use unicode characters it will be very buggy (until the next release). This is because the version you are using does not handle such characters correctly and edits are not passed on correctly to the language server. This should be fixed in the upcoming release (just started the release process). Until then I would recommend against using unicode characters :-) Thanks for your feedback anyways ! Can we close this issue ? If you have anything else not relating to pretty printing we can open a new one ! Thanks again !

[mukeshtiwari]

Yeah, you can close the issue.

Best, Mukesh

On Mon, 16 Oct 2023 at 08:00, Romain Tetley @.***> wrote:

I think if you use unicode characters it will be very buggy (until the next release). This is because the version you are using does not handle such characters correctly and edits are not passed on correctly to the language server. This should be fixed in the upcoming release (just started the release process). Until then I would recommend against using unicode characters :-) Thanks for your feedback anyways ! Can we close this issue ? If you have anything else not relating to pretty printing we can open a new one ! Thanks again !

— Reply to this email directly, view it on GitHub https://github.com/coq-community/vscoq/issues/670#issuecomment-1763850357, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIVDZLIW6QTUTMFK6OXIBDX7TLRNANCNFSM6AAAAAA6AGPZ5U . You are receiving this because you modified the open/close state.Message ID: @.***>