leanprover
Too many sorry warnings cause printing to stop
Related to #47.
example : true := sorry
example : true := sorry
...
example : true := sorry
#print nat
There are 250 lines of example : true there. The last line gets an error instead of a warning, which says
declaration '[anonymous]' uses sorry
Not showing 1 further errors and warnings.
and the final #print line produces no output. I haven't been able to find where the error/warning limit of 250 is coming from, but I don't think lean is doing it - if I run lean sorry_overflow.lean I get all the sorry warnings, plus the #print line.
This is a limitation in VSCode: https://github.com/Microsoft/vscode/blob/master/src/vs/workbench/api/node/extHostDiagnostics.ts#L19
If we get above a limit of 250 errors in one file, we could still add decorations instead of diagnostics. But then we loose a lot of features from vscode.
My suggestion is to decorate all sorrys in the file instead of adding them as diagnostics, except possibly the first one. Sorry should not be on the same level as a standard info message, since there is nothing the user will want to do about it most of the time. (Possibly a setting should be made for this, since if you are searching for sorrys and want to see them all, then it might be better to have the current behavior.) What does this "decoration" entail?
We could also handle the cutoff ourselves, by collecting the list of all diagnostics in the file to be sent to VSCode, and remove any sorry warnings until the total drops below 250 or there are no sorrys left.
This seems to have been addressed in VScode: https://github.com/Microsoft/vscode/commit/ea09391fd86584614d2763214e46034e79f63588
