search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
152 stars 32 forks source link

[server] Printing seems to forget about abbreviations. #387

Open ejgallego opened 1 year ago

ejgallego commented 1 year ago

The following document prints badly:

Notation a := 3.

Goal a = 3.
Proof. now reflexivity. Qed.

Goal min 3 3 = 3.
Proof. now reflexivity. Qed.

In both cases the abbreviation won't be properly printed.

I've confirmed this is a Coq bug, fails on v8.15, v8.16, v8.17, master using CoqIDE.

herbelin commented 1 year ago

Hum, I believe it is a "race" condition between using primitive notations and using abbreviations/notations, the former taking precedence over the latter independently of which declaration is most recent. You can probably consider it a Coq oddity to eventually be addressed.

ejgallego commented 1 year ago

Thanks @herbelin , I thought that was a problem with the coq-lsp setup, but indeed it prints badly in Coq too, not only for numeric notations, also min is printed in the goal as Nat.min.

That makes some developments to look weird.

Not sure if I should submit this as a Coq bug.

Alizter commented 1 year ago

I tested it for a regular axiom (no number notations) and the issue persists. i.e.

Axiom A : Type.
Axiom a : A.
Notation a' := a.
Goal a' = a.
ejgallego commented 1 year ago

Yup, same for CoqIDE back to 8.15

ejgallego commented 1 year ago

@Alizter not sure about the tags here, but we are gonna need a way to classify a large number of issues / bugs that are really upstream.

Actualy moving this to the Coq namespace as you suggested would allow us to transfer the issues more easily.