-
Notifications
You must be signed in to change notification settings - Fork 3.5k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[do-not-merge] apply the updated movefmt tool to framework code #13342
Conversation
⏱️ 2h 5m total CI duration on this PR
|
cc9aa7c
to
8def7f9
Compare
8def7f9
to
2d746ed
Compare
Codecov ReportAll modified and coverable lines are covered by tests ✅
Additional details and impacted files@@ Coverage Diff @@
## main #13342 +/- ##
=======================================
Coverage 57.5% 57.5%
=======================================
Files 833 833
Lines 198661 198662 +1
=======================================
+ Hits 114281 114293 +12
+ Misses 84380 84369 -11 ☔ View full report in Codecov by Sentry. |
@@ -90,8 +95,8 @@ module std::bit_vector { | |||
public fun shift_left(bitvector: &mut BitVector, amount: u64) { | |||
if (amount >= bitvector.length) { | |||
vector::for_each_mut(&mut bitvector.bit_field, |elem| { | |||
*elem = false; | |||
}); | |||
*elem = false; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This extra indent looks strange to me.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is because it is nested within two layers of calls, one is lambda and the other is for_each_mut
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I see your point but I still think the original code looks better. cc @vineethk
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Might be worth checking what rustfmt does in a similar situation.
It is a bit counter-intuitive that there is extra indentation here compared to the original. It would be okay if for some reason the lambda would have to be pushed to the next line, but as is, it does look weird. In general, having 8 spaces (or rather double or more of the default indentation) looks out of place IMHO.
if (bit_index >= length(bitvector)) { | ||
false | ||
} else { | ||
if (bit_index >= length(bitvector)) { false } |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This does not look correct to me.
invariant index >= start_index; | ||
invariant index == start_index || is_index_set(bitvector, index - 1); | ||
invariant index == start_index || index - 1 < vector::length(bitvector | ||
.bit_field); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This new line does not look correct to me.
ensures amount < bitvector.length ==> | ||
(forall i in bitvector.length - amount..bitvector.length: !bitvector.bit_field[i]); | ||
ensures amount < bitvector.length ==> | ||
(forall i in 0..bitvector.length - amount: bitvector.bit_field[i] == old(bitvector).bit_field[i + amount]); | ||
(forall i in 0..bitvector.length - amount: bitvector.bit_field[i] == old( | ||
bitvector).bit_field[i + amount]); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This new line does not look correct to me.
while (vector::length(features) <= byte_index) { | ||
vector::push_back(features, 0) | ||
}; | ||
while (vector::length(features) <= byte_index) { vector::push_back(features, 0) }; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Squeezing into one line does not look correct to me.
ed25519::signature_to_bytes(&alice_signer_capability_offer_sig), | ||
0, | ||
alice_pk_bytes, | ||
bob_addr | ||
); | ||
bob_addr); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Bracket should be in a new line?
|
||
let address_map = global<OriginatingAddress>(@aptos_framework).address_map; | ||
let new_auth_key = from_bcs::deserialize<address>(new_auth_key_vector); | ||
|
||
aborts_if !exists<OriginatingAddress>(@aptos_framework); | ||
aborts_if !from_bcs::deserializable<address>(account_resource.authentication_key); | ||
aborts_if table::spec_contains(address_map, curr_auth_key) && | ||
table::spec_get(address_map, curr_auth_key) != originating_addr; | ||
aborts_if table::spec_contains(address_map, curr_auth_key) && table::spec_get( |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The original code looks better.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In general, breaking to newline after an operator is preferable to breaking to newline in the middle of a call (like in the original).
|
||
let post auth_key = global<Account>(addr).authentication_key; | ||
ensures auth_key == new_auth_key_vector; | ||
|
||
} | ||
|
||
spec rotate_authentication_key_with_rotation_capability( | ||
delegate_signer: &signer, | ||
spec rotate_authentication_key_with_rotation_capability(delegate_signer: &signer, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The original code looks better
addr != @0x9 && | ||
addr != @0xa | ||
spec fun spec_is_framework_address(addr: address): bool { | ||
addr != @0x1 && addr != @0x2 && addr != @0x3 && addr != @0x4 && addr != @0x5 && addr |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not sure whether we should format this.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In general, it seems like having a way for the user to specify parts of code that should be left as-is without formatting is likely very important, because a user might have spent a lot of time hand-formatting certain parts of code to read a particular way.
There are two ways to handle this:
- Comments above and below the block of code that should not be formatted (
// move-format off
and// move-format on
). This is what is done in a lot of C++ tools. The positives are that it could be applied to an arbitrary portion of the code (eg., for three functions out of several, or a subset of statements within a function). The negative is that it is not really first class to the language. - Have an attribute like
#[move-format::skip]
on blocks of code that the user wants formatting to be skipped. This is what rustfmt does, however, it has the drawback of requiring lots of annotations or workarounds (see https://stackoverflow.com/questions/67288537/how-can-i-switch-off-rustfmt-for-a-region-of-code-instead-of-a-single-item), and also, we would need to support these attributes (but probably only for compiler v2).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@robinlzw , since option 2 requires support of the attribute, we may want to go with option 1
@@ -184,8 +193,12 @@ module aptos_framework::aptos_account { | |||
|
|||
#[test(alice = @0xa11ce, core = @0x1)] | |||
public fun test_transfer(alice: &signer, core: &signer) { | |||
let bob = from_bcs::to_address(x"0000000000000000000000000000000000000000000000000000000000000b0b"); | |||
let carol = from_bcs::to_address(x"00000000000000000000000000000000000000000000000000000000000ca501"); | |||
let bob = |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The original code looks better.
|
||
let curr_auth_key = | ||
from_bcs::to_address(offerer_account_resource.authentication_key); | ||
let challenge = |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The original formatting does not exceed column limit, not sure why stuff after =
got moved to the new line.
For issues such as complex code indentation, which also is not handled flexibly and make sense enough in rustfmt. Our plan is to carry out specialized efforts in the future. I think it shouldn’t affect the overall situation, you can refer to it https://github.com/movebit/movefmt/blob/develop/doc/ChangeLog.md For the code under aptos-core, most formatted versions respect the source code. |
min_voting_threshold, | ||
required_proposer_stake, | ||
voting_duration_secs | ||
}, | ||
) | ||
},) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I feel like the symmetry is lost here because )
was moved up. I am pretty sure rustfmt e.g., would put this on the next line.
should_pass: bool, | ||
) { | ||
spec vote_internal(voter: &signer, stake_pool: address, proposal_id: u64, voting_power: u64, | ||
should_pass: bool,) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
minor nit: ,)
looks a bit weird.
Description
This PR shows the result after applying the newest movefmt to the framework code.