Zulip Chat Archive

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:24):

I think you should carefully read what that guy writes in the monad thread :wink:

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: Dec 20 2023 at 11:08 UTC