check defeq between different versions of lean

Stream: lean4

[Matthew Ballard]

I would like to be able to check which declarations in mathlib might have materially changed, eg no longer defeq or maybe defeq but in a more expensive manner, after building the library with a new toolchain.

I asked Mario about this in meeting-series-formally-known-as-porting today but I don't have the capacity at the moment to pursue his suggestion as I've never directly touched an olean. He also mentioned mathport as similar case.

I was wondering if anyone has anything along these lines already.

Also is there an easy way to trick lake into doing this for me?