CI never sets AGDA_COMMIT in certain runs

[andreasabel]

This is the current logic to set AGDA_COMMIT:

agda-stdlib/.github/workflows/ci-ubuntu.yml

Lines 74 to 84 in 3a1bda2

	if [[ '${{ github.ref }}' == 'refs/heads/master' \
	|| '${{ github.base_ref }}' == 'master' ]]; then
	# Pick Agda version for master
	echo "AGDA_COMMIT=tags/v2.6.4" >> $GITHUB_ENV;
	echo "AGDA_HTML_DIR=html/master" >> $GITHUB_ENV
	elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \
	|| '${{ github.base_ref }}' == 'experimental' ]]; then
	# Pick Agda version for experimental
	echo "AGDA_COMMIT=4d36cb37f8bfb765339b808b13356d760aa6f0ec" >> $GITHUB_ENV;
	echo "AGDA_HTML_DIR=html/experimental" >> $GITHUB_ENV
	fi

This is how it pans out: https://github.com/agda/agda-stdlib/actions/runs/6688745401/job/18171228466#step:2:2

   if [[ 'refs/heads/gh-readonly-queue/master/pr-2185-aba7a8abd6908ad1126c4c0e3216b9c3a354ab47' == 'refs/heads/master' \
     || '' == 'master' ]]; then
    # Pick Agda version for master
    echo "AGDA_COMMIT=tags/v2.6.4" >> $GITHUB_ENV;
    echo "AGDA_HTML_DIR=html/master" >> $GITHUB_ENV
  elif [[ 'refs/heads/gh-readonly-queue/master/pr-2185-aba7a8abd6908ad1126c4c0e3216b9c3a354ab47' == 'refs/heads/experimental' \
       || '' == 'experimental' ]]; then
    # Pick Agda version for experimental
    echo "AGDA_COMMIT=4d36cb37f8bfb765339b808b13356d760aa6f0ec" >> $GITHUB_ENV;
    echo "AGDA_HTML_DIR=html/experimental" >> $GITHUB_ENV
  fi

You can see that none of the conditions becomes true here.

[gallais]

What is the suggested fix? We cannot know which version of Agda to use a priori.

[andreasabel]

Seems like @MatthewDaggitt is already working on this in

• Bump Haskell CI (original!) to latest minor GHC versions #2187

But, dunno. Could you have agda as a submodule`? Can repos be submodules of each other?

[MatthewDaggitt]

I've set it to use master by default which gets us off the ground for now. But yes, we need a solution to this if we want to start merging things in experimental again.