Pending mvars cause generation of closures #239

New Issue

aniva · 2025-07-12T00:04:08-07:00

aniva commented

2025-07-12 00:04:08 -07:00

Test case:

frontend.process {"file": "example : True := sorry", "sorrys": true, "newConstants": false, "readHeader": false, "inheritEnv": false, "typeErrorsAsGoals": false}
goal.tactic {"stateId": 0, "have": "0 < 2"}
goal.tactic {"stateId": 1, "tactic": "norm_num"}
goal.save {"id": 2, "path": "/tmp/goal.olean"}
goal.print {"stateId": 2, "extraMVars": ["_uniq.225"]}
goal.print {"stateId": 2, "rootExpr": true}
goal.tactic {"stateId": 2, "tactic": "decide"}
goal.tactic {"stateId": 3, "tactic": "decide"}
goal.print {"stateId": 3, "rootExpr": true}

At goal.save, the error is

INTERNAL PANIC: closures cannot be compacted. One possible cause of this error is trying to store a function in a persistent environment extension.

However, this is solved if 0 < 2 is replaced by (0 : Nat) < 2.

Test case: ``` frontend.process {"file": "example : True := sorry", "sorrys": true, "newConstants": false, "readHeader": false, "inheritEnv": false, "typeErrorsAsGoals": false} goal.tactic {"stateId": 0, "have": "0 < 2"} goal.tactic {"stateId": 1, "tactic": "norm_num"} goal.save {"id": 2, "path": "/tmp/goal.olean"} goal.print {"stateId": 2, "extraMVars": ["_uniq.225"]} goal.print {"stateId": 2, "rootExpr": true} goal.tactic {"stateId": 2, "tactic": "decide"} goal.tactic {"stateId": 3, "tactic": "decide"} goal.print {"stateId": 3, "rootExpr": true} ``` At `goal.save`, the error is ```lean INTERNAL PANIC: closures cannot be compacted. One possible cause of this error is trying to store a function in a persistent environment extension. ``` However, this is solved if `0 < 2` is replaced by `(0 : Nat) < 2`.

aniva added this to the v0.3.5 milestone 2025-07-12 00:04:08 -07:00

aniva added the

labels 2025-07-12 00:04:08 -07:00

aniva self-assigned this 2025-07-12 00:04:08 -07:00

aniva commented

2025-07-12 00:08:13 -07:00

This is probably related to

inductive SyntheticMVarKind where
  /--
  Use typeclass resolution to synthesize value for metavariable.
  If `extraErrorMsg?` is `some msg`, `msg` contains additional information to include in error messages
  regarding type class synthesis failure.
  -/
  | typeClass (extraErrorMsg? : Option MessageData)
  /--
  Use coercion to synthesize value for the metavariable.
  If synthesis fails, then throws an error.
  - If `mkErrorMsg?` is provided, then the error `mkErrorMsg expectedType e` is thrown.
    The `mkErrorMsg` function is allowed to throw an error itself.
  - Otherwise, throws a default type mismatch error message.
    If `header?` is not provided, the default header is "type mismatch".
    If `f?` is provided, then throws an application type mismatch error.
  -/
  | coe (header? : Option String) (expectedType : Expr) (e : Expr) (f? : Option Expr)
      (mkErrorMsg? : Option (MVarId → Expr → Expr → MetaM MessageData))
  /--
  Use tactic to synthesize value for metavariable.

  If `delayOnMVars` is true, the tactic will not be executed until the goal is free of unassigned
  expr metavariables.
  -/
  | tactic (tacticCode : Syntax) (ctx : SavedContext) (kind : TacticMVarKind) (delayOnMVars := false)
  /-- Metavariable represents a hole whose elaboration has been postponed. -/
  | postponed (ctx : SavedContext)
  deriving Inhabited

This is probably related to ```lean4 inductive SyntheticMVarKind where /-- Use typeclass resolution to synthesize value for metavariable. If `extraErrorMsg?` is `some msg`, `msg` contains additional information to include in error messages regarding type class synthesis failure. -/ | typeClass (extraErrorMsg? : Option MessageData) /-- Use coercion to synthesize value for the metavariable. If synthesis fails, then throws an error. - If `mkErrorMsg?` is provided, then the error `mkErrorMsg expectedType e` is thrown. The `mkErrorMsg` function is allowed to throw an error itself. - Otherwise, throws a default type mismatch error message. If `header?` is not provided, the default header is "type mismatch". If `f?` is provided, then throws an application type mismatch error. -/ | coe (header? : Option String) (expectedType : Expr) (e : Expr) (f? : Option Expr) (mkErrorMsg? : Option (MVarId → Expr → Expr → MetaM MessageData)) /-- Use tactic to synthesize value for metavariable. If `delayOnMVars` is true, the tactic will not be executed until the goal is free of unassigned expr metavariables. -/ | tactic (tacticCode : Syntax) (ctx : SavedContext) (kind : TacticMVarKind) (delayOnMVars := false) /-- Metavariable represents a hole whose elaboration has been postponed. -/ | postponed (ctx : SavedContext) deriving Inhabited ```

aniva commented

2025-07-12 00:31:07 -07:00

Setting this in goal state pickle suppresses the error

    { «elab» with syntheticMVars := {} },

After tracking down this a little more, it seems like MessageData is the root of all the problems here. I'm inclined to delete all the MessageDatas during pickling.

Setting this in goal state pickle suppresses the error ```lean { «elab» with syntheticMVars := {} }, ``` After tracking down this a little more, it seems like `MessageData` is the root of all the problems here. I'm inclined to delete all the `MessageData`s during pickling.

aniva added a new dependency 2025-07-12 12:09:05 -07:00

#238 Test Lean-Repl bugs

Sign in to join this conversation.