Zulip Chat Archive

Stream: triage

Topic: issue #3088: Towards a more beginner-friendly tactic doc


view this post on Zulip Random Issue Bot (Feb 02 2021 at 14:24):

Today I chose issue 3088 for discussion!

Towards a more beginner-friendly tactic doc
Created by @Utensil Song (@utensil) on 2020-06-16
Labels: help wanted

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Rob Lewis (Feb 02 2021 at 15:14):

I'd still like to see this happen, but this is probably not the time. If/when we have a doc tool running in mathlib4 we should work on structuring the tactic entries.

view this post on Zulip Rob Lewis (Feb 02 2021 at 15:14):

That said, a lot of doc entries are missing e.g. example uses which I'd be very happy to merge at any time.

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 15:28):

This is the sort of thing I find myself time and time again for students -- an explanation of the ten or so basic tactics which you need in order to get going. But I suspect you're talking about something else here. Is the idea that you want some super-long docstrings with lots of examples etc within lean/mathlib itself?

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 15:31):

For example, you want a couple of simple ways of using linarith in the linarith docstring?

view this post on Zulip Rob Lewis (Feb 02 2021 at 15:32):

Exactly. For instance, I'd like tactic#apply to be a combination of what's there now and what's on your page.

view this post on Zulip Rob Lewis (Feb 02 2021 at 15:33):

Too many of the tactic docs just explain what the tactic does, without any kind of examples.

view this post on Zulip Rob Lewis (Feb 02 2021 at 15:34):

Ideally there's one example for every "feature" of the tactic. (linarith, linarith [t1, t2], linarith only, linarith!`)

view this post on Zulip Rob Lewis (Feb 02 2021 at 15:36):

Ideally the doc entries are structured so that we can identify which part is the short explanation and which part is the examples. And ideally the doc entry enforces this kind of separation (and makes sure you include each component when you write a new entry).

view this post on Zulip Random Issue Bot (Mar 23 2021 at 14:27):

Today I chose issue 3088 for discussion!

Towards a more beginner-friendly tactic doc
Created by @Utensil (@utensil) on 2020-06-16
Labels: help wanted

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Kevin Buzzard (Mar 23 2021 at 14:41):

What do we want here? A page like the simp leanprover-community page which goes over the ten or so "standard tactics"?

view this post on Zulip Julian Berman (Mar 23 2021 at 15:01):

As a newbie who read that page almost in full at one point or another, definitely more examples would help, but also a bit less alphabetical sorting would help so that page you linked Kevin looks much more easy to follow because it's in order of usage-ish. I also remember in particular being confused by the description of existsi on that page when I first started

view this post on Zulip Julian Berman (Mar 23 2021 at 15:03):

existsi e will instantiate an existential quantifier in the target with e and leave the instantiated body as the new target. More generally, it applies to any inductive type with one constructor and at least two arguments, applying the constructor with e as the first argument and leaving the remaining arguments as goals.

as a newbie I had no idea what an inductive type was, what it practically meant to apply a constructor and be left with a goal, and what

Note: in mathlib, the use tactic is an equivalent tactic which sometimes is smarter with unification.

was trying to say -- i.e. if it's worse than use, why does it exist?

view this post on Zulip Julian Berman (Mar 23 2021 at 15:05):

I also found it quite hard to answer a question like "I have a statement I want to split into cases, which tactics should I look at" -- but that may just be the "make tags clickable" part of that ticket


Last updated: May 09 2021 at 16:20 UTC