Stream: Coq devs & plugin devs

Topic: SSR breaks parser?

Jason Gross (May 24 2022 at 20:23):

Is Require Coq.ssr.ssreflect supposed to make previously parseable statements unparseable? (Syntax error: 'of' or 'of' expected after 'type' (in [tactic:constr_eval]). in Ltac reify_type ty := type.reify ltac:(reify_base_type) constr:(base.type) ty.)

Gaëtan Gilbert (May 24 2022 at 20:28):

it has some notations using type as a keyword

Jason Gross (May 24 2022 at 20:31):

I thought notations and reserved notations followed Import?

Gaëtan Gilbert (May 24 2022 at 20:34):

I didn't see you wrote just require

Gaëtan Gilbert (May 24 2022 at 20:35):

I guess it's this

(* ssrvernac.mlg *)
GRAMMAR EXTEND Gram
  GLOBAL: constr_eval;
  constr_eval: TOP [
    [ IDENT "type"; "of"; c = Constr.constr -> { Genredexpr.ConstrTypeOf c }]
  ];
END

Gaëtan Gilbert (May 24 2022 at 21:02):

(* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *)
(* identifiers used as keywords. This is incompatible with ssreflect.v *)
(* which makes "by" and "of" true keywords, because of technicalities  *)
(* in the internal lexer-parser API of Coq. We patch this here by      *)
(* adding new parsing rules that recognize the new keywords.           *)

maybe we should just make of a keyword in the base grammar

Gaëtan Gilbert (May 24 2022 at 21:07):

Jason Gross said:

Is Require Coq.ssr.ssreflect supposed to make previously parseable statements unparseable? (Syntax error: 'of' or 'of' expected after 'type' (in [tactic:constr_eval]). in Ltac reify_type ty := type.reify ltac:(reify_base_type) constr:(base.type) ty.)

actually I don't get a syntax error

Require ssreflect.

Ltac reify_type ty := type.reify ltac:(reify_base_type) constr:(base.type) ty.

says Error: The reference reify_base_type was not found in the current environment.

Jason Gross (May 24 2022 at 22:08):

Hm, seems to not be an issue in 8.15, but is an issue in 8.11 :-/

Last updated: Oct 13 2024 at 01:02 UTC