Zulip Chat Archive
Stream: triage
Topic: issue #3088: Towards a more beginner-friendly tactic doc
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?
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.
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.
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?
Kevin Buzzard (Feb 02 2021 at 15:31):
For example, you want a couple of simple ways of using linarith in the linarith docstring?
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.
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.
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!`)
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).
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?
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"?
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
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?
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
Random Issue Bot (Nov 15 2021 at 14:19):
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?
Random Issue Bot (Jan 02 2022 at 14:17):
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?
Random Issue Bot (Apr 09 2022 at 14:13):
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?
Random Issue Bot (Apr 26 2022 at 14:20):
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?
Random Issue Bot (Aug 11 2022 at 14:13):
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?
Random Issue Bot (Oct 05 2022 at 14:46):
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?
Random Issue Bot (Dec 10 2022 at 14:08):
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?
Random Issue Bot (Jun 20 2023 at 14:06):
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?
Random Issue Bot (Aug 21 2023 at 14:07):
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?
Last updated: Dec 20 2023 at 11:08 UTC