Discovered when looking at #5070. Ping @wenkokke.
Agda accepts silently executables with the same basename:

E.g. I can write this into .agda/executables:

/bin/echo
/Users/abel/foetus/sml/echo

(The second command does not echo, but crashes if called on the command line.)

This makes the example from the docs fail:

{-# OPTIONS --allow-exec #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Reflection.External
open import Agda.Builtin.Sigma
open import Agda.Builtin.String
open import Agda.Builtin.Unit

_>>=_ = bindTC

macro
  echo : List String → Term → TC ⊤
  echo args hole = do
    (exitCode , (stdOut , stdErr)) ← execTC "echo" args ""
    unify hole (lit (string stdOut))

_ : echo ("hello" ∷ "world" ∷ []) ≡ "hello world\n"
_ = refl

Error:

"" != "hello world\n" of type String
when checking that the expression refl has type
"" ≡ "hello world\n"

It succeeds if I swap the entries in the executables file.
This behaviour can be explained by a use Map.fromList, which takes the last of the duplicate entries and throws the others away silently. (You have been warned by @gallais!)

This is a potential security problem!

Also, Agda swallows the OS error thrown by the second executable and simply returns the empty string. That's DOS/Windows-style error swallowing, not good...

Agda should report:

• conflicting entries in executables
• errors (or at least exitcodes) thrown by run executables.