aux files set-up as read-only

[Mbodin]

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

[ejgallego]

Yup, sorry. This is a problem related to read-only mode of build objects that I did not foresee when I chose to ignore .aux files as targets; (I don't consider them very useful and I plan to replace them soon)

Unfortunately Coq doesn't have a flag to remove aux file generation, I will add such flag for 8.11.2 / 8.12, meanwhile let me think what the best way to fix this in Dune is.

[ejgallego]

Hi @Mbodin , I cannot reproduce using a plain dune build @all , can you indeed reproduce this bug without esy?

I was a bit puzzled as even .aux files are not considered as targets by dune there should not be such problems.

[ejgallego]

Note that I'm using Coq 8.11 , this could be very well Coq-specific, can you reproduce with 8.11?

[Mbodin]

Using https://github.com/Mbodin/dune-bug and ignoring the esy part, I could indeed reproduce the bug (Coq and dune installed through Opam):

$ coqc --version
The Coq Proof Assistant, version 8.10.1 (January 2020)
compiled on Jan 8 2020 11:29:37 with OCaml 4.09.0
$ dune --version
2.5.1
$ dune build @all
        coqc theories/common.vo (exit 1)
(cd _build/default && /home/martin/.opam/4.09.0/bin/coqc -R theories Bug_Coq theories/common.v)
Error: System error: "./theories/.common.aux: Permission denied"

I also get the error with Coq 8.11.

Given that both Travis and you are getting the same positive results, this must be an issue with my own configuration.
I have for instance this line in my ~/.bashrc: alias mv='mv -n'. I find it useful to prevent unwanted removal of files. Do you think that it could have messed with Dune’s behaviour?

[ejgallego]

Thanks for the pointers @Mbodin , maybe you have some strange umask ? I don't think mv should have any effect at all on this, but you never know.

The problem seems to be that your _build directory gets some undesired permissions, I recall this was the case due to the cache. What do you have in config/dune/config ?

Even with the cache enabled I cannot reproduce the problem.

It would be helpful if you could post (from a clean build tree):

• The full contents of _build/log
• The output of ls -al _build/default

[Mbodin]

Sure. Here are the information.

• umask returns 0022
• I couldn’t see any ~/.config/dune/config. I installed Dune through Opam: should I look at a different place to get its configuration? I searched in ~/.opam/4.07.0/ and didn’t find much apart ~/.opam/4.07.0/lib/dune/ with three files: dune-package, META, and opam… but doesn’t look like this.
• here is the logs and the content of the different folders during the compilation: https://gist.github.com/Mbodin/63997dd2438cd9cd7b914a29399903c3

I’m quite surprised by the produced logs: it seems that the issue came with the compilation of the files producing the .aux files, not the extraction itself. I admit being a little lost there :-\

[ejgallego]

Thanks for the extra info @Mbodin ; just to be clear, does the problem happen on a fresh compilation, that is to say, after dune clean, or do you see it only when invoking dune in an already built tree?

[Mbodin]

I didn’t do dune clean: I just removed the _build folder. Let me see if I get a difference result after a dune clean ☺

[Mbodin]

Using a dune clean instead: https://gist.github.com/Mbodin/f89a68c884fa9db30aaa70c0fafec30f
As far as I can tell, the results look similar.

[ejgallego]

Thanks @Mbodin , what is the output of

(cd _build/default && /home/martin/.opam/4.07.0/bin/coqc -debug -R theories Bug_Coq theories/common.v)

?

[Mbodin]

Thank you for your time ☺ Here it is:

$ dune build @all
        coqc theories/common.vo (exit 1)
(cd _build/default && /home/martin/.opam/4.07.0/bin/coqc -R theories Bug_Coq theories/common.v)
Error: System error: "./theories/.common.aux: Permission denied"

$ (cd _build/default && /home/martin/.opam/4.07.0/bin/coqc -debug -R theories Bug_Coq theories/common.v)
Error:
System error: "./theories/.common.aux: Permission denied"
frame @ file "toplevel/coqc.ml", line 67, characters 4-25
frame @ file "toplevel/coqc.ml", line 45, characters 2-81
frame @ file "list.ml", line 106, characters 12-15
frame @ file "toplevel/ccompile.ml", line 214, characters 2-39
frame @ file "toplevel/ccompile.ml", line 138, characters 16-113
frame @ file "stdlib.ml", line 321, characters 2-74
frame @ file "stdlib.ml", line 316, characters 29-55

[ejgallego]

Thanks to you @Mbodin ; that is quite bizarre, in particular as the file seems to be there. If you do

(cd _build/default && rm -f theories/.common.aux && /home/martin/.opam/4.07.0/bin/coqc -R theories Bug_Coq theories/common.v)

do you still get the same?

[ejgallego]

At this point something like this may be needed:

(cd _build/default && strace -o coqc_strace_out -- /home/martin/.opam/4.07.0/bin/coqc -R theories Bug_Coq theories/common.v)

please paste the contents of the file _build/default/coqc_strace_out

[Mbodin]

Indeed, removing the aux file seems to make Coq run without issue. I fully agree that this is odd.

$ dune build @all
        coqc theories/common.vo (exit 1)
(cd _build/default && /home/martin/.opam/4.07.0/bin/coqc -R theories Bug_Coq theories/common.v)
Error: System error: "./theories/.common.aux: Permission denied"

$ (cd _build/default && rm -f theories/.common.aux && /home/martin/.opam/4.07.0/bin/coqc -R theories Bug_Coq theories/common.v)
$ ls -la _build/default/theories/
total 56
drwxr-xr-x 2 martin martin  4096 May  4 14:48 .
drwxr-xr-x 5 martin martin  4096 May  4 14:48 ..
-rw-r--r-- 1 martin martin   272 May  4 14:48 .common.aux
-rw-r--r-- 1 martin martin  1038 May  4 14:48 common.glob
-r--r--r-- 1 martin martin   306 May  4 14:48 common.v
-r--r--r-- 1 martin martin    94 May  4 14:48 common.v.d
-rw-r--r-- 1 martin martin 16738 May  4 14:48 common.vo
-rw-r--r-- 1 martin martin     0 May  4 14:48 common.vok
-rw-r--r-- 1 martin martin     0 May  4 14:48 common.vos
-r--r--r-- 1 martin martin    50 May  4 14:48 dune
-r--r--r-- 1 martin martin   213 May  4 14:48 value.v
-r--r--r-- 1 martin martin   110 May  4 14:48 value.v.d
$ dune build @all
        coqc theories/common.vo (exit 1)
(cd _build/default && /home/martin/.opam/4.07.0/bin/coqc -R theories Bug_Coq theories/common.v)
Error: System error: "./theories/.common.aux: Permission denied"

$ dune clean
$ dune build @all
        coqc theories/common.vo (exit 1)
(cd _build/default && /home/martin/.opam/4.07.0/bin/coqc -R theories Bug_Coq theories/common.v)
Error: System error: "./theories/.common.aux: Permission denied"

$ (cd _build/default && strace -o coqc_strace_out -- /home/martin/.opam/4.07.0/bin/coqc -R theories Bug_Coq theories/common.v)
Error: System error: "./theories/.common.aux: Permission denied"

The content of _build/default/coqc_strace_out is quite large: https://gist.github.com/Mbodin/ad0c48d971bbf4d284e4856380f887e8

[ejgallego]

I'm afraid I'm totally lost on why the aux file is already there when you do dune clean && dune build @all , AFAICS the file should be created on the call to coqc, however it is already there and the log doesn't explain why.

I cannot reproduce :S , only think I could image is that for some reason coqc is called twice?

[ejgallego]

If you remove the extraction stanza does that still happen?

[Mbodin]

Maybe there is something else wrong with my system :-\ The fact that the issue is not reproducible elsewhere is very frustrating ☹ (This also makes this issue less important, I imagine.)

I just commented-out the extraction stanza, and the issue is still happening, including after a dune clean. (I was first surprised as I only saw this issue since I added this stanza, but then I realised that I updated Dune to version 2.5 at the same time.)

[picojulien]

I have the same problem on a project here.
I'm struggling to produce a reasonably small example and I cannot reproduce the error from https://github.com/Mbodin/dune-bug .

Some context: I'm using OCaml 4.07.1, dune 2.5.1, coq 8.10.1 in an opam switch.

I'll try to come back with a minimum example as soon as possible.

[picojulien]

Oups, I just found that I had a remaining .my_failing_file.aux file in the source directory.
The file is copied by dune into the build directory.
dune should probably complain about it like it does when you have OCaml object files in your sources.

[ejgallego]

Oups, I just found that I had a remaining .my_failing_file.aux file in the source directory.
The file is copied by dune into the build directory.
dune should probably complain about it like it does when you have OCaml object files in your sources.

Thanks @picojulien , that would explain a lot! Good catch!

As of today dune doesn't consider .aux files as targets as they are mainly useful for async compilation support; I will prepare a fix to consider them, once that happens Dune will complain correctly.

[ejgallego]

@Mbodin would that explain some of your problems?

[Mbodin]

It does! I did not notice it before, but I do have a .common.aux file in theory in the source. I think that it has been created by Proof General. Anyway, removing the file made the issue disappear. ☺ Thanks @picojulien!

I’m thus closing this issue. Do you think that a warning message should be displayed when such aux files appear in the source? This may prevent other people from reopening this issue 😅​

[ejgallego]

This is indeed a real issue, Dune should be aware of aux files as targets and thus error if such files are present.

[ejgallego]

Something I don't fully grasp is why .aux files are copied to the build dir, nothing should be depending on them; @rgrinberg , you have an idea of why this is like that?

[rgrinberg]

Possible some stray glob dependency? If there's no dependency on .aux anywhere and it's still being copied then we should def. fix this bug in dune.

[rgrinberg]

I misunderstood the issue. #3721 adds .aux files as targets.