I would like to add VST to coq-universe.
I think it fulfill the requirements as it uses dune and it is in Coq's CI.
I have added it as a submodule in my fork but it doesn´t compile.
I get errors about libraries.
File "./VST/InteractionTrees/theories/Basics/Basics.v", line 12, characters 0-188:
Error: Cannot find a physical path bound to logical path
Structures.Functor with prefix ExtLib.
And the same for Paco.
I see that coq-ext-lib and paco are submodules inside VST.
Hi @Roland Coeurjoly , what does your dune file say?
the proper way to include VST is to first get a Dune-based build accepted by VST devs. VST is really complicated to build, so this may take considerable effort.
Indeed. It seems like this project has a bunch of dependencies. So it might make sense to port those to dune first.
I don't see any special difficult building VST
One problem with VST is that it has (and requires) various options to include CompCert. E.g. it also has a bundled CompCert which is used in phases a synchronized VST-CompCert feature is developed. Users might also want to use some locally compiled CompCert or a non standard installed CompCert (say an ARM cross CompCert on an Intel machine).
The makefiles should ensure that the architecture parameterization of VST matches the one of the CompCert used. This is usually done by reading the architecture parameter files from the used CompCert, but in case a local CompCert is used, both are set together.
Btw.: I did a rework of the VST make files ~ 2 years back to integrate it better with Coq Patform and its variant mechanism (it allows to install CompCert for different architectures in parallel).
Another problem is that the current makefile uses shell scripts to generate file lists.
Otherwise I am not aware of unusual complications.
Is there a port of compcert to dune?
@Rudi Grinberg it already is in the universe
Last updated: Feb 06 2023 at 05:03 UTC