Zulip Chat Archive

Stream: general

Topic: lean codeblocks in docstrings


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Feb 03 2020 at 16:19):

What's the difference?

view this post on Zulip 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
```

```
-/

view this post on Zulip 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.

view this post on Zulip 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