feat(serial): Pickle environment delta's #221

aniva · 2025-06-26T11:50:36-07:00

aniva commented

2025-06-26 11:50:36 -07:00

This makes the environments smaller, and also add an option to trust the pickle so we don't need to replay constants.

feat(env): Environment merging function
feat(repl): Goal state merging function
fix(goal): Combine environments in replay
~~fix(goal): Rename aux lemmas during merger~~

This makes the environments smaller, and also add an option to trust the pickle so we don't need to replay constants. - feat(env): Environment merging function - feat(repl): Goal state merging function - fix(goal): Combine environments in replay - ~~fix(goal): Rename aux lemmas during merger~~

aniva added this to the 0.3.3 milestone 2025-06-26 11:50:36 -07:00

aniva added the

labels 2025-06-26 11:50:36 -07:00

aniva self-assigned this 2025-06-26 11:50:36 -07:00

aniva changed title from ~~feat: Pickle environment delta's~~ to feat(serial): Pickle environment delta's

2025-06-26 11:50:42 -07:00

aniva added a new dependency 2025-06-26 11:50:52 -07:00

#137 🖇️ Environment Delta Pickling

aniva modified the milestone from 0.3.3 to 0.4.0

2025-06-26 11:55:59 -07:00

aniva added 1 commit 2025-06-26 15:52:01 -07:00

52f71f035e

feat(serial): Background environment in pickling

aniva added 1 commit 2025-06-26 15:52:50 -07:00

4df8fcda97

Merge branch 'dev' into serial/delta

aniva commented

2025-06-26 15:58:04 -07:00

We can store a pristine version of the environment in the main monad, and calculate deltas w.r.t. this environment.

aniva added a new dependency 2025-06-26 15:58:55 -07:00

#132 Branch unification

aniva added 1 commit 2025-06-26 16:23:34 -07:00

f914e161e8

fix(goal): Reset messages in replay

aniva added 1 commit 2025-06-26 16:42:12 -07:00

349cff6f05

test(goal): Collision of aux lemma names

aniva commented

2025-06-26 21:13:33 -07:00

There is one test case failing corresponding to adding auxiliary lemmata on both branches.

aniva commented

2025-06-27 15:49:16 -07:00

Without the DeclNameGenerator mechanism to be introduced in 4.21.0, we are looking at something like

def merge (dst src src' : Environment) : Environment × Std.HashMap Name Name :=
  let dstLemmas := Meta.auxLemmasExt.getState dst
  let srcLemmas := Meta.auxLemmasExt.getState src
  let srcLemmas' := Meta.auxLemmasExt.getState src'

  let didx := srcLemmas'.idx - srcLemmas.idx
  let nameInfix := .str .anonymous s!"_merge_{dstLemmas.idx}"

  -- Construct the map by finding name collisions
  let map := srcLemmas'.lemmas.foldl (init := Std.HashMap.emptyWithCapacity didx) λ acc _ (name, _) =>
    if src.contains name then
      acc
    else
      let name' := name.modifyBase (· ++ nameInfix)
      acc.insert name name'

  -- Rename the colliding lemmas in `src'`, including occurrences within constants

  let dst := Meta.auxLemmasExt.modifyState dst fun { idx, lemmas } =>
    ⟨idx + 1, lemmas.insert type (auxName, levelParams)⟩

  (dst.replayConsts src src', map)

but Lean's environment is really not conducive to renaming. I think we should wait until we have the name generator.

Without the `DeclNameGenerator` mechanism to be introduced in `4.21.0`, we are looking at something like ```lean def merge (dst src src' : Environment) : Environment × Std.HashMap Name Name := let dstLemmas := Meta.auxLemmasExt.getState dst let srcLemmas := Meta.auxLemmasExt.getState src let srcLemmas' := Meta.auxLemmasExt.getState src' let didx := srcLemmas'.idx - srcLemmas.idx let nameInfix := .str .anonymous s!"_merge_{dstLemmas.idx}" -- Construct the map by finding name collisions let map := srcLemmas'.lemmas.foldl (init := Std.HashMap.emptyWithCapacity didx) λ acc _ (name, _) => if src.contains name then acc else let name' := name.modifyBase (· ++ nameInfix) acc.insert name name' -- Rename the colliding lemmas in `src'`, including occurrences within constants let dst := Meta.auxLemmasExt.modifyState dst fun { idx, lemmas } => ⟨idx + 1, lemmas.insert type (auxName, levelParams)⟩ (dst.replayConsts src src', map) ``` but Lean's environment is really not conducive to renaming. I think we should wait until we have the name generator.

aniva added 1 commit 2025-06-27 16:01:50 -07:00

f4b6996f9e

test: Ignore branch unification test