安装 Move Prover

如果您想使用 Move Prover,请在安装 CLI 二进制文件后安装 Move Prover 依赖项. 安装 Prover 依赖项有两种方式.

通过 Aptos CLI 安装(推荐)

1. 安装最新的 Aptos CLI 二进制文件.

2. 执行命令 aptos update prover-dependencies.

注意

安装后环境变量 BOOGIE_EXE 和 Z3_EXE 将自动设置.请确保它们在当前环境中生效.

通过 aptos-core 安装(不推荐)

1. 参见从源代码构建 Aptos

2. 然后,在检出的 aptos-core 目录中,安装额外的 Move 工具:

   Linux / macOS

   1. 打开终端会话.
   2. 运行开发设置脚本来准备您的环境:./scripts/dev_setup.sh -yp
   3. 更新您当前的 shell 环境:source ~/.profile

   注意

   dev_setup.sh -p 使用环境变量更新您的 ~./profile 以支持已安装的 Move Prover 工具.您可能需要为您的 shell 设置 .bash_profile 或 .zprofile 或其他设置文件.

   Windows

   1. 以管理员身份打开 PowerShell 终端.
   2. 运行开发设置脚本来准备您的环境:PowerShell -ExecutionPolicy Bypass -File ./scripts/windows_dev_setup.ps1 -y

安装后,您可以运行 Move Prover 来验证一个示例:

aptos move prove --package-dir aptos-move/move-examples/hello_prover/

故障排除

如果在运行命令时遇到如下错误,请检查您的 Aptos CLI 版本或验证您使用的是正确的 aptos 工具,特别是如果您安装了多个版本.

error: unexpected token
    ┌─ ~/.move/https___github_com_aptos-labs_aptos-core_git_main/aptos-move/framework/aptos-framework/sources/randomness.move:515:16
    │
515 │         for (i in 0..n) {
    │             -  ^ Expected ')'
    │             │
    │             To match this '('

{
  "Error": "Move Prover failed: exiting with model building errors"
}