CI: Check that HOL-Light bytecode is up to date

This commit adds to the unconditional CI job `ci.yml` a
check that the bytecode in the HOL-Light proof scripts is
up to date.

This was previously only checked by the HOL-Light workflow,
which however is only triggered on changes to the HOL-Light
files.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Author: hanno-becker

.github/workflows/ci.yml

@@ -693,3 +693,11 @@ jobs:
           gh_token: ${{ secrets.GITHUB_TOKEN }}
           script: |
             python3 ./scripts/autogen --dry-run --force-cross
+      - uses: ./.github/actions/setup-shell
+        # Building the HOL-Light bytecode currently requires native compilation
+        if: ${{ matrix.system == 'pqcp-arm64' }}
+        with:
+          nix-shell: 'hol_light'
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          script: |
+            python3 ./scripts/autogen --dry-run --update-hol-light-bytecode