I am using the coq.extraction new stanza defined from dune 2.5. The compilation process of this stanza seems to request .aux files with the read-write permissions. Unfortunately, these are only created as read-only permission by the coq.theory stanza.

This might be a bug of Coq rather than Dune. I am putting it here because the bug never appeared before the coq.extraction stanza when I used ad-hoc rules like:

(rule
	(targets "extract.ml" "extract.mli")
	(deps "../theories/extraction.vo")
	(action (run cp "../theories/extract.ml" "../theories/extract.mli" "./")))

Expected Behavior

I would expect the compilation to go well, with the coq.extraction stanza using the files created during the coq.theory stanza.

Actual Behavior

I get the following output: Error: System error: "./theories/.common.aux: Permission denied" instead.
Running chmod +w on the said file, then dune build @all makes the compilation working.

Reproduction

I did a stand-alone repository to test the issue: https://github.com/Mbodin/dune-bug
I tried to make the repository as minimal as I could, but then the .aux files were not created. So I added some lemmas to trigger the issue.
I will send a PR with this same reproducing test very soon.
In the meantime, I can explain it in the context of this subrepository.

It is based on esy, a docker-like for OCaml. Basically, typing esy dune build @all calls dune in a context where all the packages constraints specified in the file package.json are met.
Typing esy dune build --verbose @all yields the output given in the gist below.
Typing chmod +w _build/default/theories/*.aux then esy dune build @all again makes the whole thing compile.

A run on Travis CI can be seen at: https://travis-ci.org/github/Mbodin/dune-bug/builds/681395518
The bug is not reproduced on Travis CI: there must be something about my specific system. I will keep investigating.

Specifications

• Version of dune (output of dune --version): 2.5.1
• Version of ocaml (output of ocamlc --version): 4.09.0
• Version of coq (output of coqcc --version): The Coq Proof Assistant, version 8.10.1 (April 2020)
• Operating system (distribution and version): Ubuntu 18.04.4 LTS, 64-bit.
• Result of uname -a: Linux ibekso 4.15.0-1079-oem Add clean subcommand #89-Ubuntu SMP Fri Mar 27 05:22:11 UTC 2020 x86_64 x86_64 x86_64 GNU/Linux

Additional information

• Link to gist with verbose output (run dune with the --verbose flag): https://gist.github.com/Mbodin/291a9c4e0d75cbac38f946b1dc3263b8