List all tactics

Stream: general

[Neil Strickland]

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]

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

[Neil Strickland]

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]

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

[Koundinya Vajjha]

@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]

Thanks, I'll have a look at that.

[Floris van Doorn]

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]

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