Switch off common subexpression elimination

Stream: lean4

[John Tristan]

Is there a simple way to switch off common subexpression elimination in the code generator?

[Henrik Böving]

Unfortunately not no. The new compiler does have a highly modifiable compilation pass pipeline but its not production ready yet and also, as of now, not being worked on though that will change again at some point.

Are you having issues with CSE and linearity?

[John Tristan]

No, I'm exploring some idea for doing probabilistic computation

[Henrik Böving]

If you want to show some code I can try to figure something out but if the only possible approach is to disable CSE you're out of luck I'm afraid.

[Tomas Skrivan]

John Tristan said:

No, I'm exploring some idea for doing probabilistic computation

I'm playing around with probabilistic programming and I didn't run into such issue. Can you share some code where common subexpression elimination causes issues?

[John Tristan]

I ran into this problem because I was trying something out and playing with the FFI (and I was doing it wrong). I'll share something when it is presentable. But I do agree that there are ways to do verification of probabilistic computation that do not have such issues, I have an example here: https://github.com/leanprover/SampCert

[Tomas Skrivan]

I was suspecting ffi, you probably didn't respect purity i.e. pure function was returning random output. The solution is to wrap it in IO monad.

[John Tristan]

Exactly. I'm now calling lean_io_result_mk_ok and my tests are working.