The CI script includes some basic caching which should prevent it doing any work if the lean files don't change.
Note that CI fails, because three of the lean files contain either type errors or invalid syntax; I would argue that CI that fails is better than no CI at all, and the fixes can come later.
The
globs
field makeslake build
work.The CI script includes some basic caching which should prevent it doing any work if the lean files don't change.
Note that CI fails, because three of the lean files contain either type errors or invalid syntax; I would argue that CI that fails is better than no CI at all, and the fixes can come later.