coreact-yade READMEThis 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. Collaborating on the same diagramThe 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). Mechanisation featuresSee https://github.com/amblafont/vscode-yade-example for an example of use.
Experimental versionThis 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-experimental/index.html can alternatively be used using the "Launch experimental YADE" command. RequirementsYou need coq-lsp vscode extension. Extension SettingsNone. Known IssuesThe experimental version of YADE does not work with vscode.dev because of https://github.com/microsoft/vscode/issues/72900. Release Notes0.0.7Integrated YADE server. 0.0.6Web extension capabilities. 0.0.5No need for the desktop version of coreact-yade: it directly runs in a vscode tab. Initial releaseInitial release of the coreact-yade extension "customEditors": [ { "viewType": "coreactyade.editor", "displayName": "YADE Editor", "selector": [ { "filenamePattern": ".yade" }, { "filenamePattern": ".json" } ], "priority": "option" } ], |