nix-build fails on master

[Coda-Coda]

Issue description

Following the instructions for building with Nix then running nix-build gives an error (below), on branch master. Note that this error does not occur at v4.7.1 and Pact builds fine when the repo is checked out at that tag.

Steps to reproduce

Clone the repository (master branch, currently commit 528b0cd)
Follow the Nix instructions in the Wiki.
nix-build

Expected Behavior

Pact should build without errors.

Debug Information

Running on NixOS,
The error produced is:

...
building '/nix/store/p55gg6wfw2mx5vfij0025srhp9s3k540-cabal2nix-pact.drv'...
installing
error:
       … while calling the 'derivationStrict' builtin

         at //builtin/derivation.nix:9:12: (source not available)

       … while evaluating derivation 'pact'
         whose name attribute is located at /nix/store/p3x4ha4dwj9agifi05wq0vf3m93p3vsx-source/pkgs/build-support/trivial-builders.nix:7:14

       … while evaluating attribute 'text' of derivation 'pact'

         at /nix/store/p3x4ha4dwj9agifi05wq0vf3m93p3vsx-source/pkgs/build-support/trivial-builders.nix:61:16:

           60|     runCommand name
           61|       { inherit text executable;
             |                ^
           62|         passAsFile = [ "text" ];

       error: function 'anonymous lambda' called without required argument 'crypton'

       at /nix/store/6a1h0hnz463dq1laa4d7q6lnhrfqamnq-cabal2nix-pact/default.nix:1:1:

            1| { mkDerivation, aeson, algebraic-graphs, ansi-terminal, async
             | ^
            2| , attoparsec, base, base16-bytestring, base64-bytestring, bound

[rsoeldner]

@Coda-Coda Thank you for bringing this up. Indeed, I can confirm this issue, which I address in #1276.

Please use the nix build command to build pact.

[Coda-Coda]

Hi @rsoeldner, thanks for the fix! However, I'm now having issues related to z3. After building pact with nix build on master or rsoeldner/nix-flake-only then running the verification example from https://chainweaver.kadena.network/contracts I get an error (shown below). Evidently installation of z3 hasn't happened properly. This example works fine on v4.7.1 built with nix-build. I feel this is a related issue to the current issue, but if it's better to open a new issue for it that's fine.

$ ./pact 
pact> ;;
....> ;; A little example showing off the merits of formal
....> ;; verification and why it pays off.
....> ;;
....> 
....> (namespace "free")
<interactive>:5:0:Error: namespace: 'free' not defined
 at <interactive>:5:0: (namespace "free")
pact> 
pact> (module verification MODULE_ADMIN
....>   @doc "Little example to show off the usefulness of formal verification."
....> 
....>   ; no-op module admin for example purposes.
....>   ; in a real contract this could enforce a keyset, or
....>   ; tally votes, etc.
....>   (defcap MODULE_ADMIN () true)
....> 
....>   (defun absBug:integer (num:integer)
....>      @doc "Ensure positive result"
....> 
....>      ;; This property fails
....>      ;; Would you have caught that with unit tests?
....>      @model [(property (>= result 0))]
....> 
....>      (if (= (- (* (- num 6) (+ num 11)) (* 42 num)) (* (* 64 7) 52270780833))
....>          (- 1)
....>          (abs num)
....>      )
....>    )
....>  )
"Loaded module verification, hash Gl9ySySdfSW715xd72rFOjU_5vcssSjxnxcI2u7eWQQ"
pact> 
pact> (verify "verification")
<interactive>:1:0:Error: Unable to locate executable for Z3 Executable specified: "z3"  CallStack (from HasCallStack):   error, called at ./Data/SBV/SMT/SMT.hs:648:23 in sbv-9.2-HTCJM8Zp57BI8ezDj7sDp6:Data.SBV.SMT.SMT

Expected result:

...
pact> (verify "verification")
"Verification of verification failed"
<interactive>:11:23:OutputFailure: Invalidating model found in verification.absBug
  Program trace:
    entering function verification.absBug with argument
      num = -4839125
    
      returning with -1

[rsoeldner]

I'm not a nix expert, but to my knowledge, nix build (as well as nix-build) only build the derivation artifacts. In this case, the pact binary. You need to install Z3 independently, or alternatively, enter the shell via nix develop (which would require you to build the executable via cabal build).

[Coda-Coda]

I see, thanks. Instead of building via cabal build it works to first do nix develop (getting z3) then doing nix build, and then running the example I gave works as expected. Thanks for your help!

I'm not sure why nix-build on v4.7.1 worked for that example as I don't have z3 installed globally.