coq-community / coq-program-verification-template Goto Github PK

I'm a relatively new user in using both make and dune to manage by coq projects. With this program verification template it has enabled me to make use of the makefile setup to nicely maintain my library with make all generating the .vo, .vos, .vok files. My understanding is that .vo files generated from compiling is needed to if I want to call upon my library.

Here is my struggle, in my exploration of dune build to compile my .v files, only .vo files are generated and when I try to import my library (I use emacs) in another .v file, it says it is unable to locate library (also it seems that I need to prefix my original library name with the declared name in the dune file). It is also unclear how to map what I have in Makefile to its 'equivalent' in dune.

So my questions are:

• how would a Makefile be mapped to dune and dune-project?
• what is the difference in in the output when we run make all compared to dune build? It seems to be the output of the latter is a folder with many nested directories.
• how do I resolve the error which says it is unable to locate the library?

Many thanks

It seems like most of the CI time is spent on building the dependencies. Is there a way to tell the CI to cache the files for e.g. CompCert in this GitHub workflow setup, or would this require a docker image with CompCert precompiled?