when a new model file is generated the proof file needs to be reloaded to realize it #98

New issue

Open

opened 2026-10-30 13:32:50 +01:00 by EatOreo · 0 comments

EatOreo commented

2026-10-30 13:32:50 +01:00

Owner

reproduce:
for instance with the run.c example you can first interpret the proof. Then change one of the arguments of the add(1, 2) line and click on the "model is stale" code lens to generate the new model. The proof should no longer be valid, but nothing changes in the proof context yet. VsRocq has not realized that the model has changed. If you reload the window and interpret the proof doesnt check out.
How do we solve this reliably? force depending proof files to reload on generating model? changes to VsRocq (is this the issue? https://github.com/rocq-prover/vsrocq/issues/768)?

reproduce: for instance with the run.c example you can first interpret the proof. Then change one of the arguments of the add(1, 2) line and click on the "model is stale" code lens to generate the new model. The proof should no longer be valid, but nothing changes in the proof context yet. VsRocq has not realized that the model has changed. If you reload the window and interpret the proof doesnt check out. How do we solve this reliably? force depending proof files to reload on generating model? changes to VsRocq (is this the issue? https://github.com/rocq-prover/vsrocq/issues/768)?

EatOreo added this to the Release roadmap project

2026-10-30 13:58:01 +01:00

EatOreo added the

bug

label

2026-10-30 13:59:29 +01:00