Zulip Chat Archive

Stream: general

Topic: wlog tests use sorry


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

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

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

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

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

view this post on Zulip Patrick Massot (Mar 09 2018 at 21:21):

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

view this post on Zulip Patrick Massot (Mar 09 2018 at 21:21):

I manually copied docstrings from the source

view this post on Zulip Patrick Massot (Mar 09 2018 at 21:21):

(and reorganized them a bit)

view this post on Zulip Sebastian Ullrich (Mar 09 2018 at 21:21):

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

view this post on Zulip Sebastian Ullrich (Mar 09 2018 at 21:22):

(not the reorganization part)

view this post on Zulip Patrick Massot (Mar 09 2018 at 21:22):

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

view this post on Zulip Patrick Massot (Mar 09 2018 at 21:22):

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

view this post on Zulip Patrick Massot (Mar 09 2018 at 21:23):

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

view this post on Zulip Sebastian Ullrich (Mar 09 2018 at 21:23):

We definitely want a documentation generator at some point

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

view this post on Zulip Patrick Massot (Mar 09 2018 at 21:24):

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

view this post on Zulip Patrick Massot (Mar 09 2018 at 21:26):

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

view this post on Zulip Patrick Massot (Mar 09 2018 at 21:26):

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

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

view this post on Zulip Sebastian Ullrich (Mar 09 2018 at 21:28):

heh


Last updated: May 14 2021 at 04:22 UTC