Skip to content

Issues: opencompl/lean-mlir

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

42 Open 55 Closed
42 Open 55 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

llvm: test_two_argument_ranges_thm
#831 opened Nov 12, 2024 by tobiasgrosser
1
@lfrenot
1
div to shift
#825 opened Nov 12, 2024 by tobiasgrosser
@bollu
slow proofs
#802 opened Nov 7, 2024 by tobiasgrosser
slow llvm benchmarks
#766 opened Nov 3, 2024 by tobiasgrosser
Update to Lean 2024-09-26 broke bv_automata
#660 opened Sep 27, 2024 by luisacicolini
8
Complete lemmas that relate shifting with &&& allOnes
#614 opened Sep 13, 2024 by tobiasgrosser
@luisacicolini
2
MLIR bytecode reader/writer
#565 opened Aug 23, 2024 by bollu
Bug: Why does GitHub workflow build Mathlib? bug Something isn't working
#500 opened Jul 31, 2024 by AtticusKuhn
3
Idea: Possible way to shorten the code of the MLIR Parser enhancement New feature or request
#473 opened Jul 17, 2024 by AtticusKuhn
2
Bug: lean-mlir does not support overflow flags bug Something isn't working
#470 opened Jul 16, 2024 by AtticusKuhn
1
Bug: lean-mlir does not fully support all syntax for llvm.icmp bug Something isn't working
#469 opened Jul 15, 2024 by AtticusKuhn
AliveStatements: a * allOnes w = -a
#447 opened Jul 10, 2024 by tobiasgrosser
@AnotherAlexHere
1
project: Floating point mechanization for arith potential-projects Projects that are well-scoped, suitable for writing a single paper or thesis on.
#394 opened Jun 8, 2024 by bollu
chore: mark div/rem instructions as .impure, with Id monad camera-ready-ltp
#383 opened Jun 6, 2024 by tobiasgrosser
@bollu
Split alive auto generated into individual files
#374 opened Jun 5, 2024 by goens
@goens
Why is simp! needed in simp_alive_meta
#349 opened May 27, 2024 by tobiasgrosser
Set the full paper into context camera-ready-ltp
#321 opened May 21, 2024 by tobiasgrosser
deanonymize tool name camera-ready-ltp
#320 opened May 21, 2024 by tobiasgrosser
ub-semantics & compare with alive camera-ready-ltp
#318 opened May 21, 2024 by tobiasgrosser
@alexkeizer
docker camera-ready-ltp
#317 opened May 21, 2024 by tobiasgrosser
@bollu
readme camera-ready-ltp
#316 opened May 21, 2024 by tobiasgrosser
@bollu
llvm: BitVec.xor_neg_one will enable ring_nf to be more powerful llvm
#308 opened May 15, 2024 by tobiasgrosser
@eurquhart1
3
llvm: BitVec.or_sub_xor_eq_and llvm
#307 opened May 15, 2024 by tobiasgrosser
Audit all warnings in the build.
#278 opened May 7, 2024 by bollu
Add typeclass for the refinement relation
#273 opened May 7, 2024 by bollu
ProTip! Type g i on any issue or pull request to go back to the issue listing page.