Update to recent version

[pimotte]

For our use of Verbose Lean, we combine it with Verso. Due to a bug in Verso, we need to be way past v4.25.0 if we want to update (see #lean4 > Verso: Updating Waterproof Genre for details).

One of the challenges in this upgrade is the deprecation of cc in favour of grind. #lean4 > strict grind only contains a possible solution.

@PatrickMassot This is more of a tracking issue for when one of our students or I could pick this up. If you have any (partial) progress in updating, we'd love to know, if this rises to the top of our backlog we'll let you know here if we start working on this.

[PatrickMassot]

Yes, I think you correctly identified the main challenge. Help is very welcome. Clearly I won’t update myself in the middle of a semester when I teach using Verbose. So there is no risk of collision.

[pimotte]

I've done some investigation based on existing exercises:

The only issue with existing exercises for the update to v4.27.0 is the one that #27 addresses.

In the upgrade to v4.28.0, there are two kinds of failing exercises.

Those that deduce an implication from a bi-implication:

example (P Q : Prop) (hPQ : P ↔ Q) : True := by
  Since P ↔ Q we get that P → Q and Q → P
  trivial

One exercise that needs the following:

example (a b c d : ℝ) (h : a = b) (h': c = d) : a - c = b - d := by
  Since a = b and c = d we conclude that a - c = b - d

We could address the first by adding the reverse of LogicIntros (LogicElims?) for anonymous fact splitting lemma's.
If we can address the second one (/the class of exercises it represents) by something as well, we might be able to reduce some complexity and just remove the entire cc part.

If not, then I think the strict grind route is a fine solution.