Documentation error when starting with `

[JadAbouHawili]

The following:

/--
`And.intro` takes a proof of `P`, a proof of `Q`, and gives a proof of `P ∧ Q` where `P Q : Prop`.

Given,

hP : P
hQ : Q

we have `And.intro hP hQ : P ∧ Q`
-/
TheoremDoc And.intro as "And.intro" in "And"

renders as

---

but this

/--
The theorem `And.intro` takes a proof of `P`, a proof of `Q`, and gives a proof of `P ∧ Q` where `P Q : Prop`.

Given,
hP : P
hQ : Q
we have `And.intro hP hQ : P ∧ Q`
-/
TheoremDoc And.intro as "And.intro" in "And"

renders as

TheoremDoc doesn't seem to like it when you start with ` as the first character. No idea why that is.

[TentativeConvert]

I was tought that starting a sentence with a non-natural-language word is bad style. But the above difference in rendering is clearly a bug rather than a feature.

In Robo, the following tactic documentation renders corretly:

/-- `specialize h a₁ a₂` ist äquivalent zu `have h := h a₁ a₂`: die Taktik ersetzt eine Annahme
`h : ∀ m₁ m₂, P m₁ m₂` durch den Spezialfall `h : P a₁ a₂`.
…
```
-/
TacticDoc specialize

(see https://github.com/hhu-adam/Robo/blob/f63d073670b795c1d2915393043b8f3db7512d7d/Game/Doc/Tactic.lean#L491C1-L508C21)

[cionx]

This problem also occurs in the game “A Lean Intro to Logic” in at least two places, both in the world “→ Tutorial: Party Snacks”:

• The conclusion to level 1 has the following code:

  Conclusion "
  Congratulations. You have evidence that your party will have cake!
  
  ----
  1:
  ```
  have c := bakery_service p
  exact c
  ```
  2:
  ```
  exact bakery_service p
  ```
  3:
  ```
  exact modus_ponens bakery_service p
  ```
  "
  

  But after finishing the level the following text appears instead:

  

• The conclusion to level 6 has the following code :

  Conclusion "
  Cool. Chips and Dip!
  
  ----
  # A Tip!
  If you're writing a function with more than one parameter, you can just list the parameters. That's a shorthand for nested function declarations.
  ```
  λ(p : P) ↦ λ(q : Q) ↦ h (and_intro p q)
  -- can be written as:
  λ(p : P)(q : Q) ↦ h (and_intro p q)
  -- Or because the propositions of p and
  -- q are clear from the goal:
  λp q ↦ h (and_intro p q)
  ```
  "
  

  But after finishing the level the following text appears instead:

  

Note that in these two examples not only is there text missing but all colons in the remaining text have also been replaced by periods.

---

So far my best explicit description of the problem is that

• if a period appears as the the first [^A-Za-z0-9 `]-character, but not as the very first character; and
• if sometimes later a colon : appears in the string;
• then all text up to and including the first colon will me missing, and all further colons will be replaced by periods.

Using these rules, the problem can already be provoked in the GameSkeleton: if we replace the line

Introduction "This text is shown as first message when the level is played.

by the modified line

Introduction "This. text is shown as first message when the level is played:

then the text This. text is shown as first message when the level is played: is completely missing from the built game.

From what I can tell, this problem was first mentioned in https://github.com/Trequetrum/lean4game-logic/issues/8 around a year ago.