Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

pp.instantiateMVars false does not seem to work #4406

Closed
nomeata opened this issue Jun 8, 2024 · 2 comments · Fixed by #4558
Closed

pp.instantiateMVars false does not seem to work #4406

nomeata opened this issue Jun 8, 2024 · 2 comments · Fixed by #4558
Labels
bug Something isn't working

Comments

@nomeata
Copy link
Contributor

nomeata commented Jun 8, 2024

Consider

import Lean.Elab.Command
open Lean Meta

run_meta do
  let mvarId ← mkFreshExprMVar (.some (.const ``Nat []))
  mvarId.mvarId!.assign (mkNatLit 0)
  withOptions (pp.instantiateMVars.set · false) do
    logInfo m!"{mvarId}"

or

import Lean.Elab.Command
open Lean Meta

set_option pp.instantiateMVars false in
run_meta do
  let mvarId ← mkFreshExprMVar (.some (.const ``Nat []))
  mvarId.mvarId!.assign (mkNatLit 0)
  logInfo m!"{mvarId}"

Both print 0 when I would have expected some form of ?m.

The ability to print expressions without mvars instantiated is rarely needed, but it is quite relevant when debugging bad mvar assignments.

Respectfully pinging @kmill.

Versions

4.10.0-nightly-2024-06-08

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
@nomeata nomeata added the bug Something isn't working label Jun 8, 2024
@kmill
Copy link
Collaborator

kmill commented Jun 8, 2024

The situation is that the first step of Lean.ppExprWithInfos is to instantiate mvars. (Note that the default value for pp.instantiateMVars is false!) I agree that it would be useful when debugging to see where there are mvars in expressions.

Maybe here's a plan:

  1. set the default value of pp.instantiateMVars to true
  2. find all main entry points to the pretty printer, and either delete any instantiateMVars that appear there, or move instantiateMVars to the format/backup case if present.

@nomeata
Copy link
Contributor Author

nomeata commented Jun 8, 2024

That plan sounds very reasonable to me, thanks for the analysis.

kmill added a commit to kmill/lean4 that referenced this issue Jun 25, 2024
@kmill
fix: set default value of pp.instantiateMVars to true and make the …
00278f9 
…option be effective

Before, `pp.instantiateMVars` generally had no effect.

This also has an effect in hovers, where metavariables can be unfolded one assignment at a time. However, the goal state still sees all metavariables instantiated due to the fact that the algorithm relies on expression equality post-instantiation (see `Lean.Widget.goalToInteractive`).

Closes leanprover#4406
@kmill kmill mentioned this issue Jun 25, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Jul 2, 2024
@kmill
fix: set default value of pp.instantiateMVars to true and make the …
3f2cf8b 
…option be effective (#4558)

Before, `pp.instantiateMVars` generally had no effect because most call
sites for the pretty printer instantiated metavariables first, but now
this functionality is entrusted upon the `pp.instantiateMVars` option.

This also has an effect in hovers, where metavariables can be unfolded
one assignment at a time. However, the goal state still sees all
metavariables instantiated due to the fact that the algorithm relies on
expression equality post-instantiation (see
`Lean.Widget.goalToInteractive`).

Closes #4406
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: set default value of pp.instantiateMVars to true and make the option be effective kmill/lean4
2 participants
@nomeata @kmill