The extension should check that dependencies are installed #10

New issue

Closed

opened 2026-10-02 10:03:37 +02:00 by EatOreo · 0 comments

EatOreo commented

2026-10-02 10:03:37 +02:00

Owner

These at least include VsRocq and Clightgen, basically the same which are required by the Software Foundations: Verifiable C book.
When our extension is activated or first time it sees crocq annotations, it should check that these are installed with correct version, and that we are able to call them.
If something is missing it should give an error notification and link to an installation guide for the dependencies (could be just https://softwarefoundations.cis.upenn.edu/vc-current/Preface.html #Practicalities) and the extension should not start or go into a minimal mode.

These at least include VsRocq and Clightgen, basically the same which are required by the Software Foundations: Verifiable C book. When our extension is activated or first time it sees crocq annotations, it should check that these are installed with correct version, and that we are able to call them. If something is missing it should give an error notification and link to an installation guide for the dependencies (could be just https://softwarefoundations.cis.upenn.edu/vc-current/Preface.html #Practicalities) and the extension should not start or go into a minimal mode.