Stream: Coq Universe

Topic: Adding VST to coq-universe

view this post on Zulip Roland Coeurjoly Lechuga (Jun 06 2022 at 20:09):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 20:29):

Hi @Roland Coeurjoly , what does your dune file say?

view this post on Zulip Karl Palmskog (Jun 08 2022 at 16:46):

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.

view this post on Zulip Rudi Grinberg (Jun 08 2022 at 17:07):

Indeed. It seems like this project has a bunch of dependencies. So it might make sense to port those to dune first.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 08 2022 at 20:58):

I don't see any special difficult building VST

view this post on Zulip Michael Soegtrop (Jun 09 2022 at 09:11):

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).

view this post on Zulip Michael Soegtrop (Jun 09 2022 at 09:13):

Another problem is that the current makefile uses shell scripts to generate file lists.

view this post on Zulip Michael Soegtrop (Jun 09 2022 at 09:13):

Otherwise I am not aware of unusual complications.

view this post on Zulip Rudi Grinberg (Jun 09 2022 at 14:04):

Is there a port of compcert to dune?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2022 at 19:28):

@Rudi Grinberg it already is in the universe

Last updated: Jun 10 2023 at 06:31 UTC