## Stream: general

### Topic: List all tactics

#### Neil Strickland (Feb 21 2019 at 15:54):

Here is a baby attempt to list all known tactics:

import tactic.interactive

meta def trace_decl_name (d : declaration) (x :tactic unit) : (tactic unit) :=
do (if (name.is_prefix_of tactic.interactive d.to_name) ∧ (d.type = (tactic unit))
then (tactic.trace d.to_name) else x),x

meta def foo : tactic unit :=
do env ← tactic.get_env,
env.fold (return unit.star) trace_decl_name

#eval foo


1. For me, this reliably causes Lean to crash.
2. Before crashing, it does roughly the right thing, listing the names of many tactics. However, it only prints things that have type tactic unit, whereas it should probably print things with types like A → B → ... → X → (tactic Z) or more general pi-types that eventually produce tactics. Is there a standard predicate on expr to detect this?
3. Can I access the docstrings for tactics in this framework?
4. Is there anything else obviously wrong with this approach?

#### Reid Barton (Feb 21 2019 at 16:24):

When you say "crashes", do you mean with a stack overflow, or another kind of crash?

#### Neil Strickland (Feb 21 2019 at 16:45):

I mean that VS Code tells me "Lean: Server has stopped with error code 3221225725". With an earlier version of foo, there was evidence that Lean had got stuck in an infinite loop, processing one element of the environment repeatedly; so that may have led to a stack overflow, but I did not see any explicit message to that effect.

#### Bryan Gin-ge Chen (Feb 21 2019 at 16:57):

Apparently 3221225725 = 0xc00000fd which is indeed the code for a stack overflow.

#### Koundinya Vajjha (Feb 21 2019 at 19:59):

@Neil Strickland I've been working on something similar for the past few weeks. Maybe this can be of some help:
https://github.com/formalabstracts/formalabstracts/tree/master/src/tactic

For (4), you can use doc_string to retreive the docstring of an arbitrary declaration.

#### Neil Strickland (Feb 21 2019 at 21:03):

Thanks, I'll have a look at that.

#### Floris van Doorn (Feb 22 2019 at 19:34):

For (2), you probably want something like

namespace expr
meta def codomain {elab : bool} : expr elab → expr elab
| (pi n bi a b) := codomain b
| a             := a
end expr


and then check whether d.type.codomain.get_app_fn is equal to (tactic)

#### Floris van Doorn (Feb 22 2019 at 19:51):

To address (1), this works for me:

meta def trace_decl_name (d : declaration) (l : list name) : list name :=
if name.is_prefix_of tactic.interactive d.to_name ∧ d.type.codomain.get_app_fn.const_name = tactic
then l.cons d.to_name else l

meta def foo : tactic unit :=
do env ← tactic.get_env,
tactic.trace \$ env.fold [] trace_decl_name

run_cmd foo
`

Last updated: May 11 2021 at 13:22 UTC