gallais (Feb 06 2023 at 11:40): gallais (Feb 06 2023 at 11:40):I'm a dummy who can't remember Coq's syntax and so I write silly programs. Here's one that led to a strange lexing error (I'm using 8.15.0 according to CoqIDE):
Require Import List.
Inductive tree (a : Type) : Type := Node : a -> list (tree a) -> tree a.
Fixpoint pmaf {a b : Type} (t : tree a) (f : a -> b) : tree b
:= match t with
| Node _ v ts => Node _ (f v) (map (\ t => pmaf t f) ts)
end.
The issue is that I'm using \ t => instead of fun t => but the lexer error points at the t in (t : tree a) as the source of the problem.
Gaëtan Gilbert (Feb 06 2023 at 11:53):on 8.11 and 8.16 the error is located on the \ on my machine with PG
with coqide it has your bug
Laurent Théry (Feb 06 2023 at 11:57):ir is ok with vscoq too
Hugo Herbelin (Feb 06 2023 at 18:57):I would suspect a bad interaction with the unicode input mode in coqide, which recognizes tokens started with \.
Hugo Herbelin (Feb 06 2023 at 18:58):BTW, the loss of error location in master's coqide should probably be considered as "critical". Does anyone know what caused it and/or how to fix it?
Enrico Tassi (Feb 07 2023 at 06:31):@Théo Zimmermann and @Pierre-Marie Pédrot did investigate it. I don't have the pr at hand, but coq started to spit loc which are absolute, instead of relative to the sentence they apply to, and there is code in coqide to adapt to this change which is broken. It is somewhat also broken in 8.16, but less broken, whatever that means. PRs involved ate by Jim and Emilio, IIRC
Théo Zimmermann (Feb 07 2023 at 09:23):@Hugo Herbelin The PR that caused the regression was https://github.com/coq/coq/pull/16978 (with follow-up https://github.com/coq/coq/pull/17026). See https://github.com/coq/coq/issues/17023 for the report, and https://github.com/coq/coq/pull/17048 for a proposed fix. The problem is that Emilio does not understand the logic behind these code changes and would like a more principled fix. For 8.17.0, I can see two options. Either someone (e.g., you) is able to review, test and merge Jim's fix. Or we could revert Emilio's PRs. Let me know what you think.
Emilio Jesús Gallego Arias (Feb 07 2023 at 15:02):I'm happy to revert my PR tho, I didn't know what I was getting into
Hugo Herbelin (Feb 07 2023 at 22:41):If a revert is possible so that a more principled fix can be found is ok, then let's do that.
Otherwise, I don't know if I can easily review 17048, but I could at least test coqide for a couple of days with the patch, if worth to do.
Théo Zimmermann (Feb 08 2023 at 15:33):I'm happy to choose any of the two solutions, but I am under the impression that the reverting option is preferred to the "blind" merging of Jim's PR.
Last updated: Sep 09 2024 at 06:02 UTC