Stream: general

Topic: lean codeblocks in docstrings

Johan Commelin (Feb 03 2020 at 16:04):

I tried to put a codeblock as in

lean
foo



in a docstring. But I got a complaint, so I removed it: https://github.com/leanprover-community/mathlib/pull/1946/commits/48a5d7c99a83709e5736398db58ef39fb4bc0821#diff-e43627ca2566b806fcd077fad0fe29c9L26

If you don't add the lean tag, then everything is fine. So


foo



works fine. I can imagine that the language modifier might be useful. But it isn't crucial. Just posting to see what others think.

Johan Commelin (Feb 03 2020 at 16:05):

FYI: the error that Lean gave was invalid docstring: expected end of code block, or something like that.

Bryan Gin-ge Chen (Feb 03 2020 at 16:14):

Looks like the error message comes from the code around here, so we could update that in 3.5.x to ignore such tags.

Rob Lewis (Feb 03 2020 at 16:15):

It's handled correctly here: https://github.com/leanprover-community/mathlib/blob/master/src/tactic/reassoc_axiom.lean#L15

Yury G. Kudryashov (Feb 03 2020 at 16:19):

What's the difference?

Bryan Gin-ge Chen (Feb 03 2020 at 16:25):

I guess there's a bug somewhere. This gives the invalid docstring error:

/-!

lean
a


a
-/


This doesn't:

/-!

lean
a


-/


Neither does this (though it should):

/-!

lean
a



-/


Bryan Gin-ge Chen (Feb 03 2020 at 18:30):

This is now issue 108 on leanprover-community/lean. I probably won't be able to look at this any more for now.

Bryan Gin-ge Chen (Feb 14 2020 at 03:20):

I looked at this again. The issue that @Johan Commelin pointed out was actually fixed last year in this PR which was merged into 3.5.0.

However, this example:

/-!



-/


does not throw an error, even though it should.

Last updated: May 15 2021 at 23:13 UTC