Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

dune frequently making full builds #1924

Closed
jdchristensen opened this issue Apr 19, 2024 · 9 comments
Closed

dune frequently making full builds #1924

jdchristensen opened this issue Apr 19, 2024 · 9 comments

Comments

@jdchristensen
Copy link
Collaborator

After a PR is merged to this repo, I pull the new commits into my local clone and run dune build. For some reason, most of the time every single .v file in the Coq-HoTT library gets rebuilt, starting with Basics/Utf8.v. I would of course normally expect that only the changed files and their dependencies get rebuilt. Note that I'm not running dune clean, so the previous .vo files are still present. (In addition, I use the dune cache, so even if the .vo files were not present, they should be found in the cache and replaced without coqc being run.)

This has been going on for a week or two I believe. I finally figured out a way to reproduce it.

# This is PR #1919:
git checkout d9ff10ee1
# Just build part, to save time:
dune build --cache=disabled _build/default/theories/Basics.vo
# This is current master, PR #1923:
git checkout c0f202e22
dune build --cache=disabled _build/default/theories/Basics.vo
# The above builds every file in Basics, including Utf8.v, which has no Requires lines.
# This shows that Basics/Datatypes.v is the only file that changed between these two:
git diff --stat d9ff10ee1 theories/Basics

In those steps, I disable the dune cache, but I'll emphasize that even with the cache enabled, it happens the first time I pull in new changes, but is not reproducible after that.

This is with dune 3.14.2 and Coq 8.19.1.

Any ideas?

@jdchristensen
Copy link
Collaborator Author

The first line in the build output is

      coqdep theories/.HoTT.theory.d 

Could it be that if any dependency in the library changes, then everything in the whole library is getting rebuilt? I don't think this happened before.

@Alizter
Copy link
Collaborator

Alizter commented Apr 20, 2024

I'm really sorry about this. This is a bug in Dune that has been around since 3.13. It hasn't been fixed yet. ocaml/dune#10149

My best advice would be to opam pin dune to 3.12. This has been annoying me a lot recently too. In fact, this is one of the reasons I didn't want to do #1910 yet.

@Alizter
Copy link
Collaborator

Alizter commented Apr 20, 2024

I've submitted a fix to dune, hopefully we can make progress on it. Once that is done, I'll try to push for it to be backported to 3.13-3.15 point releases.

Alternatively, you can directly pin my fix in opam.

@jdchristensen
Copy link
Collaborator Author

@Alizter Thanks! Glad to hear that it's understood and that a fix is on the way.

@jdchristensen
Copy link
Collaborator Author

The fix has been merged upstream. I'll close this after the next version of dune has been released and I have tested it.

@Alizter
Copy link
Collaborator

Alizter commented Apr 22, 2024

There is a 3.15.2 release planned for this to be backported to. So it should be available soon.

@Alizter
Copy link
Collaborator

Alizter commented Apr 23, 2024

3.15.2 has been released and here is the opam PR:

It will be available in the opam repository when that is merged.

@Alizter
Copy link
Collaborator

Alizter commented Apr 30, 2024

@jdchristensen Dune 3.15.2 is now available on opam.

@Alizter Alizter closed this as completed Apr 30, 2024
@jdchristensen
Copy link
Collaborator Author

I've upgraded to 3.15.2 and confirm that the problem is solved.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants