CI never sets AGDA_COMMIT in certain runs

[andreasabel]

This is the current logic to set AGDA_COMMIT: https://github.com/agda/agda-stdlib/blob/3a1bda24f1949c6fe0ba85d686745dcf246513a8/.github/workflows/ci-ubuntu.yml#L74-L84 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

• https://github.com/agda/agda-stdlib/pull/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.