Correctly Changing Lean.Compiler.IR Data Structures

Stream: lean4 dev

[Siddharth Bhat]

@Anton Lorenzen and I have been experimenting with Lean's reference counting algorithms,
and we're now trying to change Lean's Compiler.IR. In doing so, we have stage1 build failures.
I am unsure as to whether these build failures are because we missed something in the implementation,
or if it necessicitates a update-stage0.

Here's the change we made, and failing test cases on stage1:

I'm worried that an update-stage0 might mask a bug that we've made in the implementation, leading to a corrupt stage0 compiler that silently builds a seemingly correct stage1/2 compiler.

---

If we do need to update stage0, are there any caveats in how we perform update-stage0?
In particular, I am worried about the issues mentioned in "Further bootstrapping complications". Do I need to set interpreter.prefer_native?

---

Here's the change we made, and failing test cases on stage1:

Failing debug build test

99% tests passed, 1 tests failed out of 1837

Total Test time (real) = 1946.25 sec

The following tests FAILED:
  1127 - leanruntest_evalBuiltinInit.lean (Failed)

Failing release build test

99% tests passed, 2 tests failed out of 1953

Total Test time (real) = 326.50 sec

The following tests FAILED:
  1127 - leanruntest_evalBuiltinInit.lean (Failed)
  1952 - leanlaketest_toml (Failed)

Our baseline lean commit is 9cb114eb8389d104fd69da2d289f768979b543f5, and here's the (two) commits
we have on top of this: https://github.com/opencompl/lean4/commits/2024-borrowing-baseline-NOBENCH/

[Sebastian Ullrich]

You adjusted the interpreter but the IR it is loading is still the unchanged one built by the stage 0 compiler. So indeed you need to update-stage0 and then use prefer_native in order to build stage 1 without depending on the interpreter

[Siddharth Bhat]

@Sebastian Ullrich thanks for the confirmation!

[Siddharth Bhat]

I was wondering: where does the interpreter load the old (stage0) IR from?

[Sebastian Ullrich]

The .oleans, which were created by stage 0

[Siddharth Bhat]

Right. I was wondering where in the codebase this loading happens.

[Siddharth Bhat]

(a pointer to a file / function name would be super :smile: )

[Sebastian Ullrich]

The interpreter gets passed the environment, the IR is in an environment extension

[Siddharth Bhat]

Super, danke!