Zulip Chat Archive

Stream: general

Topic: List all tactics


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

view this post on Zulip Reid Barton (Feb 21 2019 at 16:24):

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

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

view this post on Zulip Bryan Gin-ge Chen (Feb 21 2019 at 16:57):

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

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

view this post on Zulip Neil Strickland (Feb 21 2019 at 21:03):

Thanks, I'll have a look at that.

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

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