autoparam makes linter/error reporting go haywire

Stream: lean4

[Kevin Buzzard]

This has happened to me a couple of times, and also to several others in Banff, but I've always put off minimising until now:

import Aesop

structure foo where
  fac : 2+2=4 := by aesop
  uniq : False

example : foo
    where
  uniq := by
    simp
    sorry

In the example, fac is being proved by aesop automatically. But working with the proof of uniq is hard. Try adding skip between simp and sorry, and linter.unreachableTactic will suddenly get really excited. As you add more code, more random things can occur. You can "reset" the system and (temporarily) make the warnings go away in two ways: either insert fac := sorry (so don't let aesop solve it) or go back to exactly the proof you had before you started editing (and it's temporarily fine, but then breaks again the moment you start editing).

In a large file the breakage can be far more serious: red error warnings start appearing in the wrong place with incorrect errors, and Lean becomes unusable, but I don't know if this is a different problem.

[Kevin Buzzard]

You don't even need the autoparam. If you want to understand the problem, try filling in the proof of uniq below. Lean is completely unusable (at least for me -- goal state doesn't update etc etc)

import Aesop

structure foo where
  fac : 2+2=4
  uniq : ∀ P : Prop, ¬ (P ↔ ¬ P)

example : foo where
  fac := by aesop
  uniq := by

    sorry

[Oliver Nash]

Thank you very much for identifying and minimising this. I was driven mad by this yesterday and today.

[Mario Carneiro]

Here's something that at least partially explains what's going on: Put this in

import Aesop

structure foo where
  fac : 2+2=4
  uniq : ∀ P : Prop, ¬ (P ↔ ¬ P)

set_option trace.Elab.info true
example : foo where
  fac := by aesop
  uniq := by

    sorry

and then try putting a space in the blank line before sorry. Before adding the space, you should be able to see several lines in the info tree referring to the span ⟨12, 4⟩-⟨12, 9⟩, which is the location of the word sorry (note that it starts on line 12, has 4 spaces before it, and is 5 characters long). However, after adding the space on line 11, this span will shift to ⟨12, 3⟩-⟨12, 8⟩, which should not happen because it is still 4 characters indented. If you keep adding spaces this count will keep going down until it gets to ⟨11, 5⟩-⟨11, 10⟩, i.e. it thinks it is entirely on the previous line which is nonsense.

[Mario Carneiro]

My guess is that something deleted some leading or trailing whitespace in the original tokens, leading to a mismatch between the indexes in the original source and the indexes in the syntax

[Oliver Nash]

Thanks, I can reproduce what you describe.

[Mario Carneiro]

I think some kind of snapshotting is also involved, because if you make an edit to the word aesop it will "reset" and work even with spaces on the line before sorry, but if you change those spaces then again the problem comes back

[Mario Carneiro]

@Jannis Limperg Does aesop make use of the checkpoint / save stuff internally?

[Mario Carneiro]

this behavior is also consistent with using a syntax from an old version of the document (which internally uses byte positions into the input) while the input changes

[Kevin Buzzard]

Oliver Nash said:

Thank you very much for identifying and minimising this. I was driven mad by this yesterday and today.

It's not the first time I've seen this, but thanks to you and Scott for encouraging me to minimise!

[Mario Carneiro]

I am strongly suspecting checkpoint as the source of the issue

[Mario Carneiro]

turns out it's pretty challenging to use elaborated info from a previous version of the document once the text moves around

[Mario Carneiro]

aesop_no_checkpoint does not exhibit the bug

[Mario Carneiro]

Hm, this is an almost aesop-free version of the MWE:

import Aesop

structure foo where
  fac : 2+2=4
  uniq : ∀ P : Prop, ¬ (P ↔ ¬ P)

set_option trace.Elab.info true
example : foo where
  fac := by checkpoint rfl
  uniq := by

    sorry

But it turns out the import Aesop at the top is load-bearing! If you remove it or replace it with import Lean the behavior goes away

[Mario Carneiro]

Oh :face_palm: the error is still there without import Aesop, it just isn't running the unreachableTactic linter unless you import Std

[Mario Carneiro]

My recommendation is just to avoid checkpoint. I think a correct implementation is quite challenging, and what we have currently isn't very reliable

[Mario Carneiro]

Here's a hack to make aesop not use checkpoint:

import Aesop

macro_rules
  | `(tactic| aesop $cs*) => `(tactic| aesop_no_checkpoint $cs*)
  | `(tactic| aesop? $cs*) => `(tactic| aesop_no_checkpoint? $cs*)

structure foo where
  fac : 2+2=4
  uniq : ∀ P : Prop, ¬ (P ↔ ¬ P)

set_option trace.Elab.info true
example : foo where
  fac := by aesop
  uniq := by

    sorry

[Oliver Nash]

Thanks so much for all this.

[Oliver Nash]

Where do we go from here? Open an issue / PR / pester Aesop authors here on Zulip?

[Siddharth Bhat]

Mario Carneiro said:

My recommendation is just to avoid checkpoint. I think a correct implementation is quite challenging, and what we have currently isn't very reliable

@Mario Carneiro I make somewhat heavy use of save to make proofs with large terms somewhat tolerable.

Would you say that relying on save is a bad idea in general?

[Mario Carneiro]

If it works for you, great. I've just had a lot of bad or confusing experiences with it

[Mario Carneiro]

I don't think it is reliable enough to use by default in tactics like aesop

[Mario Carneiro]

I need to read up on the implementation though, maybe the present issue is fixable

[Oliver Nash]

I just opened two issues about this:

• One for Lean4: https://github.com/leanprover/lean4/issues/2250
• One for Aesop: https://github.com/JLimperg/aesop/issues/57

[Oliver Nash]

Many thanks to @Jannis Limperg for such a quick resolution of https://github.com/JLimperg/aesop/issues/57

Do I understand correctly that Mathlib will automatically pick up this new logic thanks to https://github.com/leanprover-community/mathlib4/blob/d4a3d0440c6e2966175eeb3ff62bd11def2eabd8/lakefile.lean#L31 ?

[Jannis Limperg]

No, this still needs a bump PR. Lake freezes dependency versions in lake-manifest.json.

[Oliver Nash]

I see thanks (I am relieved these are not open dependencies). I've made an attempt to update it with !4#4570 I'll have to wait till morning to see if CI is happy.