Pickle environment extensions #137

New Issue

Open

opened 2024-12-08 16:11:48 -08:00 by aniva · 0 comments

aniva commented

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

Owner

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

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

aniva added the

part/Environment

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

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

Sign in to join this conversation.

No Label

part/Environment

No Milestone

No project

No Assignees

1 Participants

Notifications

Due Date

The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Depends on

#157 feat: Pickle constants in goal state

aniva/Pantograph

Reference: aniva/Pantograph#137

No description provided.