Description
Please remove the "Even Better TOML" dependency or make it optional, to improve the supply chain security of the vscode-lean4 extension.
Context
See tamasfe/taplo#715. The extension seems to be in a state where we cannot expect it to be maintained in a secure manner. Indeed, the extension was last updated 12/20/2024. From the thread I linked to, it is likely that any future updates are likely to come from people other than the author.
In #706 it was also noted that the extension is absolutely huge. Thus the attack surface of the extension is also large.
A gigantic attack surface with no maintainers is a terrible combination.
Lean 4 itself is foundational in the supply chain security of several projects that intend to be critical infrastructure for other tools (e.g. security, privacy, cryptography components), and the VS Code extension is the primary recommended interface to Lean 4. Thus it is critical that the Lean 4 VS Code extension also have a good supply chain security story.
In #706 it was suggested that the code completion (etc.) support for lakefiles is critical. IMO it is not so critical to justify complicating the security story for the project.
Description
Please remove the "Even Better TOML" dependency or make it optional, to improve the supply chain security of the vscode-lean4 extension.
Context
See tamasfe/taplo#715. The extension seems to be in a state where we cannot expect it to be maintained in a secure manner. Indeed, the extension was last updated 12/20/2024. From the thread I linked to, it is likely that any future updates are likely to come from people other than the author.
In #706 it was also noted that the extension is absolutely huge. Thus the attack surface of the extension is also large.
A gigantic attack surface with no maintainers is a terrible combination.
Lean 4 itself is foundational in the supply chain security of several projects that intend to be critical infrastructure for other tools (e.g. security, privacy, cryptography components), and the VS Code extension is the primary recommended interface to Lean 4. Thus it is critical that the Lean 4 VS Code extension also have a good supply chain security story.
In #706 it was suggested that the code completion (etc.) support for lakefiles is critical. IMO it is not so critical to justify complicating the security story for the project.