Get all tactics used in the module

Stream: Is there code for X?

[Asei Inoue]

How to get the list of tactics used in the module?

[Asei Inoue]

what is I want: #tactic_list command which print all tactics used in the module

why I want this: I’m writing a book about Lean, and I want to track tactics explained so far

[Damiano Testa]

I don't have time to look at this in detail, but the unused tactic linter extracts tactics from commands. A very crude copy-paste-modify of the code there, produces this:

import Mathlib

open Lean in
def headString (s : Syntax) : String :=
  (s.getHead?.getD default).getSubstring?.getD "" |>.toString.trim

open Lean Elab Command Mathlib.Linter.UnusedTactic in
elab "tacs " cmd:command : command => do
  elabCommand cmd
  let env ← getEnv
  let cats := (Parser.parserExtension.getState env).categories
  -- These lookups may fail when the linter is run in a fresh, empty environment
  let some tactics := Parser.ParserCategory.kinds <$> cats.find? `tactic
    | return
  let some convs := Parser.ParserCategory.kinds <$> cats.find? `conv
    | return
  let go : M Unit :=
    getTactics ∅ (fun k => tactics.contains k || convs.contains k) cmd
  let (_, map) ← go.run {}
  let allTacs := map.toList
  logInfo <| .joinSep (allTacs.map (fun s => m!"{(headString s.2, s.2)}")) m!"\n\n"

tacs
example (u v : ℝ) : min (Int.fract u) (Int.fract (-u)) ≤ Int.fract (u + v) + Int.fract v := by
  by_contra! h
  rw [ lt_inf_iff, Int.fract_neg ] at h
  · obtain ⟨ _ | _, hz ⟩ := Int.fract_add u v
      <;> simp at hz
      <;> linarith [ Int.fract_nonneg ( u + v ), Int.fract_nonneg u, Int.fract_nonneg v ]
  · linarith [ Int.fract_nonneg ( u + v ), Int.fract_nonneg v ]

[Damiano Testa]

As you can see, it is not perfect and it challenges a little what you may consider a "tactic" to be.

[Damiano Testa]

By defining more precisely exactly what it is that you would like to extract and turning this into a linter, you may get what you want!

[Asei Inoue]

Thanks!