search

opencompl / lean-mlir

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

chore: update to 2024-08-16 #541

Closed tobiasgrosser closed 2 months ago

tobiasgrosser commented 2 months ago

As we upstreamed a few of BitVec theorems to Lean earlier, these can now be deleted from our internal ForLean branch.

We also have to disable the doc-gen4 build, which is currently incompatible with the latest lean nightly. As this is resolved, we will enable it again.

Finally, there is currently one Hacker's Delight proof that is timing out. We comment out the relevant tactic and preserve the timeout information in a comment. We will revisit this as we further analyze the Hacker's Delight theorems.

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)