Why do docstrings include trailing whitespace?

Stream: lean4

[Thomas Murrills]

Just curious: seeing as the style for docstrings is generally /-- example -/ (or even

/--
example
-/

), with whitespace preceding -/, why do we only call removeLeadingWhitespace in docs#Lean.addDocString and leave trailing whitespace?

To see that trailing whitespace is not handled somewhere else in the code (before rendering, that is), note the space after test:

import Lean

/-- test -/
theorem foo : True := trivial

open Lean in
/-- info: some (test ) -/
#guard_msgs in
run_cmd logInfo m!"{(← findDocString? (← getEnv) `foo)}"

(This isn't crucial; I was just handling different ways of providing docstrings in #28133 and was surprised to note the difference.)

[Robin Arnez]

Oh you know what's even funnier? docComments don't even have leading whitespace; that gets trimmed while parsing:

/--
-- heh this is whitespace
/- This is also whitespace -/
It begins here.
-- heh this is not whitespace
/- This also isn't whitespace -/
-/
def hi := 3

[Robin Arnez]

Zulip completely messes this up, as expected :-)

[Julian Berman]

Not strictly related, but

def foo := 37

/--
/-
/-
-/
theorem stest : True := ⟨⟩

producing

▼ 3:1-3:4: warning:
unused `termination_by?`, function is not recursive

is also a bit strange (though a proper "unterminated comment" does appear at the bottom line as well)

[Robin Arnez]

Did you know that this has nothing to do with docstrings?

/-- warning: unused `termination_by?`, function is not recursive -/
#guard_msgs in
def a := 1
arbitrarily_chosen_token /-

[Robin Arnez]

The problem is that a token followed by an unterminated comment causes the token to be pushed to the syntax stack but produce an error so satisfySymbolFn doesn't check whether it is actually correct.

[Robin Arnez]

Oh and you won't believe what the output of this is (on latest mathlib):

/-- -/ /-

Error message

elaboration function for 'Lean.Parser.«command_Builtin_grind_propagator____:=_»' has not been implemented

[Thomas Murrills]

Robin Arnez said:

Oh you know what's even funnier? docComments don't even have leading whitespace; that gets trimmed while parsing:

Huh! I was curious, and traced the blame—apparently removing leading spaces was necessary in 2022. Maybe parsing has changed since then?