cannot evaluate `[init]` declaration ... in the same module

Stream: lean4

[Riyaz Ahuja]

Hello. I'm trying to cache the file context of a given theorem, so that in multiple REPL evaluations of this theorem, I can just load the context (by context, i mean file contents up to the theorem start) rather than recompiling it every time.

For example, here's a lemma from the Carleson project:

import Carleson.CoverByBalls
import Mathlib.Data.Real.StarOrdered
import Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
import Mathlib.Order.CompletePartialOrder

open MeasureTheory Measure NNReal ENNReal Metric Filter Topology TopologicalSpace
noncomputable section

namespace MeasureTheory

class Measure.IsDoubling {X : Type*} [MeasurableSpace X] [PseudoMetricSpace X]
    (μ : Measure X) (A : outParam ℝ≥0) : Prop where
  measure_ball_two_le_same : ∀ (x : X) r, μ (ball x (2 * r)) ≤ A * μ (ball x r)
export IsDoubling (measure_ball_two_le_same)

section PseudoMetric

variable {X : Type*} [PseudoMetricSpace X]

lemma ball_subset_ball_of_le {x x' : X} {r r' : ℝ}
    (hr : dist x x' + r' ≤ r) : ball x' r' ⊆ ball x r := by
  intro y h
  have h1 : dist x y < r := by
    calc dist x y ≤ dist x x' + dist x' y := dist_triangle _ _ _
        _ < dist x x' + r' := by gcongr; exact mem_ball'.mp h
        _ ≤ r := hr
  exact mem_ball'.mpr h1

I need to run ball_subset_ball_of_le many times via the repl in order to verify correctness (between different AI-generated proofs, but the same declaration & context). However, it's quite inefficient to be having to also send the file context, which could include many imports, theorems, definitions, etc. through every single time I evaluate this one theorem (especially if the target theorem is near the end of the file). So, I've been trying to pickle the file contents up until the start of the theorem, and load them when needed:

Store:

{"cmd": "import Carleson.CoverByBalls\n[...]}

{"pickleTo":"temp.o","env":0}

Load:

{"unpickleEnvFrom": "temp.o"}

{"cmd": "lemma ball_subset_ball_of_le {x x' : X} {r r' : \u211d}\n    (hr : dist x x' + r' \u2264 r) : ball x' r' \u2286 ball x r := by\n  intro y h\n  have h1 : dist x y < r := by [...]", "allTactics": true,"env":0}

If I ran these together without the pickling (so compile all the context, and then load the theorem into that environment), everything works great. However, when I add the pickling, the storing step is fine, but when attempting to load the environment, I get:

stdout: {"env":0}

stderr: libc++abi: terminating due to uncaught exception of type lean::exception: cannot evaluate `[init]` declaration 'Mathlib.Tactic.GCongr.forwardExt' in the same module

It seems that the gcongr tactic is what causes this issue. Notably, in different examples, I have gotten the same error in the same REPL commands, but for norm_num. Does anyone know why this is happening, and how to fix it?

Any help is greatly appreciated, thanks!!

[Kim Morrison]

I don't know the answer to your question, sadly, but could you confirm you're doing all this on v4.17.0-rc1?

[Riyaz Ahuja]

The above example was on the older v4.15.0, but here is a simpler MWE with the same error message on v4.17.0-rc1 (about linarith this time, instead of gcongr!)

import Mathlib.Tactic

def two : ℝ := 2

example (x:ℝ) : 1+x = two → x = 1 := by
  intro h
  unfold two at h
  linarith

The storing REPL command:

{"cmd": "import Mathlib.Tactic\n\ndef two : \u211d := 2"}

{"pickleTo":"temp.o","env":0}

The load command:

{"unpickleEnvFrom": "temp.o", "env":0}

{"cmd": "example (x:\u211d) : 1+x = two \u2192 x = 1 := by\n  intro h\n  unfold two at h\n  linarith","env":0}

And the error:

{"env": 0}

libc++abi: terminating due to uncaught exception of type lean::exception: cannot evaluate `[init]` declaration 'Mathlib.Meta.NormNum.normNumExt' in the same module

[Riyaz Ahuja]

Seems like something weird is happening when attempting to pickle/unpickle tactics defined outside of the core lean library. Perhaps the unpickling process sees the loading of such an externally defined tactic like linarith as a new declaration in the current module, which is why it gets angry when you try using it in the same module?

[Riyaz Ahuja]

(Just spitballing, I have little experience in how tactic declarations/initializations work, especially when pickled or loaded)

[Riyaz Ahuja]

Also, I've recreated this error on v4.9.0 and v4.14.0 in addition to the above v4.15.0 and v4.17.0-rc1

[Sebastian Ullrich]

I believe pickling the environment is fundamentally incompatible with some metaprogramming features.

I need to run ball_subset_ball_of_le many times via the repl in order to verify correctness (between different AI-generated proofs, but the same declaration & context). However, it's quite inefficient to be having to also send the file context, which could include many imports, theorems, definitions, etc. through every single time I evaluate this one theorem (especially if the target theorem is near the end of the file).

I don't understand this part though, REPL (and even more so Pantograph) should allow you to continue from the point just before the theorem? Or are you talking about multiple machines?

[Riyaz Ahuja]

Not necessarily multiple machines, but different REPL/pantograph instances. This is because my proof optimization agent is running an iterative refinement process, each step of which depends on the correctness/error messages of the previous step. So, I’ve been calling out to the repl binary to evaluate each batch of theorems for each step of the refinement. However, if pickling won’t be possible, I suppose the smarter strategy is to have a persistent repl instance (this is handled by pantograph nicely, so I’d probably use that instead). Alternatively, I can preprocess the theorem so that the proofs of all of its preceding theorems are simply sorry, which is picklable.

There is probably a much smarter way to handle this, but all this iterative refinement is really just being used to collect training data for a more effective model, which will be able to slot into pantograph’s interface much more easily.

[Sebastian Ullrich]

Yes, this should just work with a single Pantograph instance