aesop try this regression

Stream: general

[Kim Morrison]

I see that on nightly-2024-11-03 (which has just become v4.14.0-rc1), in aesop we now have:

-- FIXME: the tombstone in the "try this" suggestion below appeared in nightly-2024-11-03,
-- presumably because of https://github.com/leanprover/lean4/pull/5898
/--
info: Try this:
simp_all (config✝ := { }) only
-/
#guard_msgs in
example : True := by
  aesop? (config := {}) (simp_config := {})

@Kyle Miller and @Jannis Limperg, can I hand this off to you to decide if further changes are required.

For now, I'm going to commit this changed test to master.

[Jannis Limperg]

I'm looking into it.

[Jannis Limperg]

@Kyle Miller is it possible that this syntax declaration is slightly wrong?

syntax valConfigItem := atomic(" (" notFollowedBy(&"discharger" <|> &"disch") (ident <|> &"config")) " := " withoutPosition(term) ")"

With ident <|> &"config", I would expect that ident overlaps &"config", and hence that the second alternative is never considered.

[Jannis Limperg]

aesop#175 adds a workaround.