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

[rlepigre]

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]

@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.

[rlepigre]

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

[Alizter]

@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]

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

[Alizter]

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