Read a goal without an infoview¶

The infoview is the normal way to watch a goal change under a tactic, and setting up Neovim or VS Code is worth the ten minutes it takes. It is not the only way, though. Everything the infoview knows comes from the compiler, and the compiler will also say it on standard output.

This page is for three situations. The first is a machine on which no plugin can be installed. The second is pasting a goal state into an issue, a paper or a set of notes, where copying out of a floating pane is awkward. The third is doubting a goal displayed in the editor, and wanting the compiler to state it independently.

The trace_state tactic¶

The trace_state tactic does nothing to the proof. It prints the goal exactly as it stands at that point, as an ordinary informational message, and hands the unchanged goal to whatever comes next. It can therefore be dropped between any two tactics.

example : StrictlyDominates payoff defect cooperate := by
  trace_state
  intro opponent
  trace_state
  cases opponent <;> norm_num [payoff]

Building the file prints both states:

lake build

info: GameTheory/Tracing.lean:8:2: ⊢ StrictlyDominates payoff defect cooperate
info: GameTheory/Tracing.lean:10:2: opponent : Action
⊢ payoff cooperate opponent < payoff defect opponent

The 8:2 and 10:2 are the line and column of each trace_state, which is how to tell the messages apart once a proof has several. The text after them is character for character what the infoview would show at the same position.

Two habits make this pleasant. Keep one scratch file, imported from the root module, so that a rebuild touches only it. Run lake build in a second terminal after every edit, since a small file rebuilds in a few seconds.

Goals in error messages¶

An unfinished proof reports its goals as part of the error, so deleting a tactic is itself a way of asking what the goal was. Removing the final line above gives:

error: GameTheory/Tracing.lean:7:55: unsolved goals
case cooperate
⊢ payoff cooperate cooperate < payoff defect cooperate

case defect
⊢ payoff cooperate defect < payoff defect defect

Here the position 7:55 is the by that opens the tactic block, not the missing tactic, because the whole block is what failed to close the goal. Note also that both remaining goals are listed, with their case labels, which is often more informative than stepping through them one at a time.

What already reaches the build output¶

Nothing special is needed for the commands that ask Lean a direct question. #check, #eval and #print write to the same place, so a file full of them can be read entirely from a terminal:

info: GameTheory/Hello.lean:6:0: temptation : ℝ
info: GameTheory/Hello.lean:8:0: ℝ : Type

Limitations¶

This is a workable substitute and not an equal one. Every look costs a rebuild, so the tight loop of moving a cursor and reading a goal becomes a loop of editing, saving and waiting. Hover documentation, jump to definition, and the exact? style searches all still work, but only through an editor with a language server. Relying on this page often is a sign that the plugin is worth installing after all.