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.

Sign up for GitHub

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

Jump to bottom

Running "dune coq top --no-build ..." tries to take the lock #7671

Closed
rlepigre opened this issue May 3, 2023 · 5 comments · Fixed by #10547
Closed

Running "dune coq top --no-build ..." tries to take the lock #7671

rlepigre opened this issue May 3, 2023 · 5 comments · Fixed by #10547
Labels
coq

Comments

@rlepigre
Copy link
Contributor

rlepigre commented May 3, 2023

Expected Behavior

Running dune coq top --no-build ... should not fail if there is a concurrently running dune build command.

Actual Behavior

You get: Error: A running dune instance has locked the build directory.

Is there anything we can do to fix this? Or does dune coq top --no-build ... possibly need to build stuff?
@Alizter
Copy link
Collaborator

Alizter commented May 3, 2023 •
edited

@rlepigre I'll look into it. We might be running coqdep causing the build to lock.

I'll also write a cram so that we can preserve this behaviour.

@Alizter Alizter added the coq label May 3, 2023
@rlepigre
Copy link
Contributor Author

rlepigre commented May 3, 2024

@Alizter did you ever try looking into this, or did you just not get the time?

@Alizter
Copy link
Collaborator

Alizter commented May 3, 2024

@rlepigre I remember investigating but I didn't find anything conclusive. The nobuuild was set up correctly as far as I could tell, but something was causing the global lock to trigger.

@rlepigre
Copy link
Contributor Author

rlepigre commented May 3, 2024

OK cool. Now that I think about it, is it possible that this got fixed by #10446?

@Alizter
Copy link
Collaborator

Alizter commented May 3, 2024

@rlepigre I think it's unlikely, but I haven't checked. I think this issue was around before that bug was introduced.

@lzy0505 lzy0505 mentioned this issue May 17, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
coq
Projects
Coq + Dune
Status: Done
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: don't take build lock for coq top --no-build lzy0505/dune
2 participants
@rlepigre @Alizter