Stream: Coq devs & plugin devs

Topic: Strange lexing error


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

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

view this post on Zulip Laurent Théry (Feb 06 2023 at 11:57):

ir is ok with vscoq too

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

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

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

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

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

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

view this post on Zulip 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: Mar 28 2024 at 21:01 UTC