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.

on 8.11 and 8.16 the error is located on the \ on my machine with PG

with coqide it has your bug

ir is ok with vscoq too

I would suspect a bad interaction with the unicode input mode in coqide, which recognizes tokens started with `\`

.

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?

@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

@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.

I'm happy to revert my PR tho, I didn't know what I was getting into

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.

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