diff --git a/src/Lean/DocString/Add.lean b/src/Lean/DocString/Add.lean index 554b0a19da..5d960a2ffb 100644 --- a/src/Lean/DocString/Add.lean +++ b/src/Lean/DocString/Add.lean @@ -206,10 +206,12 @@ Adds an elaborated Verso docstring to the environment. -/ def addVersoDocStringCore [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadError m] (declName : Name) (docs : VersoDocString) : m Unit := do - let throwImported {α} : m α := - throwError s!"invalid doc string, declaration '{declName}' is in an imported module" + -- The decl name can be anonymous due to attempts to elaborate incomplete syntax. If the name is + -- anonymous, the `MapDeclarationExtension.insert` panics due to not being on the right async + -- branch. Better to just do nothing. + if declName.isAnonymous then return unless (← getEnv).getModuleIdxFor? declName |>.isNone do - throwImported + throwError s!"invalid doc string, declaration '{declName}' is in an imported module" modifyEnv fun env => versoDocStringExt.insert env declName docs diff --git a/tests/lean/versoDocMissing.lean b/tests/lean/versoDocMissing.lean new file mode 100644 index 0000000000..a22892b450 --- /dev/null +++ b/tests/lean/versoDocMissing.lean @@ -0,0 +1,9 @@ +set_option doc.verso true + +/-! +This test checks that the error produced for a docstring without a corresponding declaration is a parser error instead of an internal error or panic from elaborating partial syntax. +-/ + +/-- +foo +-/ diff --git a/tests/lean/versoDocMissing.lean.expected.out b/tests/lean/versoDocMissing.lean.expected.out new file mode 100644 index 0000000000..050baa15ac --- /dev/null +++ b/tests/lean/versoDocMissing.lean.expected.out @@ -0,0 +1 @@ +versoDocMissing.lean:10:0: error: unexpected end of input; 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_error_explanation', 'register_tactic_tag', 'simproc', 'simproc_decl', 'structure', 'syntax', 'tactic_extension', 'theorem' or 'unif_hint'