Skip to content

Commit 0cdeadd

Browse files
committed
fix(proof): E2E comments are not Python either (#952)
CI review follow-up. The E2E template's {title}/{description} sit in '//' comments, but they were still getting _inline's backslash-doubling — which a JS comment shows verbatim. My own docstring said 'per context, applied once', and that was the one context still getting the wrong escaper. _MARKDOWN_GATES becomes _NON_PYTHON_GATES and includes E2E. Only the Python templates need doubling; {title_js} stays on _js_string, being the one field that really is a string literal.
1 parent cd9f1ca commit 0cdeadd

2 files changed

Lines changed: 19 additions & 6 deletions

File tree

codeframe/core/proof/stubs.py

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -177,9 +177,12 @@ def _slugify(text: str) -> str:
177177
return slugify(text)
178178

179179

180-
#: Gates whose template is markdown, where none of the Python/JS escaping
181-
#: applies — the text is rendered as prose.
182-
_MARKDOWN_GATES = frozenset({Gate.DEMO, Gate.MANUAL})
180+
#: Gates whose template is not Python, so ``{title}``/``{description}`` need
181+
#: only line-collapsing: DEMO/MANUAL render the text as markdown prose, and
182+
#: E2E puts it in ``//`` comments. Backslash-doubling would show up verbatim in
183+
#: all three. (E2E's ``{title_js}`` is separate — that one is a real string
184+
#: literal and gets ``_js_string``.)
185+
_NON_PYTHON_GATES = frozenset({Gate.DEMO, Gate.MANUAL, Gate.E2E})
183186

184187

185188
def _collapse(text: str) -> str:
@@ -253,10 +256,10 @@ def generate_stubs(req: Requirement) -> dict[Gate, str]:
253256
gate = obligation.gate
254257
template = _TEMPLATES.get(gate, _TEMPLATES[Gate.UNIT])
255258
# Escaping is chosen by the template's language and applied exactly
256-
# once. Markdown renders the text as prose, so it wants neither the
257-
# Python backslash-doubling nor JSON escaping; ``title_js`` always
259+
# once. Only the Python templates need backslash-doubling; markdown
260+
# prose and JS comments would show it verbatim. ``title_js`` always
258261
# starts from the raw title for the same reason.
259-
escape = _collapse if gate in _MARKDOWN_GATES else _inline
262+
escape = _collapse if gate in _NON_PYTHON_GATES else _inline
260263
content = template.format(
261264
req_id=req.id,
262265
title=escape(req.title),

tests/core/test_proof9_evidence_integrity_952.py

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -661,3 +661,13 @@ def test_markdown_stubs_show_the_original_text(self, gate):
661661
assert self.RAW_TITLE in content
662662
if gate is Gate.MANUAL:
663663
assert self.RAW_DESC in content
664+
665+
def test_the_e2e_comments_show_the_original_text(self):
666+
"""E2E's title/description live in `//` comments, not Python
667+
docstrings, so they want no backslash-doubling either — only the
668+
`title_js` string literal needs JSON escaping."""
669+
content = self._stubs([Gate.E2E])[Gate.E2E]
670+
comments = [ln for ln in content.splitlines() if ln.lstrip().startswith("//")]
671+
672+
assert any(self.RAW_TITLE in ln for ln in comments), comments
673+
assert any(self.RAW_DESC in ln for ln in comments), comments

0 commit comments

Comments
 (0)