Skip to content

Cannot supply custom --kore-rpc-command to kevm foundry-prove #2033

Open
@geo2a

Description

@geo2a

When calling kevm found-prove, kevm does not have access to neither kore-rpc-booster nor even kore-rpc.

An attempt to provide a trivial custom command fails as follows (shortened):

cd test/foundry
...
$ kevm foundry-prove --verbose --test AccountParamsTest.testDealConcrete --kore-rpc-command 'kore–rpc'
...
INFO 2023-08-23 12:10:40,636 pyk.kore.rpc - Starting KoreServer: kore–rpc out/kompiled/definition.kore --module FOUNDRY-MAIN --server-port 0 --smt-timeout 300 --smt-retry-limit 10
...
FileNotFoundError: [Errno 2] No such file or directory: 'kore–rpc'

The command works as expected if given an absolute path to kore-rpc/kore-rpc-booster`:

$ kevm foundry-prove --verbose --test AccountParamsTest.testDealConcrete --kore-rpc-command '/nix/store/<LONG_STRING>/bin/kore–rpc'
...Normal output...

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't workingcli

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions