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.

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.

When developping, sideloading on vscode.dev does not work because of security restrictions on webviews.

Support for web extension (thanks Emilio for the help!)

Remove server implementation from the extension.

• upgrade to last version of coreact-yade
• Proofs can be arbitrary complex (tactics can be separated by ".")

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