bug(tactic): Unexpected horizontal rule (thematic break) in parsed Markdown
Nobody has claimed this yet.
- Dominant language
- Lean
- Stars
- 384
- Forks
- 124
- Avg merge
- 22h 28m
- Merged PRs (30d)
- 10
Description
Verso fails to parse a tactic docstring which contains a horizontal rule. Consider the tactic
/--
This is a Horizontal rule:
***
it does not parse.
-/
syntax (name := MyNamespace.bad_tactic) "bad_tactic " : tactic
then adding a tactic block to the file
:::tactic MyNamespace.bad_tactic show:="bad_tactic"
:::
fails with Unexpected horizontal rule (thematic break) in parsed Markdown.
Would be nice if either support for such HR could be added or if the markdown parser would simply remove them (instead of crashing).
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start with the reproducer in the issue: a tactic docstring containing ***, followed by the :::tactic MyNamespace.bad_tactic block. Trace the Markdown parsing path that reports Unexpected horizontal rule (thematic break) in parsed Markdown. Done means this input no longer crashes, with the supported handling of the horizontal rule defined.
Written by the indexing model from the issue text.
Assessment
- Domain
- documentation
- Issue type
- Bug
- Difficulty
- 3/5
- Estimated time
- 1-2 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 42/100