Installation of Agda fails when missing executable from executables file

[MatthewDaggitt]

If you have an executable listed in your executables file that is missing, and you try to install Agda, it fails. The error message given does mention that the executable is missing, but doesn't flag that its the main cause. I'd diagnosed it as a configuration problem with Cabal, and I've spent about 10 hours in the last few days nuking and reinstalling cabal/Agda repeatedly trying to get to the root of it 😢

The installation really shouldn't fail in this scenario.

The error message given is as follows:

cabal install Agda
Resolving dependencies...
Build profile: -w ghc-9.0.1 -O1
In order, the following will be built (use -v for more details):
 - Agda-2.6.2.1 (lib:Agda, exe:agda, exe:agda-mode) (requires build)
Starting     Agda-2.6.2.1 (all, legacy fallback)
Building     Agda-2.6.2.1 (all, legacy fallback)
Installing   Agda-2.6.2.1 (all, legacy fallback)
Preprocessing executable 'agda' for Agda-2.6.2.1..
Building executable 'agda' for Agda-2.6.2.1..
[1 of 1] Compiling Main             ( src/main/Main.hs, dist/build/agda/agda-tmp/Main.o )
Linking dist/build/agda/agda ...
Installing executable agda-mode in /home/matthew/.cabal/store/ghc-9.0.1/incoming/new-14467/home/matthew/.cabal/store/ghc-9.0.1/Agda-2.6.2.1-234bebf544085d48fcaed631d5b33fc54cd47c5cf3aa6a71274592a010aa6002/bin
Warning: The directory
/home/matthew/.cabal/store/ghc-9.0.1/incoming/new-14467/home/matthew/.cabal/store/ghc-9.0.1/Agda-2.6.2.1-234bebf544085d48fcaed631d5b33fc54cd47c5cf3aa6a71274592a010aa6002/bin
is not in the system search path.
Installing library in /home/matthew/.cabal/store/ghc-9.0.1/incoming/new-14467/home/matthew/.cabal/store/ghc-9.0.1/Agda-2.6.2.1-234bebf544085d48fcaed631d5b33fc54cd47c5cf3aa6a71274592a010aa6002/lib
Installing executable agda in /home/matthew/.cabal/store/ghc-9.0.1/incoming/new-14467/home/matthew/.cabal/store/ghc-9.0.1/Agda-2.6.2.1-234bebf544085d48fcaed631d5b33fc54cd47c5cf3aa6a71274592a010aa6002/bin
Warning: The directory
/home/matthew/.cabal/store/ghc-9.0.1/incoming/new-14467/home/matthew/.cabal/store/ghc-9.0.1/Agda-2.6.2.1-234bebf544085d48fcaed631d5b33fc54cd47c5cf3aa6a71274592a010aa6002/bin
is not in the system search path.
 Executable '/home/matthew/.cabal/bin/vehicle' not found.
Error: Failed to typecheck /tmp/cabal-install.-14467/dist-newstyle/tmp/src-14467/Agda-2.6.2.1/src/data/lib/prim/Agda/Builtin/Bool.agda!
Generating Agda library interface files...
... /tmp/cabal-install.-14467/dist-newstyle/tmp/src-14467/Agda-2.6.2.1/src/data/lib/prim/Agda/Builtin/Bool.agda
cabal: Failed to build Agda-2.6.2.1. See the build log above for details.

If I remove '/home/matthew/.cabal/bin/vehicle' from the executables file, then it installs fine.

[nad]

There is an option --no-libraries that (I hope) ensures that the libraries and defaults files are not read. We could add a similar option for the executables file, and use it in Setup.hs.

[andreasabel]

Do we have to verify the contents of the executables file eagerly whenever starting Agda, or could this be done lazily, when using an executable the first time? CC @wenkokke

[UlfNorell]

I postponed the check in #5786. It's checking every time an executable is called rather than only the first time. I haven't measured anything, but I don't believe the checks take any significant amount of time.

I don't see any problems delaying the check. One concern might be that executables can appear or disappear (or change) during the execution of Agda, but checking up front doesn't help anything with that.