Minor bug in tracing locations with docstrings

Stream: lean4

[Thomas Murrills]

This is on 4.0.0-nightly-2023-06-20. Is anyone else able to reproduce it? Here are the steps:

Start with:

set_option trace.compiler.ir true

/- text -/

def x : Unit := ()  -- trace appears here

Change /- to /--:

set_option trace.compiler.ir true

/-- text -/ -- trace appears here

def x : Unit := ()

Change /-- back to /-:

set_option trace.compiler.ir true

/- text -/ -- trace persists here

def x : Unit := ()

I can't imagine this is very important in itself, but I figured I'd bring it up in case the underlying issue inadvertently affects other things. :)

[Mac Malone]

This is because a docstring comment is not really a "comment" in the traditional sense (i.e., an ignored part of the grammar). Instead, a docstring comment is part of a declaration's concrete syntax.

As a trace appears at the start of a declaration, and the docstring is part of the declaration, the trace appears on it. Inversely, a normal block comment is not part of the declaration, so the trace does not appear on it.

[Kyle Miller]

@Mac That's not the issue -- it's that when you change /-- to /- the info stays on the /-

[Mac Malone]

Kyle Miller Oh, oops! :sweat_smile:

[Kyle Miller]

(I wonder though if we could have definition/theorem/etc. commands set def/theorem/etc. to be the ref for where trace messages pop up.)