Bryan Gin-ge Chen

(The GitHub actions queue is backed up, so I canceled the build of 375aa86.)

@Pazzaz gentle ping. Feel free to ask here or on Zulip if you need help with the suggestion above.

I hadn't. I might be misunderstanding your suggestion, but our workflow only runs this one action once every 15 minutes (and we're even using a GitHub token from an account...

Hmm, perhaps I wasn't being clear. What I had in mind was more along the lines of adding a (user-specified?) pause after each iteration of [this for loop](https://github.com/eps1lon/actions-label-merge-conflict/blob/cf6c16f40085290c42f2f4a61007a8439e9001a6/sources/main.ts#L156). That way...

> > So I think before feeding the docstring to markdown processor, we need to filter all LaTeX formulas > > This is not a sensible approach; the markdown parser...

Yes, if switching the processor works that would be easiest! By the way, if you need some examples to test LaTeX embedded in markdown, I put together [this markdown file](https://github.com/leanprover-community/doc-gen/blob/0ab85f2ad359ecb52311f31bbf61ea9cf60ffb4c/test/latex.md)...

There is some more documentation here which may be helpful: https://github.com/leanprover-community/lean/blob/master/doc/widget_server.md

The relevant part of the code starts here, if anyone wants to take a crack at it: https://github.com/leanprover/vscode-lean/blob/master/src/tacticsuggestions.ts#L79

So this is trickier than I thought it would be. The error messages are provided by "Diagnostics" in `diagnostics.ts` and the docstrings / types, etc. are provided by the "HoverProvider"...

First, thanks for thinking about the extension! There are certainly lots of improvements that could be made; I think many of the UX decisions up to now have been governed...