Pending mvars cause generation of closures #239

New issue

Closed

opened 2025-07-12 00:04:08 -07:00 by aniva · 3 comments

aniva commented

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

Owner

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

Author

Owner

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

Author

Owner

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

aniva referenced this issue from a pull request that will close it,

2025-07-13 23:01:05 -07:00

fix(serial): Erase closures in synthetic mvars #240

aniva commented

2025-07-13 23:02:21 -07:00

Author

Owner

Resolved by #240

aniva closed this issue