proof mode: split out tactics into separate commands

Stream: general

[Mario Carneiro]

Mario Carneiro said:

But if lean had a proof mode like HOL light's e(...) steps broken out as separate lean commands then you would certainly get back the speed benefits you are seeing in HOL Light

Mario Carneiro said:

now I think I want to try to demo something like that in lean

Here's what I was talking about @D. J. Bernstein : This is a prototype implementation of a "proof mode" in which you can save the context of a proof in a by block by writing start_proof, and then you can start writing tactics in separate commands thereafter using ## before each tactic (or group of tactics). Because lean automatically snapshots between commands, you get the benefits of a line-by-line proof like in Coq or HOL light in terms of general responsiveness. This may be considered as an alternative to the save tactic, which tries to do something similar but without linearizing the AST structure.

[Mario Carneiro]

Mathlib.Tactic.ProofMode:

import Lean
open Lean

structure ProofState where
  tacCtx : Elab.Tactic.Context
  tacState : Elab.Tactic.State
  termCtx : Elab.Term.Context
  termState : Elab.Term.State
  metaCtx : Meta.Context
  metaState : Meta.State

def ProofState.get : Elab.Tactic.TacticM ProofState :=
  fun tacCtx tacState termCtx termState metaCtx metaState => do
    let tacState ← tacState.get
    let termState ← termState.get
    let metaState ← metaState.get
    return { tacCtx, tacState, termCtx, termState, metaCtx, metaState }

def ProofState.with : ProofState → Elab.Tactic.TacticM α → CoreM α :=
  fun { tacCtx, tacState, termCtx, termState, metaCtx, metaState } x => do
    let tacState ← IO.mkRef tacState
    let termState ← IO.mkRef termState
    let metaState ← IO.mkRef metaState
    x tacCtx tacState termCtx termState metaCtx metaState

initialize proofStateExt : EnvExtension (List ProofState) ← registerEnvExtension (pure [])

elab "start_proof" : tactic => do
  let state ← ProofState.get
  modifyEnv (proofStateExt.modifyState · (state :: ·))
  Elab.Tactic.evalTactic (← `(tactic| repeat sorry))

elab tk:"##" tac:(tacticSeq)? : command => do
  let state :: rest := proofStateExt.getState (← getEnv)
    | throwError "proof mode not started, use `start_proof`"
  Elab.Command.liftTermElabM do
    state.with do
      Elab.Tactic.withTacticInfoContext tk do
        if let some tac := tac then
          Elab.Tactic.evalTactic tac
      if (← Elab.Tactic.getUnsolvedGoals).isEmpty then
        logInfoAt tk "Goals accomplished 🎉"
        modifyEnv (proofStateExt.setState · rest)
      else
        modifyEnv (proofStateExt.setState · ((← ProofState.get) :: rest))

[Mario Carneiro]

test file:

import Mathlib.Tactic.ProofMode

theorem T : ∃ x, x < x + 1 := by
  constructor
  start_proof -- this pushes the current proof state (note, it doesn't work in `example`)

## -- cursor here to see proof state
## refine Nat.lt_succ_self ?_ -- you can write a tactic or tactic block here
## exact 1 -- when the goal is finished, it pops the proof state and reports "Goals accomplished 🎉"

[Mario Carneiro]

It would be nice to get some experience reports with this from people who like to write long tactic proofs and struggle to keep things responsive

[D. J. Bernstein]

Will try with my next Lean project, thanks!

[Bolton Bailey]

Mario Carneiro said:

It would be nice to get some experience reports with this from people who like to write long tactic proofs and struggle to keep things responsive

I just tried it on my long-running crypto proof (~35 tactic calls, most of the long ones are simp only calls on a bunch of hypotheses, runs in about 200 seconds on my laptop)

• Tactic processing restarts from the point of my last edit, not the beginning :+1:
• I can see about how long each tactic call is taking without any other kind of profiling, frankly this alone makes it a useful tool.
• Works on the tactics defined in my project as well as standard mathlib tactics

I am not being able to see the actual proof state, it perpetually says "loading messages". (This was already a problem for this codebase - it was taking a long time to update the info view as I moved my cursor around, but now it just doesn't show things at all). Still, tactics like polyrith I can see the output by mousing over, so it's clear the tactics are being run.

[Mario Carneiro]

@Bolton Bailey Can you make a MWE for the loading issue? Or a project I can pull

[Bolton Bailey]

After VSCode froze and I rebooted it, I'm not actually getting the perpetual loading problem anymore.

[Bolton Bailey]

It's still slow to change the infoview when moving the cursor, but that was the case before I added start_proof. I haven't put up the code yet, I was planning to just replace my lean3 repository with my lean 4 code when it's ported.

[Bolton Bailey]

Ok the code is now here the file I am working on is FormalSnarksProject.SNARKs.Groth16TypeIII

[Eric Rodriguez]

I just found this by coincidence - this seems amazing! Mario, have you further worked on this?

[Patrick Massot]

@Sebastian Ullrich is preparing the ultimate solution to this issue. See his talk at the Lean Together conference a couple of weeks ago.

[Mario Carneiro]

I think it might be good to have it in mathlib anyway, this has been on the roadmap for ages

[Mario Carneiro]

and to answer your question @Eric Rodriguez , no I haven't done anything else with this but it's usable as is. It's mainly intended for temporary use while working on long meandering proofs that have not yet been put in mathlib style