Skip to content

Conversation

Alasdair
Copy link
Collaborator

Add a SAIL_MODULES variable to the CMakeLists file that allows specifying a smaller set of modules, useful to constraint the Lean build to be something like RV64IM or similar, when that's all we need for some use cases. For example:

 cmake -S . -B build -DCMAKE_BUILD_TYPE=RelWithDebInfo -DSAIL_MODULES="I;M;riscv_termination;riscv_main"

Not sure if this is the best way to do this with CMake, or if we want to make it work more broadly other than just for Lean.

Copy link

Test Results

2 101 tests  ±0   2 101 ✅ ±0   15m 56s ⏱️ -2s
    1 suites ±0       0 💤 ±0 
    1 files   ±0       0 ❌ ±0 

Results for commit 57d539f. ± Comparison against base commit 6ee85c5.

@Timmmm
Copy link
Collaborator

Timmmm commented Aug 20, 2025

I think either this should apply everywhere we use --all-modules, or It should be called something like LEAN_SAIL_MODULES? Otherwise LGTM.

@jordancarlin
Copy link
Collaborator

It would be good to add a test build of the model with a subset of the modules to CI. If that doesn’t happen in this PR, let’s open an issue so it doesn’t get forgotten.

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.

3 participants