ToString instance for Xml does not correctly escape
Nobody has claimed this yet.
Assessment
- Difficulty
- 2/5
- Estimated time
- 1-3 hours
- Newbie friendliness
- 75/100
- Issue type
- Bug
- Clarity
- Clearly specified
- Activity status
- Active
- Tech stack
- xml
- Domain
- compilers
Research direction
Start by running the supplied Lean.Xml.parse and toString reproduction, then locate the Lean.Xml stringifier and compare it with the parser's escape handling. Done means toString emits valid XML with quotes and angle brackets escaped as shown in the expected output, without breaking the reported doc-gen use case.
Written by the indexing model from the issue text.
Description
Prerequisites
Please put an X between the brackets as you perform the following steps:
- Check that your issue is not already filed:
https://github.com/leanprover/lean4/issues - Reduce the issue to a minimal, self-contained, reproducible test case.
Avoid dependencies to Mathlib or Batteries. - Test your test case against the latest nightly release, for example on
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
While the XML parser correctly handles XML escape sequences, the stringifier does not emit them.
Context
Zulip thread. This leads to some mangled markdown in doc-gen, which unknowingly tries to work around this bug.
Steps to Reproduce
Run the following:
import Lean
run_cmd do
let .ok doc := Lean.Xml.parse "<b class=\""\">hello < world </b>" | unreachable!
Lean.logInfo (toString doc)
Expected behavior: The output is <b class=""">hello < world </b>
Actual behavior: The output is <b class=""">hello < world </b>, which is invalid XML
Versions
4.9.0-rc1
4.10.0-nightly-2024-06-09
Additional Information
[Additional information, configuration or data that might be necessary to reproduce the issue]
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
- Dominant language
- Lean
- Stars
- 9.2k
- Forks
- 990
- Avg merge
- 1d 15h
- Merged PRs (30d)
- 165
Contributor guide
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.
More from leanprover/lean4
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 84/100
leanprover/lean4#15197 ·
-
Difficulty 2/5 1-3 hours Newbie friendliness 86/100
leanprover/lean4#15172 · 1 comment ·
-
P-medium
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
leanprover/lean4#15037 ·
-
`Nat.lt` docstring OpenP-low
Difficulty 1/5 Under an hour Newbie friendliness 85/100
leanprover/lean4#15014 ·
-
P-medium
Difficulty 2/5 1-3 hours Newbie friendliness 84/100
leanprover/lean4#14973 · 1 comment ·
All issues in leanprover/lean4
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 82/100
objectionary/eo#8869 · 1 comment ·
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
EricSpencer00/Resilient#4824 · 1 comment ·
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
objectionary/jeo-maven-plugin#1758 ·
-
generics
Difficulty 2/5 1-3 hours Newbie friendliness 82/100
-
mlir
Difficulty 2/5 1-3 hours Newbie friendliness 84/100
llvm/llvm-project#224908 · 1 comment ·