Update interactive shell test

Signed-off-by: Jake Massimo <[email protected]>

Author: jakemas

.github/workflows/hol_light.yml

@@ -63,8 +63,11 @@ jobs:
           gh_token: ${{ secrets.GITHUB_TOKEN }}
           nix-shell: 'hol_light'
           script: |
-            make -C proofs/hol_light/x86_64 mldsa/mldsa_ntt.o
-            echo 'needs "proofs/mldsa_ntt.ml";;' | hol.sh
+            # Load base infrastructure and specs to validate HOL-Light environment
+            # When we have smaller/faster proofs, we can run them here instead:
+            # make -C proofs/hol_light/x86_64 mldsa/mldsa_ntt.o
+            # echo 'needs "proofs/mldsa_ntt.ml";;' | hol.sh
+            echo 'needs "x86/proofs/base.ml";; needs "proofs/mldsa_specs.ml";; #quit;;' | hol.sh
   hol_light_proofs:
     needs: [ hol_light_bytecode ]
     strategy: