Subtree update automation: do not use git subtree merge --squash

[tautschnig]

git subtree merge --squash will always reset the subtree to the state of the tree that is being merged from, which effectively eradicates all our local changes. This was just masked by merge conflicts arising as we were always attempted to merge from some long-ago version as we hadn't consistently kept "git-subtree-split" markers.

This PR now amends the pull request descriptions to make sure we retain the necessary information and uses git merge instead of the subtree command.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[carolynzech]

Have you tested this on your fork? This looks reasonable, but it'd be nice to have some testing before merging.

[tautschnig]

Have you tested this on your fork? This looks reasonable, but it'd be nice to have some testing before merging.

Ack - I have tested this locally, but I will test once we have #290 merged and an updated toolchain in Kani. Putting this in draft mode for the time being.

[tautschnig]

This is now ready for review. See https://github.com/tautschnig/verify-rust-std/actions/runs/14104094023 (creating PRs tautschnig#16 and tautschnig#17) and https://github.com/tautschnig/verify-rust-std/actions/runs/14104444534 (creating PR tautschnig#18 as a test that things also work fine when there is a pre-existing update PR for the subtree/library branch) for the logs of successful runs.

[tautschnig]

I have now re-run this in my fork after updating my fork's subtree/library branch as the above PRs had a surprisingly large number of commits and changes. tautschnig#19 now makes a lot more sense, and tautschnig#20 does have the matching number of lines changed (actually, 2 more, as expected, for we are also updating the config files). The excessive number of commits in the latter PR is to be expected as we are doing a merge across seemingly unrelated histories for all the past subtree updates squashed changes. The actually changes, however, seem to be fine.

[carolynzech]

Thanks for all the work debugging this! The 10,000 commits is unfortunate, but I don't have any better solutions, and since we squash and merge anyway the important thing is that the diff looks good (which it does).

[qinheping]

LGTM thank you!