This extension runs the Coreact YADE editor in a vscode tab (webview) to help mechanising commutations of categorical diagrams with the Coq proof assistant. It builds upon the coq-lsp extension.
The Live Share extension allows multiple users to collaborate on the same workspace.
The present extension enables collaboration on the same diagram during live sharing. First launch the editor (using the "Launch YADE" command), then join or create a liveshare session. If you are hosting the session, the extension will automatically launch the YADE server and prompt you to share it on the port 8080 (moreover, the editor will automatically connect to the server).
See https://github.com/amblafont/vscode-yade-example for an example of use.
- Displays inline diagrams and equations between composition of morphisms as diagrams
- Builds diagrammatic proofs interactively with Coq using the vscode command "Complete diagram"
This extension is shipped with a version of the editor whose mechanisation features have been tested. The last version of the editor available at https://amblafont.github.io/graph-editor/index.html can alternatively be used using the "Launch experimental YADE" command.
You need coq-lsp vscode extension.
None.
The experimental version of YADE does not work with vscode.dev because of microsoft/vscode#72900.
Integrated YADE server.
Web extension capabilities.
No need for the desktop version of coreact-yade: it directly runs in a vscode tab.
Initial release of the coreact-yade extension