Merge pull request #3441 from mtzguido/pulse_ci

Adding Pulse bootstrapping test to check-world
FStarLang · Sep 5, 2024 · 7fd387d · 7fd387d
2 parents 715128c + bb81e9f
commit 7fd387d
Showing 1 changed file with 17 additions and 56 deletions.
diff --git a/.github/workflows/check-world.yml b/.github/workflows/check-world.yml
@@ -39,6 +39,7 @@ jobs:
         with:
           name: FStar
           extra: --exclude=FStar/ocaml/_build
+          hometag: FSTAR
 
   test-fstar:
     runs-on: ubuntu-latest
@@ -53,7 +54,6 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
 
       - name: Test
         run: make -C FStar -skj$(nproc) ci-uregressions
@@ -88,6 +88,13 @@ jobs:
           cd FStar/
           ./.scripts/check-snapshot-diff.sh
 
+      - uses: mtzguido/gci-upload@master
+        with:
+          name: FStar-boot
+          path: FStar
+          extra: --exclude=FStar/ocaml/_build
+          hometag: FSTAR
+
   build-krml:
     runs-on: ubuntu-latest
     container: mtzguido/fstar-base-testing
@@ -101,7 +108,6 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
 
       - name: Checkout karamel
         uses: actions/checkout@master
@@ -147,6 +153,7 @@ jobs:
         with:
           name: karamel
           extra: --exclude=karamel/_build
+          hometag: KRML
 
   test-krml:
     runs-on: ubuntu-latest
@@ -163,12 +170,10 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
 
       - uses: mtzguido/gci-download@master
         with:
           name: karamel
-          hometag: KRML
 
       - name: Test
         run: make -C karamel -skj$(nproc) test
@@ -188,12 +193,10 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
 
       - uses: mtzguido/gci-download@master
         with:
           name: karamel
-          hometag: KRML
 
       - name: Checkout steel
         uses: actions/checkout@master
@@ -207,6 +210,7 @@ jobs:
       - uses: mtzguido/gci-upload@master
         with:
           name: steel
+          hometag: STEEL
 
   test-steel:
     runs-on: ubuntu-latest
@@ -224,17 +228,14 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
 
       - uses: mtzguido/gci-download@master
         with:
           name: karamel
-          hometag: KRML
 
       - uses: mtzguido/gci-download@master
         with:
           name: steel
-          hometag: STEEL
 
       - name: Test
         run: make -C steel -skj$(nproc) test
@@ -244,7 +245,6 @@ jobs:
     container: mtzguido/fstar-base-testing
     needs:
       - build-fstar
-      - build-krml
     steps:
       - name: Cleanup
         run: find . -delete
@@ -254,12 +254,6 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
-
-      - uses: mtzguido/gci-download@master
-        with:
-          name: karamel
-          hometag: KRML
 
       - name: Checkout pulse
         uses: actions/checkout@master
@@ -273,13 +267,13 @@ jobs:
       - uses: mtzguido/gci-upload@master
         with:
           name: pulse
+          hometag: PULSE
 
   test-pulse-boot:
     runs-on: ubuntu-latest
     container: mtzguido/fstar-base-testing
     needs:
-      - build-fstar
-      - build-krml
+      - test-fstar-boot
     steps:
       - name: Cleanup
         run: find . -delete
@@ -288,13 +282,7 @@ jobs:
 
       - uses: mtzguido/gci-download@master
         with:
-          name: FStar
-          hometag: FSTAR
-
-      - uses: mtzguido/gci-download@master
-        with:
-          name: karamel
-          hometag: KRML
+          name: FStar-boot
 
       - name: Checkout pulse
         uses: actions/checkout@master
@@ -308,7 +296,7 @@ jobs:
           # check the library.
           make -C pulse/src -skj$(nproc) clean-snapshot
           make -C pulse/src -skj$(nproc) extract
-          make -C pulse/src -skj$(nproc) build
+          make -C pulse/src -skj$(nproc) build-ocaml
 
       - name: Check diff
         run: |
