Leaner build system causes tests to fail with weird exception

[Niols]

This issue is here to track the debugging of the issue caused by https://github.com/tweag/plutus-libs/pull/187 where:

$ cabal test pirouette-plutusir:spec
...
Test suite spec: RUNNING...
Language
  PlutusIR
    ToTerm
      With resource: resources/fromPlutusIRSpec-01.pir
        Translates the PIR program without errors: OK
        Decls contain 'long' and 'short' terms:    OK
        expandDefs produces NF terms:              OK
    Builtins
      Read, translate and typecheck programs
        Split:                                     OK
        Auction:                                   OK (0.02s)
      Can parse terms:                             OK
    Symbolic evaluation
      simple triples
        [input > 0] add 1 [result > 0] counter:    FAIL
          Exception: fd:15: hGetLine: end of file
          Use -p '/[input > 0] add 1 [result > 0] counter/' to rerun this test only.
        [input > 0] add 1 [result > 1] verified:   FAIL
          Exception: fd:18: hGetLine: end of file
          Use -p '/[input > 0] add 1 [result > 1] verified/' to rerun this test only.

2 out of 8 tests failed (0.06s)
Test suite spec: FAIL
...

[Niols]

The issue could be reproduced exactly (file descriptors included):

• in CI
• on my local machine
• on @gabrielhdt's machine
• on the Tweag builder

[Niols]

A bisection shows that both 07301a6 (last commit on main before @gabrielhdt's fork) and 35856cd (last commit on main at time of writing this) are exempt of this bug.

[Niols]

Some trace-based debugging leads me to think that the bug is somewhere in this piece of code. To my surprise, it does not seem to take place in openAndParsePIR but rather in execIncorrectnessLogic.

Following up would involve debugging in Pirouette. Pirouette does not use the mentioned hGetLine but it probably uses some higher-level version of it.

[Niols]

Trying to build gh@trythings with IOHK's compiler (instead of the one from nixpkgs) does not improve the situation.

[Niols]

Bringing back LANG = "en_US.UTF-8"; and/or LOCALE_ARCHIVE = "${pkgs.glibcLocales}/lib/locale/locale-archive" does not help with the situation.

[Niols]

8d14a973832e28b0fc6577fa5efd25ef12232530 seems to be the first commit with an issue. Sadly, this commit is pretty big.

[Niols]

Compiling https://github.com/tweag/plutus-libs/commit/8d14a973832e28b0fc6577fa5efd25ef12232530 with nixpkgs pinned to the version pinned by Niv in https://github.com/tweag/plutus-libs/commit/07301a69afaa2de0215a820dbd210ebe6e2f5748 (https://github.com/NixOS/nixpkgs/commit/74b10859829153d5c5d50f7c77b86763759e8654) also fails in the same way.

[Niols]

Compiling https://github.com/tweag/plutus-libs/commit/8d14a973832e28b0fc6577fa5efd25ef12232530 with an old version of Pirouette (https://github.com/tweag/pirouette/commit/3805638e0e11b5a0fc5cc6a41bd415d52674d23a) and Z3 and CVC4 in the Shell's buildInputs works! So it probably has to do with the new integration of Z3.

Edit: welp, there it is. It was probably just CVC4 missing from the environment. SO DUMB.

[Niols]

My experiments show that, actually, everything runs fine with recent commits of Pirouette. Not the most recent ones because there was an API change. It looks like https://github.com/tweag/pirouette/commit/69d1eea works fine. Hence #209 (and its corresponding PR on @gabrielhdt's branch, https://github.com/gabrielhdt/plutus-libs/pull/1).

[Niols]

I ran a git bisect on Pirouette to try and find where the bug was fixed. The last versions that contain the bug are:

• https://github.com/tweag/pirouette/commit/41fe7a5836469d1fecde69bf13482d54771926ca, the version currently in cabal.project.
• https://github.com/tweag/pirouette/commit/c511a16, the commit on which PRs https://github.com/tweag/pirouette/pull/153 and https://github.com/tweag/pirouette/pull/154 are based.
• https://github.com/tweag/pirouette/commit/c15b4a4741bbae3014ea93a21118ca8e21ee77bf, the merge commit of https://github.com/tweag/pirouette/pull/153.

The first versions that do not contain the bug anymore are:

• https://github.com/tweag/pirouette/commit/748cbb6, the merge commit of https://github.com/tweag/pirouette/pull/154.
• https://github.com/tweag/pirouette/commit/33977c2e05fd32213a8c804a0eaf1329d8b3d7ef, a commit within https://github.com/tweag/pirouette/pull/154.

First, I include https://github.com/tweag/pirouette/pull/153 in my picture because it was merged into https://github.com/tweag/pirouette/pull/154 before this one was merged back into main. Second, sadly, the very first commits of https://github.com/tweag/pirouette/pull/154 do not compile, so we only know that the bug was fixed on the path:

• https://github.com/tweag/pirouette/commit/c511a16 (with the bug)
• https://github.com/tweag/pirouette/commit/c79d8bb (does not compile)
• https://github.com/tweag/pirouette/commit/f52cf48 (does not compile)
• https://github.com/tweag/pirouette/commit/64f18eb (does not compile)
• https://github.com/tweag/pirouette/commit/33977c2 (without the bug)

One could for instance compare what those commits change to try and understand where the bug comes from.

[Niols]

The conclusion of this debugging session is STUPID. plutus-libs was following an old version of Pirouette... that was still using CVC4. Pirouette was not finding the binary and not managing to talk it and therefore failing when reading from it. It would deserve better error reporting but this point is made irrelevant by the recent changes in Pirouette that now relies on SMTLIB-backends. The improvement to error reporting can be tracked there, cf https://github.com/tweag/smtlib-backends/issues/43.

In the meantime, there are two possible fixes to this:

• we can add CVC4 as a dependency in the flake
• or we can bump Pirouette's version and add Z3 as a dependency in the flake. This is essentially what https://github.com/gabrielhdt/plutus-libs/pull/1 does and I would rather go for this option.