search

opencompl / lean-mlir

A minimal development of SSA theory
Other
88 stars 10 forks source link

chore: disable kernel check for tests/LLVM #750

Closed tobiasgrosser closed 1 day ago

tobiasgrosser commented 2 days ago

This disables the kernel checks in Lean for our SSA to Expr lowering in tests/LLVM until https://github.com/leanprover/lean4/pull/4595 has been resolved. We are currently interested in LLVM expression-level statements. Disabling this check will allow us to get data on these expression level statements.

After this change, we can extract the following proofs.

Number of files in llvm's tests: 1516 Number of translated test files: 193 Number of successfully built test files: 185 Number of builds that failed: 6 Number of generated BitVector theorems: 1664 Occurrences of unsupported functions: 37407

github-actions[bot] commented 2 days ago

Alive Statistics: 89 / 93 (4 failed)