Patrick Massot
Patrick Massot
@bryphe Thank you for your explanations. I still don't understand how all this explain the development priorities. I can see 11 issues tagged `daily-editor-blocker`, for instance #2140 which makes Oni...
Thank you for the information. The dreams for v2 look really nice, but it's really frightening that they rely on first developing revery... Of course I would love to see...
I'm not sure I understand what you mean. Could you provide a bit more details? Anyway, I'm pretty sure it will be easier if you use my stalled PR #65...
Other sources of information: * the original discussion at https://github.com/leanprover/lean/pull/1227 * https://github.com/leanprover/lean-client-js/blob/master/lean-client-js-core/src/commands.ts (this is a more specific version of Sebastian's suggestion) * you can have a look at https://github.com/leanprover-community/format_lean/blob/master/src/format_lean/server.py which...
I guess you already know this, but just in case, it seems that https://documentation.divio.com/ has interesting ideas about splitting documentation. Maybe it could be one source of inspiration.
bors merge
I'm sorry Sébastien, I didn't see your comment about `sqrt` before merging.
> would it be possible for MathJax to adopt xyjax and maintain it officially? To me it would be feel very strange to see a lot of efforts going into...
Is there any progress on this issue? It seems rather important to me, especially because of #157 which prevents bypassing data tables by repeated use of the same Given step....