@@ -331,17 +319,14 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
 
       - uses: mtzguido/gci-download@master
         with:
           name: karamel
-          hometag: KRML
 
       - uses: mtzguido/gci-download@master
         with:
           name: pulse
-          hometag: PULSE
 
       - name: Test
         run: make -C pulse -skj$(nproc) test
@@ -362,12 +347,10 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
 
       - uses: mtzguido/gci-download@master
         with:
           name: karamel
-          hometag: KRML
 
       - name: Checkout hacl-star
         uses: actions/checkout@master
@@ -389,6 +372,7 @@ jobs:
       - uses: mtzguido/gci-upload@master
         with:
           name: hacl-star
+          hometag: HACL
 
   test-hacl:
     runs-on: ubuntu-latest
@@ -406,17 +390,14 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
 
       - uses: mtzguido/gci-download@master
         with:
           name: karamel
-          hometag: KRML
 
       - uses: mtzguido/gci-download@master
         with:
           name: hacl-star
-          hometag: HACL
 
       - name: Get Vale (again)
         run: ./hacl-star/tools/get_vale.sh
@@ -439,12 +420,10 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
 
       - uses: mtzguido/gci-download@master
         with:
           name: karamel
-          hometag: KRML
 
       - name: Checkout everparse
         uses: actions/checkout@master
@@ -461,6 +440,7 @@ jobs:
       - uses: mtzguido/gci-upload@master
         with:
           name: everparse
+          hometag: EVERPARSE
 
   test-everparse:
     runs-on: ubuntu-latest
@@ -478,17 +458,14 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
 
       - uses: mtzguido/gci-download@master
         with:
           name: karamel
-          hometag: KRML
 
       - uses: mtzguido/gci-download@master
         with:
           name: everparse
-          hometag: EVERPARSE
 
       - name: Test
         run: make -C everparse -skj$(nproc) test
@@ -510,22 +487,18 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
 
       - uses: mtzguido/gci-download@master
         with:
           name: karamel
-          hometag: KRML
 
       - uses: mtzguido/gci-download@master
         with:
           name: everparse
-          hometag: EVERPARSE
 
       - uses: mtzguido/gci-download@master
         with:
           name: hacl-star
-          hometag: HACL
 
       - name: Checkout merkle-tree
         uses: actions/checkout@master
@@ -561,22 +534,18 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
 
       - uses: mtzguido/gci-download@master
         with:
           name: karamel
-          hometag: KRML
 
       - uses: mtzguido/gci-download@master
         with:
           name: everparse
-          hometag: EVERPARSE
 
       - uses: mtzguido/gci-download@master
         with:
           name: hacl-star
-          hometag: HACL
 
       - uses: mtzguido/gci-download@master
         with:
@@ -602,22 +571,18 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
 
       - uses: mtzguido/gci-download@master
         with:
           name: karamel
-          hometag: KRML
 
       - uses: mtzguido/gci-download@master
         with:
           name: everparse
-          hometag: EVERPARSE
 
       - uses: mtzguido/gci-download@master
         with:
           name: hacl-star
-          hometag: HACL
 
       - name: Checkout mitls-fstar
         uses: actions/checkout@master
@@ -631,6 +596,7 @@ jobs:
       - uses: mtzguido/gci-upload@master
         with:
           name: mitls-fstar
+          hometag: MITLS
 
   test-mitls-fstar:
     runs-on: ubuntu-latest
@@ -650,27 +616,22 @@ jobs:
       - uses: mtzguido/gci-download@master
         with:
           name: FStar
-          hometag: FSTAR
 
       - uses: mtzguido/gci-download@master
         with:
           name: karamel
-          hometag: KRML
 
       - uses: mtzguido/gci-download@master
         with:
           name: everparse
-          hometag: EVERPARSE
 
       - uses: mtzguido/gci-download@master
         with:
           name: hacl-star
-          hometag: HACL
 
       - uses: mtzguido/gci-download@master
         with:
           name: mitls-fstar
-          hometag: MITLS
 
       - name: Build
         run: make -C mitls-fstar/src/tls -skj$(nproc) test