CertiCoq dev with Coq 8.19

[liyishuai]

No description provided.

[SkySkimmer]

Seems broken

# coqc -R ./ CertiCoq.Benchmarks -R lib CertiCoq.Benchmarks.lib tests.v
# File "./tests.v", line 8, characters 0-45:
# Error: Cannot find a physical path bound to logical path
# CertiCoq with prefix CertiCoq.Plugin.

[liyishuai]

I was copying the OPAM file in the master branch: https://github.com/CertiCoq/certicoq/blob/master/coq-certicoq.opam

@mattam82 Which OCaml version should we run CertiCoq with?

[mattam82]

We use a docker image on our CI:

MetaCoq 1.3.2 and Coq 8.19 images use OCaml 4.14 and include equations-1.3, compcert-3.13.1, ext-lib-0.12.1 and clang-14.

dev images use OCaml 4.14 and include equations-1.3, compcert-3.13.1, ext-lib-0.12.1 and clang-14.

[mattam82]

with-test targets won't work. They assume an already installed CertiCoq iirc.