[K-Bug] Kompile silently allows files with the same name to exist in multiple include directories

[juliankuners]

What component is the issue in?

Front-End

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

v7.1.276

Operating System

Linux

K Definitions (If Possible)

See runtimeverification/wasm-semantics#732 and runtimeverification/skribe@9a10619

Steps to Reproduce

The include directories are sorted prior to being passed to kompile in the pyk library. Due to the different nix build directory on MacOS compared to Linux (/private/tmp/nix-build-skribe-dirty.drv-1/source/kdist-fb9c790/... <-> /build/source/kdist-5b094bf/...), the skribe kdist build dependencies were passed last on nix MacOS compared to being passed first on nix Linux. Therefore, due to a file having the same name in wasm-semantics and in skribe-semantics, the nix build succeeded on Linux and failed on MacOS.

Expected Results

The build should fail if a file that is included via the requires keyword exists in multiple places. At the very least, a warning should be generated.