better mathlib linter integration

[bryangingechen]

The linter provided by mathlib is now fairly sophisticated. We should see if we can better integrate it with the extension. One idea is to make #lint output something which vscode-lean can parse to create diagnostics (warning underlines at the position of the lint failure).