Skip to content

Use `-native-compiler no` to make sure we do not rely on (bugs) in `native_compute`.

Robbert Krebbers requested to merge robbert/no_native_compiler into master

In std++ and Iris we do not use native_compute, so relying on it needlessly increases the trusted code base. Since recently an unsoundness bug in naive_compute was discovered (which was also fixed immediately), I wonder if it wouldn't make sense to just disable native_compute altogether in std++ and Iris.

Merge request reports