Skip to content

Tags: opencompl/lean-mlir

Tags

blase-v0.0.1

Toggle blase-v0.0.1's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
fix: stop swallowing LLVM status code on evaluation CI failure (#1628)

Previously the CI would be green even if the script raised an error,
because our script would swallow the non-zero status code in the code
that persisted the error to the environment, so we ensure that the
second branch also exits with a non-zero code.

oopsla25-bv-decide

Toggle oopsla25-bv-decide's commit message
chore: final artifact changes

ITP24

Toggle ITP24's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
feat: rewritePeepholeRecursively (#410)

@tobiasgrosser spotted that 'rewritePeephole' only works at one level of
the IR,
and will not recurse into regions.
We write a variant ('rewritePeepholeRecursively').
This first calls 'rewritePeephole' on the 'Com'.
Then, it recurses into each let-binding of the 'Com' to call
'rewritePeepholeRecursively' on all region arguments.
This ensures that the rewrite is applied to all occurrences of the lhs
in all (nested) regions.

This supercedes #408

ITP24V2

Toggle ITP24V2's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
feat: rewritePeepholeRecursively (#410)

@tobiasgrosser spotted that 'rewritePeephole' only works at one level of
the IR,
and will not recurse into regions.
We write a variant ('rewritePeepholeRecursively').
This first calls 'rewritePeephole' on the 'Com'.
Then, it recurses into each let-binding of the 'Com' to call
'rewritePeepholeRecursively' on all region arguments.
This ensures that the rewrite is applied to all occurrences of the lhs
in all (nested) regions.

This supercedes #408

v0.1.3

Toggle v0.1.3's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
feat: new version of artifact with more explanations. (#399)

v0.1.2

Toggle v0.1.2's commit message
chore: explain better what is to be verified

list

Toggle list's commit message
chore: explain better what is to be verified

v0.1.1

Toggle v0.1.1's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
chore: fix tests (#336)

This fixed #334.

v0.1.0

Toggle v0.1.0's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Merge pull request #156 from opencompl/alive-hardest-proof-1

feat: add proof of DivRemOfSelect

slowdown-1

Toggle slowdown-1's commit message
Simplify test case