[Janno]

Description

dune does not clean symlinks in _build/install when the underlying files need to be rebuild. In various scenarios, this can lead to failures in unrelated theories when they scan all "installed" rocq theories. I think it only happens when rocq is in the workspace but I am not 100% sure. It definitely does happen when rocq is in the workspace and when it is used in cram tests that get executed at the same time that unrelated theories get their artifacts cleaned and rebuild (leaving broken symlinks momentarily).

The solution in this PR is to test for existence of the symlink target before adding it to the memo.

I have added a very hacky test that forces the issue to appear in a somewhat unrealistic way. Unfortunately, all my attempts to do anything with an up-to-date, real rocq in the workspace are failing for many different reasons and the one working setup that I have requires a bunch of custom patches that no longer work against rocq/master and the version of rocq used is not compatible with dune/main.

Related Issue and Motivation

The problem has been mentioned in #6015 (comment) and it is still a problem to this day.

This is probably related to #7580

Checklist

• Tests added, if applicable.
• Change log entry added for any user-facing changes.
• Documentation added for any user-facing changes.

[Alizter]

Could you split the reproduction case into a separate PR?

[Alizter]

@Janno I've merged the test, can you rebase?

[Alizter]

@Janno The issue mentioned in the PR description don't seem to be related. For instance, you are explicitly using fs_memo which is about tracking files outside the _build/ directory, yet the description mentions using the install staging area, which is part of that. Nothing in _build/ should go through fs_memo.

Could you explain why broken symliks in _build/install are affecting your builds at all? i.e. who is depending on the layout.

[Janno]

I am not sure the division is as strict as you say. As mentioned in the PR description, I have seen this problem pop up very frequently when running cram tests that use Rocq while Rocq itself is in the workspace. Maybe it's just because we need to use export ROCQPATH="$WORKSPACE/_build/install/default/lib/coq/user-contrib" in of our cram tests? I am not sure, to be honest.

There is also special logic in Rocq itself to figure out the paths of where libraries will end up when Rocq is in the workspace. Maybe there is some problem with absolute versus relative paths there that makes dune not realize that it is being pointed at files in the _build/install?

I believe that I have seen the problem pop up outside of cram tests as well but I do not remember in which context.

[rlepigre-skylabs-ai]

Maybe it's just because we need to use export ROCQPATH="$WORKSPACE/_build/install/default/lib/coq/user-contrib" in of our cram tests? I am not sure, to be honest.

We still have this in some of our tests, but I don't think this is necessary anymore. This might have to do with Rocq now trying to find these directories using a relative path from its own binary.