comments

Stream: mathlib4

[Johan Commelin]

I've heard the rumour that in the past mathport didn't port line comments. Is that (still) true? I think there are a lot of important comments in mathlib.

[Mario Carneiro]

yes, that's still true. The most important comment that we don't preserve is the head comment, it would be nice to backport something more structured / machine readable for that

[Mario Carneiro]

Comments are not preserved at all in the AST, so we lose track of them quickly. It is hard to see how to mix them in too, since the source-to-source translation can be complex and it's not obvious where to put a comment which can appear literally anywhere in the proof

[Johan Commelin]

Hmm, I know that @Sebastien Gouezel wrote a bunch of complicated proofs that were very well-documented.

[Johan Commelin]

Naive question: I thought mathport was trying to port tactic proofs directly. Why can't you record the position of the line comment in the (linear) stream of tactic lines that forms the proof?

[Sebastien Gouezel]

Indeed, I would be a little bit sad if the comments in the proof of docs#Gromov_Hausdorff.GH_space.topological_space.second_countable_topology, say, were lost in translation.

[Mac]

@Johan Commelin As @Mario Carneiro said, the problem is that comments are not preserved in the AST mathport is porting. That is, by the time mathport gets to inspect the syntax of a proof, the comments are already gone.

However, I wonder if it might be possible to augment the tactic syntax in Lean 3 to support a docstring per tactic. That way such comments could be converted into docstrings and they could be preserved in the AST and ported by mathport. @Mario Carneiro, does that sound feasible?

[Johan Commelin]

mathport has tweaked lean 3 before. Can't the comments be added to the AST?

[Mario Carneiro]

I would much prefer it if this could be done by actually making them doc comments, i.e. using /--

[Mario Carneiro]

or maybe some other sigil

[Johan Commelin]

have : bla,
{ some subproof },
comment "Hello, world",
yet_another_tactic,

[Mario Carneiro]

If we are going to add comments to the AST, it seems like the most logical way to get them is to just use the row/col of existing AST nodes together with the original file text to find whitespace areas, and then grab anything in there that isn't literally a space

[Johan Commelin]

With

meta def tactic.interactive.comment (s : string) := tactic.skip

[Mario Carneiro]

That would certainly work, although it leaves much to be desired on the lean 3 side

[Sebastian Ullrich]

Mario Carneiro said:

If we are going to add comments to the AST, it seems like the most logical way to get them is to just use the row/col of existing AST nodes together with the original file text to find whitespace areas, and then grab anything in there that isn't literally a space

That's not too different from what the Lean 4 parser does, and it's also a reasonable strategy in reverse for adding back comments after the fact. It's always better to place comments at roughly the same position as before, perhaps concatenating them with others that are already there, than to lose them.

[Eric Wieser]

@Johan Commelin, you could presumably even use comment /-" Hello world "-/ with that trick

[Johan Commelin]

Wouldn't that be a regular comment, and hence filtered out?

[Gabriel Ebner]

That's a string literal.

[Mac]

Mario Carneiro said:

I would much prefer it if this could be done by actually making them doc comments, i.e. using /--

@Mario Carneiro Note my suggestion was to make them doc comments.