notify when model.v is invalid

EatOreo commented

2026-10-16 10:18:45 +02:00

Owner

This should be in v0.1.
If the user changes the c code, the model generated by clightgen is no longer valid and thus crocq annotations should be invalidated until model is regenerated. We can show that the model is invalidated by diagnostics/greying out annotations (decide on this) and a code lens prompting the user to run "Create Rocq model" command. In this way it will always be required that the model is generated on every new session. First step is to check whether clightgen has anything useful for this, else invalidate every time .c is changed/saved.

An idea for a better solution that might not be v0.1:
We require a special crocq annotation at the very top of every C file, else Crocq will not analyse it.
This is useful because every .c will have one corresponding .v model and we can use this annotation instead of hasAnnotationMarker() in src/dependencies/manager.ts (so the extension doesnt have to scan every C file not containing an annotation to the end).
This annotation could then contain a hash of the C program (minus all comments and annotations), which we update with a text edit on the "Create Rocq model" command. This can verify that the current model is for the current c code and if not it is invalid. Additionally the user could optionally specify if the model should have a different file path than the default.
This change might also mean reworking our annotation structs a bit so it could be an issue in itself if we start by just solving the first paragraph.

This should be in v0.1. If the user changes the c code, the model generated by clightgen is no longer valid and thus crocq annotations should be invalidated until model is regenerated. We can show that the model is invalidated by diagnostics/greying out annotations (decide on this) and a code lens prompting the user to run "Create Rocq model" command. In this way it will always be required that the model is generated on every new session. First step is to check whether clightgen has anything useful for this, else invalidate every time .c is changed/saved. An idea for a better solution that might not be v0.1: We require a special crocq annotation at the very top of every C file, else Crocq will not analyse it. This is useful because every .c will have one corresponding .v model and we can use this annotation instead of hasAnnotationMarker() in src/dependencies/manager.ts (so the extension doesnt have to scan every C file not containing an annotation to the end). This annotation could then contain a hash of the C program (minus all comments and annotations), which we update with a text edit on the "Create Rocq model" command. This can verify that the current model is for the current c code and if not it is invalid. Additionally the user could optionally specify if the model should have a different file path than the default. This change might also mean reworking our annotation structs a bit so it could be an issue in itself if we start by just solving the first paragraph.

EatOreo added the

priority!

label

2026-10-16 10:18:45 +02:00

EatOreo commented

2026-10-16 10:24:14 +02:00

Author

Owner