Because we use a test runner that spawns child processes, these flags are not properly passed to the individual tests. Ideally lake would support multiple test drivers (see leanprover/lean4#10531 for example), but in the meantime we can easily pass the flags ourselves at least for CslibTests.