[Bug] Move Prover not working on Aptos CLI

[wintertoro]

🐛 Bug

https://github.com/aptos-labs/aptos-core/pull/2086

To reproduce

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

// Paste the output here

FAILURE proving 1 modules from package hello_prover in 0.074s { "Error": "Move Prover failed" }

Expected Behavior

System information

Please complete the following information:

• Aptos CLI Release v0.2.5
• rust: stable 1.62.1
• Mac OS Monteray v12.5

Additional context

Add any other context about the problem here.

[davidiw]

did you install the dev setup with all the prover function? but the error message isn't great either...

[wintertoro]

I succeeded in all the tasks before like hello blockchain. I cloned the whole Aptos-core and I double checked that the prover files were in the right directory I was referencing

Jing

On Aug 13, 2022, at 8:55 AM, David Wolinsky @.***> wrote:

 did you install the dev setup with all the prover function? but the error message isn't great either...

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you authored the thread.

[wrwg]

Unfortunately, the actual prover error is omitted by the CLI, something which will be fixed soon. From the information given here, there is not much to say. Just to make clear what @davidiw already mentioned. You must install the needed tools as follows:

cd aptos-core
./scripts/dev_setup.sh -yp
source ~/.profile
# Verify things work
$BOOGIE_EXE

Closing now, feel free to reopen once there is more information about this error.

[wintertoro]

Hi first of all, I want to note that the tutorial does not give instructions on setting that up.

I also want to note that dev-setup.sh, devnet was on 5.0 and I keep getting build errors cause its no longer supported. So I checked the latest version, and dotnet is now on 6.0, and the moment I changed the versioning in the dev-setup.sh file, the download worked. Likewise for boogie, I had to change it a newer version for it to download.

BOOGIE_EXE gives me *** Error: No input files were specified. Is there something I should be appending?

Also, even with those tools now downloaded, the prover still doesn't work. Same error message. Does upgrading to the newer dotnet and boogie version break it?

cd aptos-core ./scripts/dev_setup.sh -yp source ~/.profile cd: no such file or directory: aptos-core Welcome to Aptos!

This script will download and install the necessary dependencies needed to build, test and inspect Aptos Core.

Based on your selection, these tools will be included: Move prover tools (since -y was provided):

• z3
• cvc5
• dotnet
• boogie Moreover, ~/.profile will be updated (since -p was provided). If you'd prefer to install these dependencies yourself, please exit this script now with Ctrl-C. Proceed with installing necessary dependencies? (y/N) > y curl is already installed Installing Z3 Z3 4.8.13 already installed Installing cvc5 cvc5 0.0.3 already installed Installing .Net ./scripts/dev_setup.sh: line 442: /Users/jing/.dotnet//dotnet: No such file or directory dotnet-install: Note that the intended use of this script is for Continuous Integration (CI) scenarios, where: dotnet-install: - The SDK needs to be installed without user interaction and without admin rights. dotnet-install: - The SDK installation doesn't need to persist across multiple CI runs. dotnet-install: To set up a development environment or to run apps, use installers rather than this script. Visit https://dotnet.microsoft.com/download to get the installer.

dotnet-install: Attempting to download using primary link https://dotnetcli.azureedge.net/dotnet/Sdk/5.0.408/dotnet-sdk-5.0.408-osx-arm64.tar.gz curl: (22) The requested URL returned error: 404 dotnet-install: The resource at primary link 'https://dotnetcli.azureedge.net/dotnet/Sdk/5.0.408/dotnet-sdk-5.0.408-osx-arm64.tar.gz' is not available. dotnet-install: Attempting to download using legacy link https://dotnetcli.azureedge.net/dotnet/Sdk/5.0.408/dotnet-dev-osx-arm64.5.0.408.tar.gz curl: (22) The requested URL returned error: 404 dotnet-install: The resource at legacy link 'https://dotnetcli.azureedge.net/dotnet/Sdk/5.0.408/dotnet-dev-osx-arm64.5.0.408.tar.gz' is not available. dotnet_install: Error: Could not find .NET Core SDK with version = 5.0.408 dotnet_install: Error: Refer to: https://aka.ms/dotnet-os-lifecycle for information on .NET Core support

[davidiw]

We're updating to expose the error. Once that PR lands, let's try again :)

[github-actions[bot]]

This issue is stale because it has been open 45 days with no activity. Remove the stale label or comment - otherwise this will be closed in 15 days.