chore: re-enable native compilation

[ineol]

No description provided.

[tobiasgrosser]

Lean 2024-04-16 still yields: 😢

info: stderr:
ibc++abi: terminating due to uncaught exception of type lean::exception: error loading library, libLake_shared.so: cannot open shared object file: No such file or directory
error: Lean exited with code 134

[ineol]

I've been meaning to try on a Linux machine, because it works on my macbook, and it's strange that it tries to load Lake anyways.

[ineol]

It's very strange, because it worked on our Linux machine...

[github-actions]

leanSAT and Bitwuzla solved: 0
leanSAT and Bitwuzla provided 0 counterexamples
leanSAT and Bitwuzla both failed on 0 theorems
leanSAT failed and Bitwuzla succeeded on 0 theorems
leanSAT succeeded and Bitwuzla failed on 0 theorems
There were 0 inconsistencies
Errors raised: 365
ran rg 'Bitwuzla failed' | wc -l, expected 0, found 0, SUCCESS
ran rg 'LeanSAT failed' | wc -l, expected 0, found 0, SUCCESS
ran rg 'LeanSAT provided a counter' | wc -l, expected 0, found 0, SUCCESS
ran rg 'Bitwuzla provided a counter' | wc -l, expected 0, found 0, SUCCESS
ran rg 'LeanSAT proved' | wc -l, expected 0, found 0, SUCCESS
ran rg 'Bitwuzla proved' | wc -l, expected 0, found 0, SUCCESS
error build failed was raised 365 times

[github-actions]

bv_decide solved 0 theorems.
bitwuzla solved 0 theorems.
bv_decide found 0 counterexamples.
bitwuzla found 0 counterexamples.
bv_decide only failed on 0 problems.
bitwuzla only failed on 0 problems.
both bitwuzla and bv_decide failed on 0 problems.
In total, bitwuzla saw 0 problems.
In total, bv_decide saw 0 problems.
ran rg 'LeanSAT provided a counter' | wc -l, this file found 0, rg found 0, SUCCESS
ran rg 'Bitwuzla provided a counter' | wc -l, this file found 0, rg found 0, SUCCESS
ran rg 'LeanSAT proved' | wc -l, this file found 0, rg found 0, SUCCESS
ran rg 'Bitwuzla proved' | wc -l, this file found 0, rg found 0, SUCCESS
raw-data/InstCombine/g2004h08h10hBoolSetCC_proof_ceg_data.csv
raw-data/InstCombine/g2004h08h10hBoolSetCC_proof_solved_data.csv
raw-data/InstCombine/g2004h08h10hBoolSetCC_proof_err_data.csv

[tobiasgrosser]

@ineol, is this still something you would like to enable in CI?

[tobiasgrosser]

In fact, #1415 seems more up-to-date.