enable the x86 hol interactive workflow

Signed-off-by: Dusan Kostic <[email protected]>

Author: dkostic

.github/workflows/hol_light.yml

@@ -43,7 +43,7 @@ jobs:
   # but we use this as a fast path to not even start the proofs
   # if the byte code needs updating.
   hol_light_bytecode:
-    name: HOL-Light bytecode check
+    name: AArch64 HOL-Light bytecode check
     runs-on: pqcp-arm64
     if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
     steps:
@@ -57,7 +57,7 @@ jobs:
           script: |
             autogen --update-hol-light-bytecode --dry-run
   hol_light_interactive:
-    name: HOL-Light interactive shell test
+    name: AArch64 HOL-Light interactive shell test
     runs-on: pqcp-arm64
     needs: [ hol_light_bytecode ]
     if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
@@ -71,7 +71,7 @@ jobs:
           nix-shell: 'hol_light'
           script: |
             make -C proofs/hol_light/arm mlkem/mlkem_poly_tobytes.o
-            echo 'needs "proofs/mlkem_poly_tobytes.ml";;' | hol.sh
+            echo 'needs "arm/proofs/mlkem_poly_tobytes.ml";;' | hol.sh
   hol_light_proofs:
     needs: [ hol_light_bytecode ]
     strategy:
@@ -151,7 +151,7 @@ jobs:
 
   # x86_64 proofs
   hol_light_bytecode_x86_64:
-    name: HOL-Light bytecode check
+    name: x86_64 HOL-Light bytecode check
     runs-on: pqcp-x64
     if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
     steps:
@@ -164,23 +164,22 @@ jobs:
           nix-shell: 'hol_light'
           script: |
             autogen --update-hol-light-bytecode --dry-run
-  # TODO: fix the interactive mode to work for both x86 and arm.
-  # hol_light_interactive_x86_64:
-  #   name: HOL-Light interactive shell test
-  #   runs-on: pqcp-x64
-  #   needs: [ hol_light_bytecode_x86_64 ]
-  #   if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
-  #   steps:
-  #     - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
-  #       with:
-  #         fetch-depth: 0
-  #     - uses: ./.github/actions/setup-shell
-  #       with:
-  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
-  #         nix-shell: 'hol_light'
-  #         script: |
-  #           make -C proofs/hol_light/x86 mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o
-  #           echo 'needs "proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml";;' | hol.sh
+  hol_light_interactive_x86_64:
+    name: x86_64 HOL-Light interactive shell test
+    runs-on: pqcp-x64
+    needs: [ hol_light_bytecode_x86_64 ]
+    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
+    steps:
+      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+        with:
+          fetch-depth: 0
+      - uses: ./.github/actions/setup-shell
+        with:
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          nix-shell: 'hol_light'
+          script: |
+            make -C proofs/hol_light/x86 mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o
+            echo 'needs "x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml";;' | hol.sh
   hol_light_proofs_x86_64:
     needs: [ hol_light_bytecode_x86_64 ]
     strategy: