Currently the OPAM packages coq-vst and coq-vst-zlist are conflicting, because they are installed to the same directory. So I added a flag ZLIST (similar to COMPCERT) in Makefile. ZLIST=bundled by default, so for VST developers who don't explicitly set it, the source code in the repo will be used. The other possible value is ZLIST=platform, which means to use zlist from the installed library (e.g. OPAM). When installing VST from OPAM, it needs to depend on zlist and use the flag ZLIST=platform. I edited OPAM files accordingly. Also notice that, the OPAM files in the repo have "coq-vst-zlist" {= "dev"}, because they are the dev version as well. For released versions, we should depend on the same version number of zlist as VST.
Currently the OPAM packages
coq-vstandcoq-vst-zlistare conflicting, because they are installed to the same directory. So I added a flagZLIST(similar toCOMPCERT) in Makefile.ZLIST=bundledby default, so for VST developers who don't explicitly set it, the source code in the repo will be used. The other possible value isZLIST=platform, which means to usezlistfrom the installed library (e.g. OPAM). When installing VST from OPAM, it needs to depend onzlistand use the flagZLIST=platform. I edited OPAM files accordingly. Also notice that, the OPAM files in the repo have"coq-vst-zlist" {= "dev"}, because they are thedevversion as well. For released versions, we should depend on the same version number of zlist as VST.I tested on Coq 8.15.2.