@@ -231,25 +231,16 @@ You can also directly run Miri on a Rust source file:
231231## Advanced topic: Syncing with the rustc repo
232232
233233We use the [ ` josh ` proxy] ( https://github.com/josh-project/josh ) to transmit changes between the
234- rustc and Miri repositories.
234+ rustc and Miri repositories. You can install it as follows:
235235
236236``` sh
237237cargo +stable install josh-proxy --git https://github.com/josh-project/josh --tag r22.12.06
238- josh-proxy --local=$HOME /.cache/josh --remote=https://github.com --no-background
239238```
240239
241- This uses a directory ` $HOME/.cache/josh ` as a cache, to speed up repeated pulling/pushing.
242-
243- To make josh push via ssh instead of https, you can add the following to your ` .gitconfig ` :
244-
245- ``` toml
246- [url "git@github .com:" ]
247- pushInsteadOf = https://github.com/
248- ```
240+ Josh will automatically be started and stopped by ` ./miri ` .
249241
250242### Importing changes from the rustc repo
251243
252- Josh needs to be running, as described above.
253244We assume we start on an up-to-date master branch in the Miri repo.
254245
255246``` sh
@@ -268,16 +259,14 @@ needed.
268259
269260### Exporting changes to the rustc repo
270261
271- Keep in mind that pushing is the most complicated job that josh has to do --
272- pulling just filters the rustc history, but pushing needs to construct a new
273- rustc history that would filter to the given Miri history! To avoid problems, it
274- is a good idea to always pull immediately before you push. In particular, you
275- should never do two josh pushes without an intermediate pull; that can lead to
276- duplicated commits.
262+ Keep in mind that pushing is the most complicated job that josh has to do -- pulling just filters
263+ the rustc history, but pushing needs to construct a new rustc history that would filter to the given
264+ Miri history! To avoid problems, it is a good idea to always pull immediately before you push. If
265+ you are getting strange errors, chances are you are running into [ this josh
266+ bug] ( https://github.com/josh-project/josh/issues/998 ) . In that case, please get in touch on Zulip.
277267
278- Josh needs to be running, as described above. We will use the josh proxy to push
279- to your fork of rustc. Run the following in the Miri repo, assuming we are on an
280- up-to-date master branch:
268+ We will use the josh proxy to push to your fork of rustc. Run the following in the Miri repo,
269+ assuming we are on an up-to-date master branch:
281270
282271``` sh
283272# Push the Miri changes to your rustc fork (substitute your github handle for YOUR_NAME).
@@ -287,3 +276,11 @@ up-to-date master branch:
287276This will create a new branch called 'miri' in your fork, and the output should
288277include a link to create a rustc PR that will integrate those changes into the
289278main repository.
279+
280+ If this fails due to authentication problems, it can help to make josh push via ssh instead of
281+ https. Add the following to your ` .gitconfig ` :
282+
283+ ``` toml
284+ [url "git@github .com:" ]
285+ pushInsteadOf = https://github.com/
286+ ```
0 commit comments