Skip to content

push should likely push to latest HEAD, not the commit recorded in rust-version #46

@RalfJung

Description

@RalfJung

See this discussion: a long time ago when Miri was the only tool using josh, I made it so that the push logic roughly does the following:

  • Prepare a branch in RalfJung/rust that is set to exactly the commit currently configured in the rust-version file
  • Tell josh to push to that branch

If I remember correctly, I did this because I got some strange problems once when pushing to the latest rust-lang/rust HEAD and this made things more deterministic. However, this makes one non-trivial demand on Josh. Consider the case where one does two push syncs without an intermediate pull: the second push will now re-do the work of the first, since both of them are asked to reconstruct the subrepo history on the main repo from the same starting point. If for some reason Josh is not fully deterministic in how it reconstructs such history during a push, then the 2nd push will duplicate commits from the first. That is exactly what happened with RA in the Zulip thread linked above.

@christian-schilling recommends that we should push on top of the latest rust-lang/rust HEAD rather than the commit recorded in rust-version. That would avoid relying on determinism during push syncs. I don't know which strange problems I got when I decided to introduce this logic that always pushes on top of rust-version, but we can hope that if it happens again, it would be caught by the round-trip check.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions