Using leaff to verify a refactor

Stream: batteries

[Alex Keizer]

I'm trying to use leaff to check that std4#646 does not introduce any unintended functional changes.
Running it locally gives an error:

uncaught exception: invalid .olean file header, likely due to a Lean version mismatch
        you may wish to disable CHECK_OLEAN_VERSION / LEAN_CHECK_OLEAN_VERSION in your Lean build,
        or manually adjust the Lean version used by Leaff and hope for the best

Indeed, std is using v4.6.0-rc1, while leaff uses v4.5.0-rc1. I tried to let leaff use 4.6 as well, but that didn't work.
How do I actually disable CHECK_OLEAN_VERSION? I tried a few variations of

CHECK_OLEAN_VERSION=false ./runleaf Std ../std4 ../std4-main

But all gave the same error as before

[Mac Malone]

@Alex Keizer The notice about setting CHECK_OLEAN_VERSION is for custom builds of Lean form th source. There is no way to disable CHECK_OLEAN_VERSION in a release version of Lean. This is for good reason, as oleans from different toolchains are highly unlikely to be compatible and will likely cause a segfault if loaded across versions. The only tried and true way to solve this is to have Leaff update to use v4.6.0-rc1 as well (i.e., potentially bug @Alex J. Best ).

[Kim Morrison]

@Alex J. Best , the Leaff README instructions don't work for me.

I was hoping that cloning, lake build, and ./runleaff.sh Mathlib ../test-mathlib2/ ../test-mathlib/ would do something, but this doesn't configure the mathlib=on flag properly. Could you update the README with instructions that work from a clean clone?

[Kim Morrison]

After irreproducibly fiddling, I did get something to happen, but only:

fatal: reference is not a tree: d9ba3f07499769fc5730aea4be84298a2c13ff61

[Alex J. Best]

@Mac Malone is it definitely always true that the olean format will change every time lean changes versions. As the message is meant to imply building with that flag is experimental, and I never properly tried but I'd have imagined that some lean version bumps or commits to lean master wouldn't actually change the olean format, so with the above caveat emptor it might be worth a shot.

[Alex J. Best]

To be clear building here means rebuilding lean itself not leaff

[Sebastian Ullrich]

It changes relatively rarely (it depends a bit on which parts of the olean file you actually inspect) but there are no guarantees and if it does change, access is undefined behavior

[Alex J. Best]

Ok indeed that was my impression. I'd imagine that the extension diffs are more likely to fault than the declarations so maybe an option to disable those would be helpful

[Alex Keizer]

Right, I've submitted a PR to leaff that bumps the lean version. That seemed easier than messing with a custom lean build and hoping that things don't break :sweat_smile:

[Alex Keizer]

And now I get:

> ./runleaff.sh Std ../std4 ../std4-main
uncaught exception: unknown package 'Std'

Am I doing something wrong, or did I break something with the version bump?

I also tried std instead of Std, no luck there either

[Alex J. Best]

@Alex Keizer did you run lake build in both std4 and std4-main

[Alex J. Best]

Does your username or the directory that everything is in have spaces in?

[Alex J. Best]

Thanks for the pr will try and review shortly

[Alex Keizer]

Alex J. Best said:

Alex Keizer did you run lake build in both std4 and std4-main

I did not, I didn't know this was a requirement. After I built them, it now works :tada:

[Alex J. Best]

Ok great! I'll try and update the instructions to make that clearer

[Alex Keizer]

I took the liberty of opening a PR to add a sentence to the readme: https://github.com/alexjbest/leaff/pull/8

[Alex Keizer]

Also, when leaff reports that a type has changed, is there some way to make it print the old and new types as well, for manual comparison?

[Alex J. Best]

Amazing, thanks, merged. It can't currently but that is one of the features I'm hoping to add next. It shouldn't be too hard so hopefully can get to it soone