Stream: Elpi users & devs

Topic: Requiring Elpi makes `lib.` a syntax error

Paolo Giarrusso (Mar 29 2023 at 13:06):

after From elpi Require Import elpi., I see many occurrences of lib.foo becoming a syntax error.

Worse, stepping back and forth fixes the error in the coqidetop — I guess that's clearly a bug? This is with coq-elpi.1.16.0 BTW.

I guess that's about the lib : syntax shadowing lib. but maybe failing to left-factor?

  term: LEVEL "0"
    [ [ "lib"; ":"; id = qualified_name -> { ...
      | "lib"; ":"; "@"; id = qualified_name -> { ...

Paolo Giarrusso (Mar 29 2023 at 13:07):

but I've only reverse-engineered Coq notations, and I know .mlgs can have more tricks under their sleeves...

Paolo Giarrusso (Mar 29 2023 at 13:51):

minimized:

Module a.
  Module lib.
    Definition a := 0.
  End lib.
End a.
Import a.
Check a.lib.a.
Check lib.a.

From elpi Require elpi.
(* Step over the above, and do NOT step back *)

Check a.lib.a. (* works. *)

(* Check lib.a. (* Fails *) *)
Module lib. (* Fails. *)
  Definition a := 0.
End lib.

Enrico Tassi (Mar 29 2023 at 14:02):

Hum, I see, it is expected but maybe a bad choice. In practice it turns "lib" into a keyword

Enrico Tassi (Mar 29 2023 at 14:05):

Years after that addition, I believe it is not very useful. But purging it would require some work.
In the early days writing {{ foo }} would not resolve foo to a Coq name once and forall, so "coqlib" was better. Today names in term quotations are resolved statically, so the feature serves no purpose IMO.

Paolo Giarrusso (Mar 29 2023 at 14:53):

could you make lib: a keyword instead? I'm assuming the lexer has better backtracking...

Enrico Tassi (Mar 29 2023 at 18:15):

Yes, but then forall (lib : nat) and foralll (lib: nat) would be different, and that would be confusing

Paolo Giarrusso (Mar 29 2023 at 20:10):

It wouldn't be the first time, and that example is a bit easier to workaround compared to Import lib.foo. where lib. is external

Paolo Giarrusso (Mar 29 2023 at 20:11):

Anyway, thank you for the prompt response; I'll file a bug on this.

Paolo Giarrusso (Mar 29 2023 at 20:49):

What about backtracking + syntax extension, and the fact this happens on require? Those seem both odd, and potentially the same oddity...

Last updated: Oct 13 2024 at 01:02 UTC