chore: remove Blase dependence from SSA

[ineol]

This should speed up compilation of core Lean MLIR, but the width-independent tactics will not be exercised by the AliveStatements.lean workload.

[tobiasgrosser]

Hi @ineol, did you measure the compile-time speedup on your machine? I am curious how much this actually is?

[tobiasgrosser]

I think it is great to decouple Blase and SSA. I find it useful to understand the project-wide vision. What is our vision respect to our evaluations?

[ineol]

I wanted to test this because on this run compiling Mathlib to C takes a long time in the opt build and I think it's because of Blase.

It seems there are other dependencies to mathlib

[bollu]

@tobiasgrosser : My vision wrt eval is that the only dependency is the goal states, which are provided as Lean files. I propose that we zip the files from a given lean-mlir version, and use these as the goal states for our Blase evaluation.

This allows us to have a stable evaluation baseline.

[bollu]

@ineol if we remove Blase from the lean-mlir root, then we will need to build Blase separately. The "correct" way to do this is to have a toplevel Monorepo lake project, which has lean-mlir, Blase, Medusa as dependencies. Then, a toplevel lake build will build al our projects.

[bollu]

Currently, lean-mlir plays the dual role of:

1. Being a separate project on its own for MLIR semantics, as well as
2. Being a toplevel "monorepo target".

[tobiasgrosser]

I wanted to test this because on this run compiling Mathlib to C takes a long time in the opt build and I think it's because of Blase.

It seems there are other dependencies to mathlib

I believe this issue is not due to SSA depending on Blase. The CI has already run lake build -R at this point and filled the cache accordingly. Everything else you see is because of additional dependencies that Blase lake build -R opt pulls in. One of the big ones is that lake build opt pulls in the RISC-V backend which is otherwise not built.

[tobiasgrosser]

I feel there are two issues here:

1. Why does the RISC-V backend pull in so much of mathlib?
2. Should lake build also build opt and/or the RISCV backend such that the cache works better?

[tobiasgrosser]

@tobiasgrosser : My vision wrt eval is that the only dependency is the goal states, which are provided as Lean files. I propose that we zip the files from a given lean-mlir version, and use these as the goal states for our Blase evaluation.

This allows us to have a stable evaluation baseline.

Refactoring the evaluation blase style is a conversation that needs higher bandwidth. We should consciously decide when to have this conversation. I feel this PR may not be the right place to open this conversation. Can you maybe open an issue that we can remember to have this conversation?

[ineol]

I feel there are two issues here:

1. Why does the RISC-V backend pull in so much of mathlib?

One issue is that SSA.Projects.InstCombine.ForLean uses Mathlib quite extensively, I looked for 20 minutes and proofs need to be rewritten. One possible way forward would be to make an effort to demathlibify the core modules of lean-MLIR

[tobiasgrosser]

SSA.Projects.InstCombine.ForLean

This is something generally useful. We can have two files, ForLean and ForMathlib and split according to these lines. Then we can incrementally push back mathlib.