Extracting Lean source from REPL/Lean process/OLean

Stream: new members

[Michael Zappa]

I am experimenting with using the https://github.com/leanprover-community/repl project as a means of interactive Lean use outside of an LSP-enabled text editor. This project has the capability to write out a .olean file representing its internal state so it can be re-loaded by a different REPL instance. I would, however, like the ability to write out a Lean source code file representing this state - definitions, theorems, etc. so it can be recorded as source separate from REPL interaction.

I see all of the #print/#where family of transient operations, which are helpful - and lead me to believe Lean can have the capability of re-creating its source code in some form. I also see that in the past there was a low level export format, but it doesn't seem to be around in Lean 4.

Is there anything in this vein I am missing or not aware of?

[Henrik Böving]

There is no way to recover the exact input source code from a .olean file. Commands like #print inspect the elaborate core terms and attempt to recreate a syntax that they might have been derived from. This is entirely best effort.

[James E Hanson]

Is it even possible to recover the exact order in which declarations were added to the environment? I don't understand how Lean.SMap works well enough to make a judgment call about this.

[James E Hanson]

Michael Zappa said:

I also see that in the past there was a low level export format, but it doesn't seem to be around in Lean 4.

The export format still exists but it has transitioned to JSON and is really not meant to be human readable.

[James E Hanson]

The export format would only really let you recover fully elaborated terms. This means that something like Nat.pow, which in source looks like this

@[extern "lean_nat_pow"]
protected def Nat.pow (m : @& Nat) : (@& Nat) → Nat
  | 0      => 1
  | succ n => Nat.mul (Nat.pow m n) m

would be recovered as something like this

def Nat.pow : Nat → Nat → Nat :=
fun (m : Nat) (x._@.Init.Prelude.427477602._hygCtx._hyg.10 : Nat) => Nat.brecOn.{1} (fun
(x._@.Init.Prelude.427477602._hygCtx._hyg.10 : Nat) => Nat)
x._@.Init.Prelude.427477602._hygCtx._hyg.10 (fun
(x._@.Init.Prelude.427477602._hygCtx._hyg.10 : Nat) (f : Nat.below.{1} (fun
(x._@.Init.Prelude.427477602._hygCtx._hyg.10 : Nat) => Nat)
x._@.Init.Prelude.427477602._hygCtx._hyg.10) => Nat.pow.match_1.{1} (fun
(x._@.Init.Prelude.427477602._hygCtx.10.Init.Prelude.427477602._hygCtx._hyg.21 : Nat) =>
(Nat.below.{1} (fun (x._@.Init.Prelude.427477602._hygCtx._hyg.10 : Nat) => Nat)
x._@.Init.Prelude.427477602._hygCtx.10.Init.Prelude.427477602._hygCtx._hyg.21) -> Nat)
x._@.Init.Prelude.427477602._hygCtx._hyg.10 (fun (_ : Unit)
(x._@.Init.Prelude.427477602._hygCtx._hyg.41 : Nat.below.{1} (fun
(x._@.Init.Prelude.427477602._hygCtx._hyg.10 : Nat) => Nat) (OfNat.ofNat.{0} Nat 0
(instOfNatNat 0))) => OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) (fun (n : Nat)
(x._@.Init.Prelude.427477602._hygCtx._hyg.41 : Nat.below.{1} (fun
(x._@.Init.Prelude.427477602._hygCtx._hyg.10 : Nat) => Nat) (Nat.succ n)) => Nat.mul
x._@.Init.Prelude.427477602._hygCtx._hyg.41.1 m) f)

[James E Hanson]

To be fair most of this complexity comes from the way Lean generates fresh variable names, but even without those, it's meaningfully harder to read:

def Nat.pow : Nat → Nat → Nat :=
fun (m : Nat) (x0 : Nat) => Nat.brecOn.{1} (fun (x0 : Nat) => Nat) x0 (fun (x0 : Nat)
(f : Nat.below.{1} (fun (x0 : Nat) => Nat) x0) => Nat.pow.match_1.{1} (fun (x1 : Nat)
=> (Nat.below.{1} (fun (x0 : Nat) => Nat) x1) -> Nat) x0 (fun (_ : Unit)
(x2 : Nat.below.{1} (fun (x0 : Nat) => Nat) (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
=> OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) (fun (n : Nat) (x2 : Nat.below.{1} (fun
(x0 : Nat) => Nat) (Nat.succ n)) => Nat.mul x2.1 m) f)

[Michael Zappa]

Thank you both for the input and examples!

[James E Hanson]

James E Hanson said:

Is it even possible to recover the exact order in which declarations were added to the environment? I don't understand how Lean.SMap works well enough to make a judgment call about this.

One last thing to note is that the export format definitely does not preserve the order in which declarations are added to the environment.