aesop test instability

Stream: nightly-testing

[Kim Morrison]

@Jannis Limperg, the tests

-- example : |a + b| ≤ |c + d| := by
--   aesop!
--   guard_hyp fwd_1 : |a + b| ≤ |a| + |b|
--   guard_hyp fwd : |c + d| ≤ |c| + |d|
--   falso

and

-- example (m n : Nat) : (↑m : Int) < 0 ∧ (↑n : Int) > 0 := by
--   set_option aesop.check.script.steps false in -- TODO lean4#4315
--   set_option aesop.check.script false in
--   aesop (config := { enableSimp := false, warnOnNonterminal := false })
--   all_goals
--     guard_hyp fwd   : 0 ≤ (n : Int)
--     guard_hyp fwd_1 : 0 ≤ (m : Int)
--     falso

in AesopTest/RulePattern.lean seem to fail on every new release, when the naming of the introduced hypotheses flips. This requires manual intervention during the release process.

In this cycle, I've simply commented out these tests. (https://github.com/leanprover-community/aesop/pull/251) Do you think you could look into make these more robust (either in implementation or in testing)?