List of all conv tactics

Stream: new members

[Jakub Nowak]

When I hit autocompletion button inside tactic mode I get list of all tactics:
image.png

But this doesn't work for conv mode:
image.png

I haven't checked in VSCode, because I don't know how to open autocompletion popup there, but I would be surprised if it were working differently in VSCode.

Could this be fixed? Also, is there maybe a list of all conv tactics somewhere in lean4 reference, or mathlib? Like https://leanprover-community.github.io/mathlib-manual/html-multi/Tactics/All-tactics/

[Mirek Olšák]

Not very convenient but #help conv

[Aaron Liu]

import Batteries.Tactic.HelpCmd

#help conv

[Jakub Nowak]

Hm, looks like doc-string for dsimp? got mixed up with doc-string of simp?

syntax "dsimp?"... [Lean.Parser.Tactic.Conv.dsimpTrace]
  `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
  that would be sufficient to close the goal. See the `simp?` tactic for more information.

[Mirek Olšák]

Also, I once wrote a meta-snippet to display all syntaxes (in live lean) with the possibility to hover over them. Looks like many standard tactics work too.

[Lua Viana Reis]

Trying to reproduce @Jakub Nowak OP made me realize the module system is breaking the tactic completions. Is this a known issue?

module

example := by
  sor -- place the cursor here, all completions are fully qualified names

[Jakub Nowak]

Hm, it looks it's broken withmodule because all names are fully qualified:
image.png

But that fully qualified name completion is bonkers. Completing sor gives this, which doesn't work:

module

example := by
  Lean.Parser.Tactic.tacticSorry

[Lua Viana Reis]

it's completing with the parser constant names, which have term-mode values but are not tactics

[Lua Viana Reis]

compare

module

import Lean.Elab.Tactic.Doc

open Lean.Elab.Tactic.Doc

#eval do
  let docs ← allTacticDocs
  return docs.map TacticDoc.userName

and

import Lean.Elab.Tactic.Doc

open Lean.Elab.Tactic.Doc

#eval do
  let docs ← allTacticDocs
  return docs.map TacticDoc.userName

[Marc Huisinga]

Regarding the feature request in the OP: could you open an RFC in core?

(I can already say that from an implementation perspective, this is likely pretty tricky. Completion in whitespace is pretty subtle, especially if you want it to make use of incrementality, and making it context-dependent on whether you're currently in a conv block or not is even more subtle.)

[David Thrane Christiansen]

Jakub Nowak said:

is there maybe a list of all conv tactics somewhere in lean4 reference

The reference manual section on conv contains a list of the tactics.

@Lua Viana Reis #12047 fixes the first-token detection (using a strategy suggested by @Sebastian Ullrich - thanks!). This seems to fix the completion issue as well. Thank you for reporting it!

image.png