diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 43ffe2770ff6213eb0d5222b8fad52c71d4c6cbd..3296de266b51b7a0a1102426d7b6f082ac268d00 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -88,19 +88,19 @@ or the [examples]. To do this, check out the respective project and change its build-iris.dev: <<: *template variables: - OPAM_PINS: "coq version 8.9.0 coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#yourname/feature" + OPAM_PINS: "coq version 8.9.0 coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#yourname/feature coq-iris-heap-lang.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#yourname/feature" tags: - fp-timing ``` You will have to adjust this a bit: you should use the same Coq version as whatever the master branch uses for its timing job, which you can determine by -checking its `.gitlab-ci.yml`. If you change the Coq version, remember to do it -in both places (`OPAM_PINS` and `TIMING_CONF`). You will also have to adjust -the Iris branch being used, which is determined after the `#` in `OPAM_PINS`. -If you are in doubt, ask on Mattermost *before* pushing your branch. Please -double-check that the job name is `build-iris.dev` to avoid polluting the caches -of regular CI builds! This way, you are going to share the cache with the -nightly builds, which is fine. +checking its `.gitlab-ci.yml`. You will also have to adjust the Iris branch +being used, which is determined after the `#` in `OPAM_PINS`. If the repo you +are testing does not need HeapLang, you can remove the `coq-iris-heap-lang` part +of `OPAM_PINS`. If you are in doubt, ask on Mattermost *before* pushing your +branch. Please double-check that the job name is `build-iris.dev` to avoid +polluting the caches of regular CI builds! This way, you are going to share the +cache with the nightly builds, which is fine. Once you are confident with your CI configuration, push this to a new branch whose name starts with `ci/`. It should usually be of the form