Linking Z3 fails on rebuild

[qaristote]

Describe the bug It sometimes happen that linking Z3 will fail at compile time, raising the following error:

[46 of 46] Compiling Language.Pirouette.Example.IsUnity ( src/Language/Pirouette/Example/IsUnity.hs, /home/niols/git/tweag/pirouette/dist-newstyle/build/x86_64-linux/ghc-9.0.2/pirouette-2.0.0/build/Language/Pirouette/Example/IsUnity.p_o ) [TH]
<command line>: user specified .o/.so/.DLL could not be loaded (libz3.so: cannot open shared object file: No such file or directory)
Whilst trying to load:  (dynamic) z3
Additional directories searched: (none)
cabal: Failed to build pirouette-2.0.0 (which is required by test:spec from
pirouette-2.0.0).

To Reproduce This is unclear. @Niols says it sometimes happens to him when running cabal run test, it happened to me while rebuilding Pirouette after a change.

Expected behavior Pirouette should compile properly every time.

Additional context This was introduced in #154. This doesn't seem to happen on the very first build, as the CI didn't fail unexpectedly after that. A solution is to explicitely set

LD_LIBRARY_PATH="${pkgs.z3.lib}/lib";

in shell.nix, but it doesn't feel right: Nix should be doing that automatically.

[qaristote]

It seems making a meaningful change to src/Pirouette/Symbolic/Eval.hs (I didn't try other files) is enough to reproduce the error. For instance

$ cabal clean
$ cabal build
$ $EDITOR src/Pirouette/Symbolic/Eval.hs # edit the file so that the module's signature changes
$ cabal build

should produce this error message.

[qaristote]

I get the same error when I try putting z3.dev inside buildInputs instead of nativeBuildInputs.

[qaristote]

Looking at the ouput of set, it seems choosing buildInputs or nativeBuildInputs doesn't matter: in both cases, z3.dev appears in NIX_CFGLAGS_COMPILE and z3.lib in NIX_LDFLAGS.

[qaristote]

If I replace {-# OPTIONS_GHC -lz3 #-} with {-# OPTIONS_GHC -L/path/to/z3-lib/lib -lz3 #-} in the header of src/Language/Pirouette/Example/IsUnity.hs I can't reproduce the error anymore. Recall that this flag was added in https://github.com/tweag/pirouette/pull/154/commits/2522d0bdb0325b6c546403e94b7588f2313c2f6a by @facundo because having no flag at all causes the following error:

[46 of 46] Compiling Language.Pirouette.Example.IsUnity ( src/Language/Pirouette/Example/IsUnity.hs, /home/qaristote/code/pirouette/dist-newstyle/build/x86_64-linux/ghc-9.0.2/pirouette-2.0.0/build/Language/Pirouette/Example/IsUnity.o, /home/qaristote/code/pirouette/dist-newstyle/build/x86_64-linux/ghc-9.0.2/pirouette-2.0.0/build/Language/Pirouette/Example/IsUnity.dyn_o )

GHC.Runtime.Linker.dynLoadObjs: Loading temp shared object failed
During interactive linking, GHCi couldn't find the following symbol:
  /tmp/ghc974135_0/libghc_3.so: undefined symbol: Z3_del_context
This may be due to you not asking GHCi to load extra object files,
archives or DLLs needed by your current session.  Restart GHCi, specifying
the missing library using the -L/path/to/object/dir and -lmissinglibname
flags, or simply by naming the relevant files on the GHCi command line.
Alternatively, this link failure might indicate a bug in GHCi.
If you suspect the latter, please report this as a GHC bug:
  https://www.haskell.org/ghc/reportabug

cabal: Failed to build pirouette-2.0.0 (which is required by test:spec from
pirouette-2.0.0).

IIRC this was caused by Template Haskell.

[facundominguez]

This is unclear. @Niols says it sometimes happens to him when running cabal run test, it happened to me while rebuilding Pirouette after a change.

Any chance these commands are inadvertently run from outside a nix shell?

[Niols]

Nope, I was very much in the Nix Shell (I wouldn't even have Cabal on the outside and I made sure that the Nix Shell was up to date).