## Stream: general

### Topic: wlog tests use sorry

#### Scott Morrison (Mar 09 2018 at 20:40):

@Simon Hudon, I noticed your tests for the wlog tactic contain sorries, and these cause warning messages when compiling mathlib. Perhaps this is worth fixing, so we can all have clean outputs.

#### Patrick Massot (Mar 09 2018 at 20:51):

And what about taking docstrings and tests and extract a documentation from them, as my conversion mode doc?

#### Simon Hudon (Mar 09 2018 at 21:18):

@Patrick Massot I'm looking at https://github.com/leanprover/mathlib/commit/fa255396ff01ea2c0aaef1a2a1000fb03f217468 and I'm not sure what you're alluding to. Are you saying that this doc is extracted automatically from Lean code?

#### Patrick Massot (Mar 09 2018 at 21:20):

No it's not. That why some more work is required (I could do it if nobody else does it but it will probably introduce errors).

#### Simon Hudon (Mar 09 2018 at 21:20):

@Scott Morrison You're right, it is annoying. I try not to make my goals true so that tactics don't accidentally discharge it before the interesting bit of the proof. I'm going to try something less noisy

#### Patrick Massot (Mar 09 2018 at 21:21):

https://github.com/leanprover/mathlib/blob/master/docs/tactics.md is _not_ autogenerated

#### Patrick Massot (Mar 09 2018 at 21:21):

I manually copied docstrings from the source

#### Patrick Massot (Mar 09 2018 at 21:21):

(and reorganized them a bit)

#### Sebastian Ullrich (Mar 09 2018 at 21:21):

You could write a tactic program to do that :laughing:

#### Sebastian Ullrich (Mar 09 2018 at 21:22):

(not the reorganization part)

#### Patrick Massot (Mar 09 2018 at 21:22):

My hope is that this doc is more visible here than in the source code

#### Patrick Massot (Mar 09 2018 at 21:22):

But maybe it's me refusing to understand that source code is the documentation

#### Patrick Massot (Mar 09 2018 at 21:23):

I think we discussed tactics extracting docstrings back in the gitter days

#### Sebastian Ullrich (Mar 09 2018 at 21:23):

We definitely want a documentation generator at some point

#### Patrick Massot (Mar 09 2018 at 21:24):

I'm sure Simon could do it. Sebastian, have you seen the tactic Simon wrote for https://github.com/PatrickMassot/lean-differential-topology/pull/1/files ?

#### Patrick Massot (Mar 09 2018 at 21:26):

When I have 5 minutes to kill I sometimes randomly look at the monad review discussion.

#### Patrick Massot (Mar 09 2018 at 21:26):

But I resisted when reading https://github.com/leanprover/lean/pull/1881#discussion_r173307598

#### Patrick Massot (Mar 09 2018 at 21:27):

I didn't create a fake Github account only to post a link to the Lean FAQ ::stuck_out_tongue_winking_eye:

#### Sebastian Ullrich (Mar 09 2018 at 21:28):

heh

Last updated: May 14 2021 at 04:22 UTC