lean3 icon indicating copy to clipboard operation
lean3 copied to clipboard

--make should fail on failed dependencies

Open Kha opened this issue 9 years ago • 1 comments

It makes sense to keep going in server mode, but less so when building the stdlib.

Kha avatar Jan 19 '17 20:01 Kha

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).

Kha avatar Apr 19 '17 14:04 Kha