Skip to content

chore: enable native compilation#1415

Open
ineol wants to merge 1 commit intomainfrom
push-mrstwyxkolzr
Open

chore: enable native compilation#1415
ineol wants to merge 1 commit intomainfrom
push-mrstwyxkolzr

Conversation

@ineol
Copy link
Copy Markdown
Collaborator

@ineol ineol commented Jun 30, 2025

No description provided.

@github-actions
Copy link
Copy Markdown
Contributor

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
The InstCombine benchmark contains 4520 theorems in total.
Saved dataframe at: /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/raw-data/InstCombine/instcombine_ceg_data.csv
Saved dataframe at: /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/raw-data/InstCombine/instcombine_solved_data.csv

@tobiasgrosser
Copy link
Copy Markdown
Collaborator

Updated to latest main to check if native_compilation works again.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants