correctness proof of Codegen doesn't compile

[womeier]

The proof of correctness for Codegen doesn't compile with Coq 8.14.1 it is also not included in the CI build (has never been?)

for now it would help to know if there is a version of Coq, CertiCoq for which it is known to compile?

(I tried an older version with Coq 8.9 and had some issues installing the dependencies. )

thanks!

[mattam82]

@andrew-appel you might have some information I don't have here?

[spitters]

It appears that this was not spotted by the CI because it is not included in https://github.com/CertiCoq/certicoq/blob/master/theories/_CoqProject

[andrew-appel]

Over the next 10 months, @zoep will be working on correctness proofs of two CertiCoq phases, including codegen, so I expect this will get fixed by early 2024.