panic and error with rw?

Stream: mathlib4

[Floris van Doorn]

The following example raises an error and panics on the latest mathlib for me. (Note that in the first example the intros is necessary to trigger it - I wonder whether it is related to instantiateMVars/cleanupAnnotations/withMainGoal or the like). I noticed the panic while minimizing the first example.

import Mathlib.Tactic.Rewrites

example : ∀ (x y : ℕ), x ≤ y  := by {
  intros x y
  rw? -- unknown free variable '_uniq.17'
}

example : ∀ (x y : ℕ), x ≤ y  := by {
  rw? -- Lean panics
}

[Floris van Doorn]

@Scott Morrison

[Floris van Doorn]

(I also had a panic when using apply? in a separate project, but I cannot reproduce that on the latest mathlib)

[Kyle Miller]

withLocation doesn't itself use withMainContext, which suggests its missing here:
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Rewrites.lean#L220

[Floris van Doorn]

Floris van Doorn said:

(I also had a panic when using apply? in a separate project, but I cannot reproduce that on the latest mathlib)

Is it possible that lake update and then lake exe cache get doesn't update the apply? cache? I have two projects depending on identical versions of mathlib, with identical configurations (lakefile, lake-manifest) except for the name, and in one project apply? panics on a line, and in the other project it doesn't panic on the same line. The first project was updated from a ~1 month old mathlib, the other one is brand new.

[Scott Morrison]

If you're still getting mathlib oleans you should be getting the apply? cache.

[Yury G. Kudryashov]

In this thread @Mauricio Collares found out that the reason is that two caches are there, and the wrong one is used.

[Scott Morrison]

@Floris van Doorn and @Kyle Miller, thanks for the report and the suggestion. I've also fixed the panic reported above in rw? at #5563.

[Heather Macbeth]

Oh snap, I also just got a panic in rw?. Is it the "unreachable code has been reached" one?

import Mathlib.Algebra.Ring.Defs
import Mathlib.Tactic.Rewrites

axiom K : Type
@[instance] axiom K.ring : Ring K

def foo : K → K := sorry

example : foo x = 1 ↔ ∃ k : ℤ, x = k := by
  rw?

[Heather Macbeth]

branch#hrmacbeth-panic-unreachable

[Scott Morrison]

Yes, #5563 should fix this.

[Scott Morrison]

(Sorry, rw? was tested exactly to the extent the test file indicates. Thanks everyone for giving it a spin regardless. :-)

[Heather Macbeth]

@Scott Morrison My panic seems to persist (I just merged in #5563)

[Scott Morrison]

@Heather Macbeth, now fixed on #5563.