I'm browsing the FLOC program, and noticed that isabelle is using an open version of vscode, which seems to give them some advances. Does anyone know what is going on there, and whether it would be useful for Coq too?
This is a technology preview of the forthcoming release Isabelle2022, which is anticipated for October 2022. It will include a fully integrated Isabelle/VSCode Prover IDE based on a bundled distribution of VSCodium, which is an open-source branch of Microsoft's VSCode project. VSCode is based on Electron, which is a desktop application framework with Chromium browser and Node.js environment. Careful patching and repackaging of VSCodium exposes Electron and Node.js for other Isabelle applications. Thus we gain access to high-end web technologies for Isabelle/PIDE browsing and editing, for example a cross-platform PDF viewer with custom URLs for Isabelle/PIDE commands.
@Bas Spitters Coq supports VSCodium, see my PR here which notes this in the README: https://github.com/coq-community/vscoq/pull/296
but we go a different route than Isabelle by doing a more shallow VS Code integration as a regular extension (this is what VsCoq is)
OK. So, that does not give access to the electron part they are using.
right, there is no integration for Coq with something like Electron or Node.js, except what one might do through jsCoq
I think VS Code / VSCodium already give access to a pretty powerful HTML / Typescript API that could be used for advanced features inspired by jsCoq. But that does not look very close to me on the roadmap (the VsCoq roadmap is here BTW: https://github.com/coq-community/vscoq/wiki/VsCoq-1.0-Roadmap).
Last updated: Jun 04 2023 at 23:30 UTC