Stream: Dune devs & users

Topic: Coq Load commands and dune build -p

Karl Palmskog (May 30 2020 at 13:22):

So is there any workaround for https://github.com/ocaml/dune/issues/3286 until it is solved more generally? I'm being bitten by this in a project in coq-community that I want to convert to dune, namely https://github.com/coq-community/buchberger.

Emilio Jesús Gallego Arias (May 30 2020 at 13:33):

I guess we should implemented the suggested feature, until coqdep can provide more information. For now the workaround I think is to make the loaded file buildable, you could maybe also use (copy_files .) as a temp hack?

Emilio Jesús Gallego Arias (May 30 2020 at 13:35):

To be clear, you could add a (copy_files mCoef) , not sure how robust is that tho.

Karl Palmskog (May 30 2020 at 13:38):

OK I'll give it a go and see what happens, thanks

Emilio Jesús Gallego Arias (May 30 2020 at 13:52):

Actually I have a branch fixing that in dune, but got some trouble due to rebases.

Karl Palmskog (May 30 2020 at 13:54):

not sure I'm doing it right, but (copy_files hCoefStructure) just gives the error:

Error: Cannot copy files onto themselves. The format is <dir>/<glob> where
<dir> is not the current directory.

Karl Palmskog (May 30 2020 at 13:55):

nice that there is a branch. A side-effect of this feature is that one can have legacy/attic .v files that are not compiled/checked as part of releases, etc., which I have seen that quite a lot of projects have (currently handled for coq_makefile by excluding those files from _CoqProject)

Emilio Jesús Gallego Arias (May 30 2020 at 16:56):

this you can already do with (modules) , right?

Emilio Jesús Gallego Arias (May 30 2020 at 16:56):

Indded to try to the copy files hack you should copy the file to a new one

Emilio Jesús Gallego Arias (May 30 2020 at 16:56):

likely wont' work tho...

Karl Palmskog (May 30 2020 at 16:59):

Emilio Jesús Gallego Arias said:

this you can already do with (modules) , right?

my understanding was that build hygiene will remove everything that's not a module? And if you don't want something to be compiled, you remove it from modules.

Emilio Jesús Gallego Arias (May 30 2020 at 18:29):

Oh I see what you mean; indeed these files are just documentation, so you should install them with a regular (install ...) stanza

Last updated: Apr 16 2024 at 04:02 UTC