@@ -231,25 +231,16 @@ You can also directly run Miri on a Rust source file:
231
231
## Advanced topic: Syncing with the rustc repo
232
232
233
233
We 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:
235
235
236
236
``` sh
237
237
cargo +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
239
238
```
240
239
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 ` .
249
241
250
242
### Importing changes from the rustc repo
251
243
252
- Josh needs to be running, as described above.
253
244
We assume we start on an up-to-date master branch in the Miri repo.
254
245
255
246
``` sh
@@ -268,16 +259,14 @@ needed.
268
259
269
260
### Exporting changes to the rustc repo
270
261
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.
277
267
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:
281
270
282
271
``` sh
283
272
# Push the Miri changes to your rustc fork (substitute your github handle for YOUR_NAME).
@@ -287,3 +276,11 @@ up-to-date master branch:
287
276
This will create a new branch called 'miri' in your fork, and the output should
288
277
include a link to create a rustc PR that will integrate those changes into the
289
278
main 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