Zulip Chat Archive

Stream: lean4

Topic: rfc: update error message for misplaced doc comments


Alok Singh (Apr 26 2025 at 08:09):

GPT often puts doc comments in inapropos spots (namespace, section, import, open) but even I've done it and scratched my head a second figuring out the error since it gives a rather long and a bit crytpic parse error:

unexpected token 'namespace'; expected '#guard_msgs', 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_dsimproc', 'builtin_dsimproc_decl', 'builtin_grind_propagator', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'dsimproc', 'dsimproc_decl', 'elab', 'elab_rules', 'example', 'grind_propagator', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'recommended_spelling', 'register_tactic_tag', 'simproc', 'simproc_decl', 'structure', 'syntax', 'tactic_extension', 'theorem' or 'unif_hint'

I propose that the error message reflect that doc comments can't be put on that item, and specifically mentions doc comments in the error message for benefit of man and machine.

Joachim Breitner (Apr 27 2025 at 13:19):

(JFTR: Open issue for that: https://github.com/leanprover/lean4/issues/7591)


Last updated: May 02 2025 at 03:31 UTC