Fallout from lean#7717 in Aesop

Stream: nightly-testing

[Kim Morrison]

Just trying to bump Aesop to v4.19.0-rc1, but ran into trouble from @Kyle Miller's lean#7717. I'm surprised this didn't fail Mathlib's nightly-testing, however...

(@Kyle Miller, could you have a look?)

[Kim Morrison]

(Pinging @Jannis Limperg for visibility, too.)

[Kim Morrison]

% lake build
info: batteries: checking out revision '5a56dfa58c18a1c4c485e5e630f9035e56c0952b'
✖ [81/163] Building Aesop.BaseM
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib/lean:././.lake/build/lib/lean /Users/kim/projects/lean/lean4-2/build/release/stage1/bin/lean ././././Aesop/BaseM.lean -R ./././. -o ././.lake/build/lib/lean/Aesop/BaseM.olean -i ././.lake/build/lib/lean/Aesop/BaseM.ilean -c ././.lake/build/ir/Aesop/BaseM.c --json
error: ././././Aesop/BaseM.lean:46:42: unknown constant 'Aesop.RPINFCache.mk._flat_ctor'
error: Lean exited with code 1
✖ [158/163] Building Aesop.Script.StructureDynamic
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib/lean:././.lake/build/lib/lean /Users/kim/projects/lean/lean4-2/build/release/stage1/bin/lean ././././Aesop/Script/StructureDynamic.lean -R ./././. -o ././.lake/build/lib/lean/Aesop/Script/StructureDynamic.olean -i ././.lake/build/lib/lean/Aesop/Script/StructureDynamic.ilean -c ././.lake/build/ir/Aesop/Script/StructureDynamic.c --json
error: ././././Aesop/Script/StructureDynamic.lean:142:17: unknown constant 'Aesop.GoalWithMVars.mk._flat_ctor'
error: ././././Aesop/Script/StructureDynamic.lean:164:21: unknown constant 'Aesop.Script.TacticState.mk._flat_ctor'
error: Lean exited with code 1

[Kyle Miller]

I'm not seeing any error @Kim Morrison:

% git checkout bump_to_v4.19.0-rc1
branch 'bump_to_v4.19.0-rc1' set up to track 'origin/bump_to_v4.19.0-rc1'.
Switched to a new branch 'bump_to_v4.19.0-rc1'
% cat lean-toolchain
leanprover/lean4:v4.19.0-rc1
% lake build
info: downloading https://github.com/leanprover/lean4/releases/download/v4.19.0-rc1/lean-4.19.0-rc1-darwin_aarch64.tar.zst
Total: 399.9 MiB Speed:  34.3 MiB/s
info: installing /Users/kmill/.elan/toolchains/leanprover--lean4---v4.19.0-rc1
info: batteries: checking out revision '5a56dfa58c18a1c4c485e5e630f9035e56c0952b'
Build completed successfully.

[Kim Morrison]

Indeed, after a lake clean and restarting VS Code, lake build is working for me too.

[Kim Morrison]

The PR is failing in tests. @Kyle Miller do you have an opinion about the test in NormSimpUnchangedMVarAssigned?

I think perhaps the (new) failure is just fine, and we delete the test?

[Kyle Miller]

Do you know what the test is supposed to be testing?

With pp.explicit, I've gotten as far as seeing that the old state before aesop was

⊢ ∀ (x : Unit),
  @Eq Unit (@Foo.f Unit (@Foo.mk Unit (fun x ↦ Unit.unit) ?x) x) (@Foo.f Unit (@Foo.mk Unit (fun x ↦ Unit.unit) ?x) x)

but the new state is

⊢ Unit → () = ()

[Kyle Miller]

Here's a way we can preserve that state:

class Foo (α : Type u) where
  f : α → α
  p : True

class Bar (α : Type u) where
  toFoo : Foo α
  eq : ∀ x : α, Foo.f x = Foo.f x

def bar : Bar Unit where
  toFoo := { f := fun _ => (), p := ?x }
  eq := by aesop

[Kim Morrison]

Okay, but I agree with you that I don't see why we'd want to do that...

[Kim Morrison]

I will comment out that test in the PR, and we can ask @Jannis Limperg what they want to do with it.

[Kyle Miller]

Yeah, let's comment it out @Kim Morrison.

@Jannis Limperg In this code block, why does aesop solve for the ?x metavariable? I think it's not supposed to. At least, if you do aesop? it gives intro x; rfl, which doesn't solve that metavariable.