diff --git a/Cargo.lock b/Cargo.lock index 8f99c87f9ba82..d5056dbfcc27d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2866,6 +2866,7 @@ dependencies = [ "aptos-vm", "clap 4.4.14", "move-cli", + "move-model", "move-package", "move-prover", "move-unit-test", diff --git a/aptos-move/framework/tests/move_prover_tests.rs b/aptos-move/framework/tests/move_prover_tests.rs index 94237a2e220f2..9bb09f7314e18 100644 --- a/aptos-move/framework/tests/move_prover_tests.rs +++ b/aptos-move/framework/tests/move_prover_tests.rs @@ -2,6 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 use aptos_framework::{extended_checks, prover::ProverOptions}; +use move_binary_format::file_format_common::VERSION_DEFAULT; +use move_model::metadata::{CompilerVersion, LanguageVersion}; use std::{collections::BTreeMap, path::PathBuf}; const ENV_TEST_INCONSISTENCY: &str = "MVP_TEST_INCONSISTENCY"; @@ -57,9 +59,9 @@ pub fn run_prover_for_pkg(path_to_pkg: impl Into) { false, pkg_path.as_path(), BTreeMap::default(), - None, - None, - None, + Some(VERSION_DEFAULT), + Some(CompilerVersion::latest_stable()), + Some(LanguageVersion::latest_stable()), skip_attribute_checks, extended_checks::get_all_attribute_names(), &[], diff --git a/aptos-move/move-examples/Cargo.toml b/aptos-move/move-examples/Cargo.toml index 7380a8bccfc5f..7eb718b6a160a 100644 --- a/aptos-move/move-examples/Cargo.toml +++ b/aptos-move/move-examples/Cargo.toml @@ -19,6 +19,7 @@ aptos-types = { workspace = true } aptos-vm ={ workspace = true, features = ["testing"] } clap = { workspace = true } move-cli = { workspace = true } +move-model = { workspace = true } move-package = { workspace = true } move-prover = { workspace = true } move-unit-test = { workspace = true } diff --git a/aptos-move/move-examples/tests/move_prover_tests.rs b/aptos-move/move-examples/tests/move_prover_tests.rs index 23db183aafbed..b3bec1b1f7cbf 100644 --- a/aptos-move/move-examples/tests/move_prover_tests.rs +++ b/aptos-move/move-examples/tests/move_prover_tests.rs @@ -4,6 +4,7 @@ use aptos_framework::extended_checks; use aptos_types::account_address::AccountAddress; use move_cli::base::prove::run_move_prover; +use move_model::metadata::{CompilerVersion, LanguageVersion}; use move_package::CompilerConfig; use std::{collections::BTreeMap, path::PathBuf}; use tempfile::tempdir; @@ -28,6 +29,8 @@ pub fn run_prover_for_pkg( install_dir: Some(tempdir().unwrap().path().to_path_buf()), compiler_config: CompilerConfig { known_attributes: extended_checks::get_all_attribute_names().clone(), + compiler_version: Some(CompilerVersion::latest_stable()), + language_version: Some(LanguageVersion::latest_stable()), ..Default::default() }, ..Default::default() diff --git a/crates/aptos/CHANGELOG.md b/crates/aptos/CHANGELOG.md index 2e687eba93ecd..5f56758e8c928 100644 --- a/crates/aptos/CHANGELOG.md +++ b/crates/aptos/CHANGELOG.md @@ -7,6 +7,7 @@ All notable changes to the Aptos CLI will be captured in this file. This project - Add `aptos update prover-dependencies`, which installs the dependency of Move prover, boogie, z3 and cvc5. - Update the default version of `movefmt` to be installed from 1.0.4 to 1.0.5 - Update the local-testnet logs to use `println` for regular output and reserve `eprintln` for errors. +- Set compiler V2 as default when using `aptos move prove`. ## [4.2.3] - 2024/09/20 - Fix the broken indexer in localnet in 4.2.2, which migrates table info from sycn to async ways. diff --git a/crates/aptos/src/move_tool/mod.rs b/crates/aptos/src/move_tool/mod.rs index 4b15f51e6b63e..74e2eaaa5eb1a 100644 --- a/crates/aptos/src/move_tool/mod.rs +++ b/crates/aptos/src/move_tool/mod.rs @@ -644,14 +644,21 @@ impl CliCommand<&'static str> for ProvePackage { prover_options, } = self; + let compiler_version = move_options + .compiler_version + .or_else(|| Some(CompilerVersion::latest_stable())); + let language_version = move_options + .language_version + .or_else(|| Some(LanguageVersion::latest_stable())); + let result = task::spawn_blocking(move || { prover_options.prove( move_options.dev, move_options.get_package_path()?.as_path(), move_options.named_addresses(), - fix_bytecode_version(move_options.bytecode_version, move_options.language_version), - move_options.compiler_version, - move_options.language_version, + fix_bytecode_version(move_options.bytecode_version, language_version), + compiler_version, + language_version, move_options.skip_attribute_checks, extended_checks::get_all_attribute_names(), &[], diff --git a/third_party/move/move-model/src/metadata.rs b/third_party/move/move-model/src/metadata.rs index c1a26833bffc8..3ff8814dced2a 100644 --- a/third_party/move/move-model/src/metadata.rs +++ b/third_party/move/move-model/src/metadata.rs @@ -145,6 +145,16 @@ impl CompilerVersion { } } + /// The latest compiler version. + pub fn latest() -> Self { + CompilerVersion::V2_1 + } + + /// The latest stable compiler version. + pub fn latest_stable() -> Self { + CompilerVersion::V2_0 + } + /// Check whether the compiler version supports the given language version, /// generates an error if not. pub fn check_language_support(self, version: LanguageVersion) -> anyhow::Result<()> { @@ -236,6 +246,16 @@ impl LanguageVersion { } } + /// The latest language version. + pub fn latest() -> Self { + LanguageVersion::V2_1 + } + + /// The latest stable language version. + pub fn latest_stable() -> Self { + LanguageVersion::V2_0 + } + /// Whether the language version is equal to greater than `ver` pub fn is_at_least(&self, ver: LanguageVersion) -> bool { *self >= ver diff --git a/third_party/move/tools/move-cli/src/base/prove.rs b/third_party/move/tools/move-cli/src/base/prove.rs index f11e2cbf47ab9..27a499c3db82f 100644 --- a/third_party/move/tools/move-cli/src/base/prove.rs +++ b/third_party/move/tools/move-cli/src/base/prove.rs @@ -6,8 +6,9 @@ use anyhow::bail; use clap::Parser; use codespan_reporting::term::termcolor::{ColorChoice, StandardStream}; use colored::Colorize; +use move_model::metadata::{CompilerVersion, LanguageVersion}; use move_package::{BuildConfig, ModelConfig}; -use move_prover::run_move_prover_with_model; +use move_prover::run_move_prover_with_model_v2; use std::{ io::Write, path::{Path, PathBuf}, @@ -127,7 +128,10 @@ impl ProverTest { for_test: true, options: Some(ProverOptions::Options(std::mem::take(&mut self.options))), }; - let res = cmd.execute(Some(pkg_path), move_package::BuildConfig::default()); + let mut build_config = BuildConfig::default(); + build_config.compiler_config.language_version = Some(LanguageVersion::latest_stable()); + build_config.compiler_config.compiler_version = Some(CompilerVersion::latest_stable()); + let res = cmd.execute(Some(pkg_path), build_config); std::env::set_current_dir(saved_cd).expect("restore current directory"); res.unwrap() } @@ -212,7 +216,7 @@ pub fn run_move_prover( } else { None }; - let res = run_move_prover_with_model(&mut model, &mut error_writer, options, Some(now)); + let res = run_move_prover_with_model_v2(&mut model, &mut error_writer, options, now); if for_test { let basedir = path .file_name()