Software Foundations vol 5 - Verifiable C expects VST 2.10 but Coq platform has VST 2.9

[ghulette]

(Not sure if this is the right place to file this, please redirect as appropriate. I cannot find a GitHub repo for Software Foundations itself.)

The code for Software Foundations: Verifiable C (Version 1.2.1 (2022-08-08 21:24, Coq 8.15)) doesn't seem to build under the most recent version of the Coq platform (2022.04.1, Coq 8.15 and VST 2.9). The build process complains that it expects VST 2.10. This contradicts the build instructions found in the preface which mention only VST 2.9.

Perhaps rashly, I tried running opam upgrade in my Coq platform switch and got VST 2.10. Now running make in vc yields the following puzzling error message: Error: Cannot find a physical path bound to logical path VST.floyd.proofauto.

[yiyuan-cao]

Perhaps rashly, I tried running opam upgrade in my Coq platform switch and got VST 2.10. Now running make in vc yields the following puzzling error message: Error: Cannot find a physical path bound to logical path VST.floyd.proofauto.

Same here!