Bas Spitters (Aug 10 2022 at 08:03): Bas Spitters (Aug 10 2022 at 08:03):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?
https://easychair.org/smart-program/FLoC2022/Isabelle-2022-08-11.html#talk:197555
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.
Karl Palmskog (Aug 10 2022 at 08:36):@Bas Spitters Coq supports VSCodium, see my PR here which notes this in the README: https://github.com/coq-community/vscoq/pull/296
Karl Palmskog (Aug 10 2022 at 08:40):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)
Bas Spitters (Aug 10 2022 at 08:56):OK. So, that does not give access to the electron part they are using.
Karl Palmskog (Aug 10 2022 at 08:58):right, there is no integration for Coq with something like Electron or Node.js, except what one might do through jsCoq
Théo Zimmermann (Aug 10 2022 at 12:30):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: Apr 16 2024 at 06:01 UTC