Closed Coda-Coda closed 1 year ago
@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.
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
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
).
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.
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 528b0cd7020290594360d69b895a9155e681e511) 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: