diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 316a2289d2cdc85ac7c79be081e9a18177af8fc8..71fb3de73f1baeb83d47dec8d49d5ee47a0c2660 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -78,50 +78,45 @@ same by pinning `coq-iris` to your Iris checkout.)
Note that `./make-package` will never run the test suite, so please always do a
regular `make -jN` before submitting an MR.
-## How to measure the timing effect on a reverse dependency
-
-So say you did a change in Iris, and want to know how it affects [lambda-rust]
-or the [examples]. To do this, check out the respective project and change its
-`.gitlab-ci.yml` to contain only one build job, which should look like
+## How to test effects on reverse dependencies
+
+The `iris-bot` script makes it easy tot est the effect of a branch on reverse
+dependencies. It can start tests ensuring they all still build, and it can do
+comparative timing runs.
+
+But first, you need to do some setup: you need to create a GitLab access token
+and set the `GITLAB_TOKEN` environment variable to it. Go to
+<https://gitlab.mpi-sws.org/-/profile/personal_access_tokens>, pick a suitable
+name (such as "iris-bot"), select the "api" scope, and then click "Create
+personal access token". Copy the value it shows and store it in some suitable
+place, you will not be able to retrieve this value from GitLab in the future!
+For example, you could create a `.env` file in your Iris clone containing:
```
-build-iris.dev:
- <<: *template
- variables:
- OPAM_PINS: "coq version 8.12.0 git+https://gitlab.mpi-sws.org/iris/iris.git#yourname/feature"
- tags:
- - fp-timing
+export GITLAB_TOKEN=<your token here>
```
-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`. 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
-`ci/yourname/feature`. You should see a pipeline running in GitLab with just a
-single job, and you can follow its progress there.
-
-When the job is done, you should be able to see it as a single dot on our
-[statistics server][coq-speed] after selecting the right project and branch.
-Click on "Coq-Speed" on the top-left corner to switch to another dashboard, and
-select "Coq-Compare". Now you can select the project and the two measurements
-you want to compare, which would be the SHA of the commit you just created as
-"Commit 2", and the SHA of its parent as "Commit 1". Don't forget to also
-select the right configuration for both of them. The "Grouping" is a regular
-expression that you can use to switch between per-file, per-directory and
-per-project grouping of the measurements.
-
-If you changed your Iris branch and want to make another measurement, *do not*
-just "Retry" the CI job. That will lead to an error, because you would end up
-with two measurements for the same commit. Instead, create an empty commit in
-your branch of the to-be-measured project (`git commit --allow-empty -m
-"rerun"`), and push that.
-
-[lambda-rust]: https://gitlab.mpi-sws.org/iris/lambda-rust
+Then you can easily get the token back into the environment via `. .env`.
+
+Once that setup is done, you can now use `iris-bot`.
+Set at least one of `IRIS_REV` or `STDPP_REV` to control which branches of these
+projects to build against (default to default git branch). `IRIS_REPO` and
+`STDPP_REPO` can be used to take branches from forks. Setting `IRIS` to
+"user:branch" will use the given branch on that user's fork of Iris, and
+similar for `STDPP`
+
+Supported commands:
+- `./iris-bot build [$filter]`: Builds all reverse dependencies against the
+ given branches. The optional `filter` argument only builds projects whose
+ names contains that string.
+- `./iris-bot time $project`: Measure the impact of this branch on the build
+ time of the given reverse dependency. Only Iris branches are supported for
+ now.
+
+Examples:
+- `IRIS_REV=myname/mybranch ./iris-bot build` builds *all* reverse dependencies
+ against `myname/mybranch` from the main Iris repository.
+- `IRIS=user:branch ./iris-bot build examples` builds the [examples] against
+ the `branch` in `user`'s fork of Iris.
+- `IRIS_REV=myname/mybranch ./iris-bot time examples` measure the timing impact
+ of `myname/mybranch` from the main Iris repository on the [examples].
+
[examples]: https://gitlab.mpi-sws.org/iris/examples
-[coq-speed]: https://coq-speed.mpi-sws.org
diff --git a/build-all b/build-all
deleted file mode 100755
index f73b6079a85d203681182066528ec1f023c6eabc..0000000000000000000000000000000000000000
--- a/build-all
+++ /dev/null
@@ -1,69 +0,0 @@
-#!/usr/bin/python3
-import sys, os
-import requests
-
-# A script to build Iris' reverse-dependencies (the one that usually get built every night against Iris master)
-# against a branch of your choice.
-# Set the GITLAB_TOKEN environment variable to a GitLab access token.
-# Set at least one of IRIS_REV or STDPP_REV to control which branches of these projects to build against
-# (default to default git branch). IRIS_REPO and STDPP_REPO can be used to take branches from forks.
-# Setting IRIS to "user:branch" will use the given branch on that user's fork of Iris, and similar for STDPP.
-
-# Pre-processing for variables: you can set 'PROJECT' to 'user:branch',
-# or set 'PROJECT_REPO' and 'PROJECT_REV' automatically.
-PROJECT_VARS = ['STDPP', 'IRIS', 'ORC11', 'GPFSL']
-GITLAB_VARS = []
-
-for var in PROJECT_VARS:
- if var in os.environ:
- (repo, rev) = os.environ[var].split(':')
- repo = repo + "/" + var.lower()
- else:
- repo = os.environ.get(var+"_REPO")
- rev = os.environ.get(var+"_REV")
- # Add them to GITLAB_VARS
- if repo is not None:
- GITLAB_VARS.append({ 'key': var+"_REPO", 'value': repo })
- if rev is not None:
- GITLAB_VARS.append({ 'key': var+"_REV", 'value': rev })
-
-# Check if everything is set
-if not "GITLAB_TOKEN" in os.environ:
- print("You need to set the GITLAB_TOKEN environment variable to a GitLab access token.")
- print("You can create such tokens at <https://gitlab.mpi-sws.org/profile/personal_access_tokens>.")
- print("Make sure you grant access to the 'api' scope.")
- sys.exit(1)
-if not "IRIS_REV" in os.environ and not "IRIS" in os.environ:
- print("Please set IRIS_REV, STDPP_REV, ORC11_REV and GPFSL_REV environment variables to the branch/tag/commit of the respective project that you want to use.")
- print("Only IRIS_REV is mandatory, the rest defaults to the default git branch.")
- sys.exit(1)
-
-GITLAB_TOKEN = os.environ["GITLAB_TOKEN"]
-VARS = ['STDPP_REPO', 'STDPP_REV', 'IRIS_REPO', 'IRIS_REV', 'ORC11_REPO', 'ORC11_REV', 'GPFSL_REPO', 'GPFSL_REV']
-PROJECTS = [
- { 'name': 'lambda-rust', 'branch': 'master' },
- { 'name': 'lambda-rust', 'branch': 'masters/weak_mem' }, # covers GPFSL and ORC11
- { 'name': 'examples', 'branch': 'master' },
- { 'name': 'iron', 'branch': 'master' },
- { 'name': 'reloc', 'branch': 'master' },
- { 'name': 'spygame', 'branch': 'master' },
- { 'name': 'time-credits', 'branch': 'master' },
- { 'name': 'actris', 'branch': 'master' },
- { 'name': 'tutorial-popl20', 'branch': 'master' },
- { 'name': 'tutorial-popl21', 'branch': 'master' },
-]
-
-filter = sys.argv[1] if len(sys.argv) > 1 else ''
-for project in PROJECTS:
- name_branch = project['name'] + ('' if project['branch'] == 'master' else ':'+project['branch'])
- if filter in name_branch:
- print("Triggering build for {}...".format(name_branch))
- id = str(project['id']) if 'id' in project else "iris%2F{}".format(project['name'])
- url = "https://gitlab.mpi-sws.org/api/v4/projects/{}/pipeline".format(id)
- json = {
- 'ref': project['branch'],
- 'variables': GITLAB_VARS,
- }
- r = requests.post(url, headers={'PRIVATE-TOKEN': GITLAB_TOKEN}, json=json)
- r.raise_for_status()
- print(" Pipeline running at {}".format(r.json()['web_url']))
diff --git a/iris-bot b/iris-bot
new file mode 100755
index 0000000000000000000000000000000000000000..73a5a544f4ddd3a6152d7a19731a43e9e1cdd733
--- /dev/null
+++ b/iris-bot
@@ -0,0 +1,148 @@
+#!/usr/bin/python3
+import sys, os, subprocess
+import requests
+from datetime import datetime, timezone
+
+################################################################################
+# This script lets you autoamtically trigger some operations on the Iris CI to
+# do further test/analysis on a branch (usually an MR).
+# Set the GITLAB_TOKEN environment variable to a GitLab access token.
+# Set at least one of IRIS_REV or STDPP_REV to control which branches of these
+# projects to build against (default to default git branch). IRIS_REPO and
+# STDPP_REPO can be used to take branches from forks. Setting IRIS to
+# "user:branch" will use the given branch on that user's fork of Iris, and
+# similar for STDPP.
+#
+# Supported commands:
+# - `./iris-bot build [$filter]`: Builds all reverse dependencies against the
+# given branches. The optional `filter` argument only builds projects whose
+# names contains that string.
+# - `./iris-bot time $project`: Measure the impact of this branch on the build
+# time of the given reverse dependency. Only Iris branches are supported for
+# now.
+################################################################################
+
+PROJECTS = {
+ 'lambda-rust': { 'name': 'lambda-rust', 'branch': 'master', 'timing': True },
+ 'lambda-rust-weak': { 'name': 'lambda-rust', 'branch': 'masters/weak_mem' }, # covers GPFSL and ORC11
+ 'examples': { 'name': 'examples', 'branch': 'master', 'timing': True },
+ 'iron': { 'name': 'iron', 'branch': 'master' },
+ 'reloc': { 'name': 'reloc', 'branch': 'master' },
+ 'spygame': { 'name': 'spygame', 'branch': 'master' },
+ 'time-credits': { 'name': 'time-credits', 'branch': 'master' },
+ 'actris': { 'name': 'actris', 'branch': 'master' },
+ 'tutorial-popl20': { 'name': 'tutorial-popl20', 'branch': 'master' },
+ 'tutorial-popl21': { 'name': 'tutorial-popl21', 'branch': 'master' },
+}
+
+if not "GITLAB_TOKEN" in os.environ:
+ print("You need to set the GITLAB_TOKEN environment variable to a GitLab access token.")
+ print("You can create such tokens at <https://gitlab.mpi-sws.org/profile/personal_access_tokens>.")
+ print("Make sure you grant access to the 'api' scope.")
+ sys.exit(1)
+GITLAB_TOKEN = os.environ["GITLAB_TOKEN"]
+
+# Pre-processing for branch variables of dependency projects: you can set
+# 'PROJECT' to 'user:branch', or set 'PROJECT_REPO' and 'PROJECT_REV'
+# automatically.
+BUILD_BRANCHES = {}
+for project in ['stdpp', 'iris', 'orc11', 'gpfsl']:
+ var = project.upper()
+ if var in os.environ:
+ (repo, rev) = os.environ[var].split(':')
+ repo = repo + "/" + project
+ else:
+ repo = os.environ.get(var+"_REPO", "iris/"+project)
+ rev = os.environ.get(var+"_REV")
+ if rev is not None:
+ BUILD_BRANCHES[project] = (repo, rev)
+
+if not "iris" in BUILD_BRANCHES:
+ print("Please set IRIS_REV, STDPP_REV, ORC11_REV and GPFSL_REV environment variables to the branch/tag/commit of the respective project that you want to use.")
+ print("Only IRIS_REV is mandatory, the rest defaults to the default git branch.")
+ sys.exit(1)
+
+# Things Pythonr eally should have...
+def list_get(l, i, default=None):
+ return l[i] if len(l) > i else default
+
+# Useful helpers
+def trigger_build(project, branch, vars):
+ id = "iris%2F{}".format(project)
+ url = "https://gitlab.mpi-sws.org/api/v4/projects/{}/pipeline".format(id)
+ json = {
+ 'ref': branch,
+ 'variables': [{ 'key': key, 'value': val } for (key, val) in vars.items()],
+ }
+ r = requests.post(url, headers={'PRIVATE-TOKEN': GITLAB_TOKEN}, json=json)
+ r.raise_for_status()
+ return r.json()['web_url']
+
+# The commands
+def build():
+ # Convert BUILD_BRANCHES into suitable dictionary
+ vars = {}
+ for project in BUILD_BRANCHES.keys():
+ (repo, rev) = BUILD_BRANCHES[project]
+ var = project.upper()
+ vars[var+"_REPO"] = repo
+ vars[var+"_REV"] = rev
+ # Loop over all projects, and trigger build.
+ filter = list_get(sys.argv, 2, '')
+ for (name, project) in PROJECTS.items():
+ if filter in name:
+ print("Triggering build for {}...".format(name))
+ pipeline_url = trigger_build(project['name'], project['branch'], vars)
+ print(" Pipeline running at {}".format(pipeline_url))
+
+def time():
+ # Make sure only 'iris' variables are set.
+ for project in BUILD_BRANCHES.keys():
+ if project != 'iris':
+ print("'time' command only supports Iris branches")
+ sys.exit(1)
+ (iris_repo, iris_rev) = BUILD_BRANCHES['iris']
+ # Get project to test and ensure it supports timing
+ project_name = list_get(sys.argv, 2)
+ if project_name is None or project_name not in PROJECTS:
+ print("ERROR: a specific project must be used for timing")
+ sys.exit(1)
+ project = PROJECTS[project_name]
+ if not project.get('timing'):
+ print("ERROR: {} does not support timing".format(project_name))
+ sys.exit(1)
+ # Obtain a unique ID for this experiment
+ id = datetime.now(timezone.utc).strftime("%Y%m%d-%H%M%S")
+ # Determine the branch commit to build
+ subprocess.run(["git", "fetch", "-q", "https://gitlab.mpi-sws.org/{}".format(iris_repo), iris_rev], check=True)
+ test_commit = subprocess.run(["git", "rev-parse", "FETCH_HEAD"], check=True, stdout=subprocess.PIPE).stdout.decode().strip()
+ # Determine the base commit in master
+ subprocess.run(["git", "fetch", "-q", "origin"], check=True)
+ base_commit = subprocess.run(["git", "merge-base", test_commit, "origin/master"], check=True, stdout=subprocess.PIPE).stdout.decode().strip()
+ # Trigger the builds
+ print("Triggering timing builds for {} base commit ({}) and test commit ({}) with ad-hoc ID {}...".format(project_name, base_commit[:8], test_commit[:8], id))
+ vars = {
+ 'IRIS_REPO': iris_repo,
+ 'IRIS_REV': base_commit,
+ 'TIMING_AD_HOC_ID': id+"-base",
+ }
+ base_pipeline_url = trigger_build(project['name'], project['branch'], vars)
+ print(" Base pipeline running at {}".format(base_pipeline_url))
+ vars = {
+ 'IRIS_REPO': iris_repo,
+ 'IRIS_REV': test_commit,
+ 'TIMING_AD_HOC_ID': id+"-test",
+ }
+ test_pipeline_url = trigger_build(project['name'], project['branch'], vars)
+ print(" Test pipeline running at {}".format(test_pipeline_url))
+ print(" Once done, timing comparison will be available at https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project={}&var-branch1=@hoc&var-config1={}&var-branch2=@hoc&var-config2={}".format(project['name'], id+"-base", id+"-test"))
+
+# Dispatch
+command = list_get(sys.argv, 1, '')
+if command == 'build':
+ build()
+elif command == 'time':
+ time()
+else:
+ print("ERROR: unsupported or no command")
+ sys.exit(1)