leanprover-community / repl

A simple REPL for Lean 4, returning information about errors and sorries.
69 stars 16 forks source link

feat: pickle and unpickle Environments #11

Closed kim-em closed 11 months ago

kim-em commented 11 months ago

As a test, I pickled the result of

import Mathlib

def f := 42

and produced a 5kb olean file. (This is good: we're not accidentally storing content from the imports.)