Skip to content

Fix guard msgs docstring - #978

Open
mo271 wants to merge 2 commits into
leanprover:mainfrom
mo271:fix-guard-msgs-docstring
Open

Fix guard msgs docstring#978
mo271 wants to merge 2 commits into
leanprover:mainfrom
mo271:fix-guard-msgs-docstring

Conversation

@mo271

@mo271 mo271 commented Sep 7, 2026

Copy link
Copy Markdown

No description provided.

The doc comment in `#guard_msgs in` holds the messages that the wrapped
command is expected to produce. It was attributed to the declaration in
that command, which then had two docstring items, and `verso-html`
failed with "Duplicate document ID". Only the wrapped command is now
searched for docstrings.
Adds `LitConfig.GuardMsgs` to the literate-config test project, with a
theorem that has a docstring and is wrapped in `#guard_msgs in`, and a
literate HTML test checking that the theorem's docstring is rendered
exactly once and that the expected-messages comment is kept as prose.

Without the preceding fix, the comment was attributed to the theorem as
a second docstring: the page showed the docstring twice, the expected
messages were gone, and `verso-literate-html` failed with
"Duplicate document ID".
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant