The ml-kem lax-checking CI job should be using the same hax commit for extraction and hax-lib. For now it uses the hax commit it is ran against for extraction, but it uses main for hax-lib (because libcrux's Cargo.toml points to hax main). For PRs that make changes to hax-lib we need to run this job using hax-lib from the commit being tested.
The current situation is quite annoying in situations like: #1199 (comment)