lean3
lean3 copied to clipboard
--make should fail on failed dependencies
It makes sense to keep going in server mode, but less so when building the stdlib.
To make a concrete proposal: I believe that in non-interactive usage, we should not try to compile dependent modules after a non-recoverable error (i.e. one that most likely leads to a missing definition).