trustLevel = 0 still trust fake olean files

Stream: lean4

[Kitsune Kiriha]

I do the following experiment:
s.png

1. Compile a lean file.
2. Manually modify the olean file to make it a mismatched (false) olean.
3. Compile another lean file which imports this false module, and set trustLevel = 0 (--trust=0).
4. Lean4 passes the proof and says the axioms set is correct.
   Do I have wrong understanding for trustLevel in documentation? I also see the Lean source code is simply discard this argument. Is it not implemented yet?

[James E Hanson]

I believe that --trust=0 doesn't do anything in Lean 4.

[Kitsune Kiriha]

Thanks, let me try lean4checker now.