Issues

• feat/blase: Create Less Naive Generalizer Based on Multi-Width tactic

  opencompl/lean-mlir#1913 · Filter by author bollu opened on Dec 1, 2025
  1

• blase/cav26: make list of problems that used to work on single-width instcombine, but not on multi-width instcombine

  opencompl/lean-mlir#1905 · Filter by author bollu opened on Nov 25, 2025

• blase/cav26: make 10 examples for manasij/john

  opencompl/lean-mlir#1904 · Filter by author bollu opened on Nov 25, 2025

• Blase: bring back support for left shifts

  opencompl/lean-mlir#1831 · Filter by author ineol opened on Nov 5, 2025
  

• Bug: Evaluation.yml CI workflow jobs are not robust against cache evictions

  opencompl/lean-mlir#1765 · Filter by author alexkeizer opened on Oct 11, 2025

• LLVM Evaluation Tracking issue

  opencompl/lean-mlir#1757 · Filter by author alexkeizer opened on Oct 9, 2025

• Bug: the LLVM evaluation is broken

  needs-consensus
  opencompl/lean-mlir#1754 · Filter by author alexkeizer opened on Oct 8, 2025
  1

  

• SSA.elimValuation triggers a (kernel) application type mismatch error

  opencompl/lean-mlir#1748 · Filter by author alexkeizer opened on Oct 8, 2025
  

• tests: have a story for end-to-end tests that actually run the opt binary

  opencompl/lean-mlir#1730 · Filter by author alexkeizer opened on Oct 2, 2025
  1

  

• AliveStatements CI check in Testing, Tools, and auto-generated is Flaky

  opencompl/lean-mlir#1697 · Filter by author bollu opened on Sep 24, 2025

• Two directories with the same name up to case

  opencompl/lean-mlir#1684 · Filter by author ineol opened on Sep 22, 2025
  3

  

• Should we maintain our own CI runner for building Docker images (to reduce time spent shuffling caches around)

  needs-consensus
  opencompl/lean-mlir#1606 · Filter by author alexkeizer opened on Aug 27, 2025
  1

• check if parser use of importModules (loadExt := true) requires enableInitializersExecution

  opencompl/lean-mlir#1203 · Filter by author tobiasgrosser opened on May 11, 2025

• fix source operator in Handshake dialect

  opencompl/lean-mlir#1147 · Filter by author luisacicolini opened on Apr 27, 2025
  1

  

• bv_decide/symbolic: simplify Add with remainder expressions as operands

  opencompl/lean-mlir#934 · Filter by author tobiasgrosser opened on Dec 30, 2024
  

• div to shift

  opencompl/lean-mlir#825 · Filter by author tobiasgrosser opened on Nov 12, 2024
  

• slow proofs

  opencompl/lean-mlir#802 · Filter by author tobiasgrosser opened on Nov 7, 2024

• slow llvm benchmarks

  opencompl/lean-mlir#766 · Filter by author tobiasgrosser opened on Nov 3, 2024
  1

  

• MLIR bytecode reader/writer

  opencompl/lean-mlir#565 · Filter by author bollu opened on Aug 23, 2024

• Idea: Possible way to shorten the code of the MLIR Parser

  enhancement
  opencompl/lean-mlir#473 · Filter by author AtticusKuhn opened on Jul 17, 2024
  2

• Bug: lean-mlir does not fully support all syntax for llvm.icmp

  backlog
  opencompl/lean-mlir#469 · Filter by author AtticusKuhn opened on Jul 15, 2024

• AliveStatements: a * allOnes w = -a

  opencompl/lean-mlir#447 · Filter by author tobiasgrosser opened on Jul 10, 2024
  1

  

• project: Floating point mechanization for arith

  potential-projects
  opencompl/lean-mlir#394 · Filter by author bollu opened on Jun 8, 2024

• Split alive auto generated into individual files

  opencompl/lean-mlir#374 · Filter by author goens opened on Jun 5, 2024
  

• Why is simp! needed in simp_alive_meta

  opencompl/lean-mlir#349 · Filter by author tobiasgrosser opened on May 27, 2024