Skip to content

Conversation

Kobzol
Copy link
Member

@Kobzol Kobzol commented Oct 2, 2025

If a pull is a no-op, the preparation commit that updates rust-version, along with the (possibly empty) merge commit, is kept if --allow-noop is passed.

CC @RalfJung

Fixes: #26

@RalfJung
Copy link
Member

RalfJung commented Oct 2, 2025 via email

@Kobzol Kobzol force-pushed the allow-noop-keep-state branch from 861eb48 to f64718c Compare October 2, 2025 09:39
@Kobzol
Copy link
Member Author

Kobzol commented Oct 2, 2025

The commit is only created if there are some empty merge commits from upstream, sometimes it's not even created.

I thought that what you suggest would complicate the implementation, but it actually makes it simpler 😆 So I changed it like you proposed.

@Kobzol
Copy link
Member Author

Kobzol commented Oct 2, 2025

Although, I wonder if it won't be an issue that rust-version will be set to the latest rustc commit, but potentially the empty merge commits from rustc will not be included in the subtree at that point. But I guess it shouldn't be an issue, the empty merge commits will just be added on the next (non-empty) pull.

@RalfJung
Copy link
Member

RalfJung commented Oct 2, 2025

The commit is only created if there are some empty merge commits from upstream, sometimes it's not even created.

Ah, good point.

There's a slight risk the next josh-push will act up because the commit it is based on (which is taken from rust-version) hasn't been fully integrated into the local history yet. But that seems unlikely and we should notice if this ever happens.

@Kobzol
Copy link
Member Author

Kobzol commented Oct 2, 2025

Alright, let's try it.

@Kobzol Kobzol merged commit 0e5d6ce into rust-lang:main Oct 2, 2025
1 check passed
@Kobzol Kobzol deleted the allow-noop-keep-state branch October 2, 2025 10:02
@RalfJung
Copy link
Member

RalfJung commented Oct 3, 2025

Pushing changes...
Rerun with `-v` to see executed commands
Error: cannot perform push

Caused by:
    Command `cd "/home/r/src/rust/miri" && "git" "push" "http://localhost:42042/RalfJung/rust.git:rev(75dd959a3a40eb5b4574f8d2e23aa6efbeb33573:prefix=src/tools/miri):/src/tools/miri.git" "HEAD:miri"` failed with exit code Some(1). STDOUT:
    
    STDERR:
    To http://localhost:42042/RalfJung/rust.git:rev(75dd959a3a40eb5b4574f8d2e23aa6efbeb33573:prefix=src/tools/miri):/src/tools/miri.git
     ! [rejected]            HEAD -> miri (non-fast-forward)
    error: failed to push some refs to 'http://localhost:42042/RalfJung/rust.git:rev(75dd959a3a40eb5b4574f8d2e23aa6efbeb33573:prefix=src/tools/miri):/src/tools/miri.git'
    hint: Updates were rejected because a pushed branch tip is behind its remote
    hint: counterpart. If you want to integrate the remote changes, use 'git pull'
    hint: before pushing again.
    hint: See the 'Note about fast-forwards' in 'git push --help' for details.

Yeah I guess it does cause issues.^^

(The fix is to pull again before making a push.)

@Kobzol
Copy link
Member Author

Kobzol commented Oct 3, 2025

That seems annoying. I'd rather remove the flag if it has such footgun. WDYT about keeping also the potential merge commit?

@RalfJung
Copy link
Member

RalfJung commented Oct 3, 2025

Yeah I think if josh-proxy returned new commits we should just have that merge commit then. We don't need a merge commit if josh-proxy returned the exact same commit that has already been merged before.

@Kobzol
Copy link
Member Author

Kobzol commented Oct 3, 2025

We don't need a merge commit if josh-proxy returned the exact same commit that has already been merged before.

That's easy, because in that case git doesn't evern create the merge commit.

#30 should fix this.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

"pull -f" mode that bumps the rust-version file even if nothing changed
2 participants