🖇️ Environment Delta Pickling #137

New Issue

aniva · 2024-12-08T16:11:48-08:00

aniva commented

2024-12-08 16:11:48 -08:00

Some tactics such as simp generates environment extensions. These should be pickled alongside the goal state or environment to ensure these tactics work properly.

https://leanprover.zulipchat.com/#narrow/channel/219941-Machine-Learning-for-Theorem-Proving/topic/Pantograph/near/486815694

Moreover, the current pickling method pickles the entire environment, whose size could be unbounded. This is a problem for parallelization on a cluster.

Some tactics such as `simp` generates environment extensions. These should be pickled alongside the goal state or environment to ensure these tactics work properly. https://leanprover.zulipchat.com/#narrow/channel/219941-Machine-Learning-for-Theorem-Proving/topic/Pantograph/near/486815694 Moreover, the current pickling method pickles the entire environment, whose size could be unbounded. This is a problem for parallelization on a cluster.

aniva added the

labels 2024-12-08 16:11:48 -08:00

aniva self-assigned this 2024-12-08 16:11:48 -08:00

aniva added this to the 0.2.22 milestone 2024-12-08 16:13:10 -08:00

aniva added the

priority

medium

label 2024-12-08 16:22:26 -08:00

aniva removed this from the 0.2.22 milestone 2024-12-09 20:19:25 -08:00

aniva added this to the 0.2.25 milestone 2025-01-13 12:35:24 -08:00

aniva referenced this issue

2025-01-13 12:44:40 -08:00

feat: Pickle constants in goal state #157

aniva added a new dependency 2025-01-13 12:45:16 -08:00

#157 feat: Pickle constants in goal state

aniva modified the milestone from 0.2.25 to 0.3

2025-01-24 15:06:56 -08:00

aniva removed this from the 0.3 milestone 2025-03-24 18:22:55 -07:00

aniva added this to the 0.4.0 milestone 2025-05-17 11:22:13 -07:00

aniva removed the

priority

medium

label 2025-05-17 11:22:17 -07:00

aniva changed title from ~~Pickle environment extensions~~ to Tracker: Environment Delta Pickling

2025-06-19 15:04:11 -07:00

aniva referenced this issue

2025-06-19 15:06:05 -07:00

Branch unification #132

aniva commented

2025-06-19 19:21:31 -07:00

One simple solution here is to collect all generated proof terms and check if they contain constants not in the parent environment.

Vide Mathlib4's https://leanprover-community.github.io/mathlib4_docs/Lean/Environment.html#Lean.Environment.replayConsts

One simple solution here is to collect all generated proof terms and check if they contain constants not in the parent environment. Vide Mathlib4's https://leanprover-community.github.io/mathlib4_docs/Lean/Environment.html#Lean.Environment.replayConsts

aniva added a new dependency 2025-06-20 12:16:49 -07:00

#216 feat(serial): Robust environment extension pickling

aniva changed title from ~~Tracker: Environment Delta Pickling~~ to 🖇️ Environment Delta Pickling

2025-06-25 10:44:18 -07:00

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

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

aniva modified the milestone from 0.4.0 to 0.3.4

2025-07-02 15:26:59 -07:00

Sign in to join this conversation.