chore: Parallelise construction of perturbator coefficients at each level #427

	# Mirror PRs labeled external-ci-approved. It will sync on every-reapply.
	name: Mirror PRs for External CI

	on:
	pull_request_target:
	types: [labeled]

	jobs:
	mirror-pr:
	runs-on: ubuntu-latest

	if: contains(github.event.pull_request.labels.*.name, 'external-ci-approved')

	steps:
	- name: Checkout
	uses: actions/checkout@v3
	with:
	fetch-depth: 0
	# TODO remove guesswork
	ref: ${{ github.event.pull_request.head.sha \|\| github.event.pull_request_target.head.sha }}
	token: ${{ secrets.AZTEC_BOT_GITHUB_TOKEN }}

	- name: Set up Git
	run: \|
	git config user.name "${{ github.actor }}"
	git config user.email "${{ github.actor }}@users.noreply.github.com"

	- name: Create or update the mirrored branch
	run: \|
	HASH=$(git rev-parse HEAD)
	git checkout -b mirrored/${{ github.head_ref }} \|\| git checkout mirrored/${{ github.head_ref }}
	git reset --hard $HASH
	git push origin mirrored/${{ github.head_ref }} --force

	- name: Create or update the mirrored pull request
	uses: peter-evans/create-pull-request@v5
	with:
	token: ${{ secrets.AZTEC_BOT_GITHUB_TOKEN }}
	base: master
	head: ${{ github.head_ref }}
	title: "Mirror PR: ${{ github.event.pull_request.title }}"
	body: "This PR has been created because #${{ github.event.pull_request.number }} has been labeled external-ci-approved. It will sync on every-reapply."
	draft: false
	branch: mirrored/${{ github.head_ref }}
	update_existing_pr: true

Provide feedback