expanding and serializing expressions

Stream: general

[Jason Rute]

I've been thinking again about serializing goals and expressions in Lean so that they can be deserialized into another Lean process. It seems that I should just be able to read off the internal representation of the expression, but there are three main complexities:

• metavariables
• macros
• the elab flag

[Jason Rute]

As for metavariables, they can be serialized, (and maybe I also need to separately serialize their type?). As for deserialization, this might be naive, but I think metavariables can be handled by making fresh metavariables when deserializing and replacing the old metavariables with those. Any issues with this approach?

[Jason Rute]

As for macros, my understanding is that a macro is just a form of lazy evaluation which promises to expand in the expression later. I notice if I pretty print the expressions that the macros seem to be evaluated. Is there a way in lean to evaluate a macro expression into one without any macros? (I need to do a bit more digging also and see how common it is to get macros in goals. Maybe it is a rarity.)

[Jason Rute]

Last, for the elab flag, what is the elab flag set to for goal statements? Is it always tt, always ff, or mixed? Also, am I correct that that given an expression e there is no way to know which flag was used to create it? Or is the idea that if I see a type expr, it is really expr tt since tt is the default?

[Jason Rute]

Note, it looks like this is going to be easier in Lean 4 since there are no macros or elab flag and it seems that expressions are pure data types. (Also the hashing will make serialization possibly faster since one doesn't have to traverse the whole tree.)

[Gabriel Ebner]

elab = ff means pre-expression, i.e., an AST representation of the input. You should probably only look at elaborated expressions: elab = tt. Lean 4's Expr type is essentially the elab = tt variant.

[Gabriel Ebner]

Just expand macros before serialization using docs#environment.unfold_all_macros

[Gabriel Ebner]

You might want to look at docs#io.serialize for more efficient serialization of expressions.

[Gabriel Ebner]

Jason Rute said:

Or is the idea that if I see a type expr, it is really expr tt since tt is the default?

Exactly.

[Jason Rute]

I forgot about the io.serialize. I'll give it a try.

[Scott Morrison]

Have a look at branch#mathlib-cache (PR #2300), a prototype tactic written by my former student Keeley Hoek, which caches the results of begin ... end blocks to the filesystem, for faster recompilation.

[Jason Rute]

@Gabriel Ebner unfold_all_macros doesn't seem to work always. Here is a MWE based on my use case (I thought revert_all would be a convenient way to turn the goal with its local context into a single expression, which could then be serialized.)

meta def unfold_macros_in_goal : tactic expr := do
  env <- tactic.get_env,
  goal <- tactic.target,
  let goal := env.unfold_all_macros goal,
  tactic.trace goal.to_raw_fmt,
  return goal

theorem trivial_thm (m n : nat) (h1 : m = m) : n = n := by refl

example (m : nat) : m = m := begin
    apply trivial_thm, -- puts delayed_abstraction macros in the goal (which I think build metavariables)
    tactic.revert_all,    -- goal is ∀ (m : ℕ), ?m_1[m] = ?m_1[m]
    unfold_macros_in_goal,  -- "failed to expand macro" error
end

Moreover, if I try to serialize this goal I get the "'unreachable' code was reached" error. Is this a bug, or is it just not possible to unfold/serialize some expressions?

[Jason Rute]

@Scott Morrison I'll try to have a look. By chance, is it easy to explain what it means to cache the result of a begin...end block? Does it just cache the term proof? Does it work for partial proofs, or just complete proofs?

[Scott Morrison]

Just complete proofs, sorry. :-)

[Scott Morrison]

It just caches the entire proof term by serializing it. Subsequent executions of the tactic block first look for a cached file, and happily proceed to use the cached term if it typechecks.