Could not load mathlib environment from saved file #225

New Issue

aniva · 2025-07-01T12:35:21-07:00

aniva commented

2025-07-01 12:35:21 -07:00

To reproduce: Clone Mathlib, and

Execute in one instance lake env $PANTOGRAPH/repl Mathlib

env.save {"path": "/tmp/env.olean"}
goal.start {"expr": "forall (n : Nat), n = n"}
goal.save {"id": 0, "path": "/tmp/goal.olean"}

Then, execute in another instance lake env $PANTOGRAPH/repl Init

env.load {"path": "/tmp/env.olean"}
goal.load {"path": "/tmp/goal.olean"}
goal.print {"stateId": 0, "goals": true}
goal.tactic {"stateId": 0, "tactic": "intro n"}

To reproduce: Clone Mathlib, and Execute in one instance `lake env $PANTOGRAPH/repl Mathlib` ```jsonl env.save {"path": "/tmp/env.olean"} goal.start {"expr": "forall (n : Nat), n = n"} goal.save {"id": 0, "path": "/tmp/goal.olean"} ``` Then, execute in another instance `lake env $PANTOGRAPH/repl Init` ```jsonl env.load {"path": "/tmp/env.olean"} goal.load {"path": "/tmp/goal.olean"} goal.print {"stateId": 0, "goals": true} goal.tactic {"stateId": 0, "tactic": "intro n"} ```

aniva added the

labels 2025-07-01 12:35:21 -07:00

aniva commented

2025-07-01 12:47:59 -07:00

The main problem is this part:

// src/library/compiler/ir_interpreter.cpp

        // no native code, so might be part of the current module
        if (get_regular_init_fn_name_for(m_env, fn)) {
            // We don't know whether `[init]` decls can be re-executed, so let's not.
            throw exception(sstream() << "cannot evaluate `[init]` declaration '" << fn << "' in the same module");
        }

i.e. initialization of [init] declarations.

The main problem is this part: ```c++ // src/library/compiler/ir_interpreter.cpp // no native code, so might be part of the current module if (get_regular_init_fn_name_for(m_env, fn)) { // We don't know whether `[init]` decls can be re-executed, so let's not. throw exception(sstream() << "cannot evaluate `[init]` declaration '" << fn << "' in the same module"); } ``` i.e. initialization of `[init]` declarations.

Sign in to join this conversation.