Merge pull request #3653 from mtzguido/checkw

Fixes to check-world, and a nightly build
FStarLang · Jan 6, 2025 · 0d377d4 · 0d377d4
2 parents 57797ed + cde2c28
commit 0d377d4
Show file tree

Hide file tree

Showing 4 changed files with 40 additions and 43 deletions.
diff --git a/.github/workflows/check-world.yml b/.github/workflows/check-world.yml
@@ -66,6 +66,8 @@ on:
   # push:
   workflow_dispatch:
   workflow_call:
+  schedule:
+    - cron: '0 1 * * *' # 1AM UTC
 
 # TODO:
 # Is there a way to set the default container?
@@ -302,7 +304,7 @@ jobs:
     runs-on: ubuntu-latest
     container: mtzguido/fstar-base-testing
     needs:
-      - build-fstar
+      - test-fstar-boot
     steps:
       - name: Cleanup
         run: find . -delete
@@ -311,7 +313,7 @@ jobs:
 
       - uses: mtzguido/gci-download@master
         with:
-          name: FStar
+          name: FStar-boot
 
       - name: Checkout pulse
         uses: actions/checkout@master
@@ -327,40 +329,6 @@ jobs:
           name: pulse
           hometag: PULSE
 
-  test-pulse-boot:
-    runs-on: ubuntu-latest
-    container: mtzguido/fstar-base-testing
-    needs:
-      - test-fstar-boot
-    steps:
-      - name: Cleanup
-        run: find . -delete
-      - run: echo "HOME=/home/opam" >> $GITHUB_ENV
-      - uses: mtzguido/set-opam-env@master
-
-      - uses: mtzguido/gci-download@master
-        with:
-          name: FStar-boot
-
-      - name: Checkout pulse
-        uses: actions/checkout@master
-        with:
-          path: pulse/
-          repository: FStarLang/pulse
-
-      - name: Build
-        run: |
-          # This is similar for 'make full-boot', but does not
-          # 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-ocaml
-
-      - name: Check diff
-        run: |
-          cd pulse/
-          ./.scripts/check-snapshot-diff.sh
-
   test-pulse:
     runs-on: ubuntu-latest
     container: mtzguido/fstar-base-testing
@@ -374,9 +342,15 @@ jobs:
       - run: echo "HOME=/home/opam" >> $GITHUB_ENV
       - uses: mtzguido/set-opam-env@master
 
+      # Install rust toolchain
+      - run: sudo apt-get update && sudo apt-get install -y curl
+      - uses: dtolnay/rust-toolchain@stable
+      - run: cargo install bindgen-cli # needed for tests
+      - run: sudo apt-get install -y llvm-dev libclang-dev clang # for pulse2rust
+
       - uses: mtzguido/gci-download@master
         with:
-          name: FStar
+          name: FStar-boot
 
       - uses: mtzguido/gci-download@master
         with:
@@ -764,7 +738,7 @@ jobs:
     container: mtzguido/fstar-base-testing
     needs:
       - build-fstar
-      - build-krml
+      # - build-krml
       - build-pulse
     steps:
       - name: Cleanup
@@ -773,20 +747,38 @@ jobs:
       - uses: mtzguido/set-opam-env@master
 
       # Install rust toolchain
+      - run: sudo apt-get update && sudo apt-get install -y curl
       - uses: dtolnay/rust-toolchain@stable
 
       - uses: mtzguido/gci-download@master
         with:
-          name: FStar
+          name: FStar-boot
 
-      - uses: mtzguido/gci-download@master
+      # karamel was built with the FStar artifact, not FStar-boot. If we
+      # try to use it, the build later fails due to a dependence hash
+      # mismatch. The error is probably bogus and due to absolute paths
+      # or some similar discrepancy, but we just avoid it by rebuilding
+      # karamel.
+
+      # - uses: mtzguido/gci-download@master
+      #   with:
+      #     name: karamel
+      - name: Checkout karamel
+        uses: actions/checkout@master
         with:
-          name: karamel
+          path: karamel/
+          repository: FStarLang/karamel
+      - run: make -C karamel -skj$(nproc)
+      - run: echo "KRML_HOME=$(pwd)/karamel" >> $GITHUB_ENV
 
       - uses: mtzguido/gci-download@master
         with:
           name: pulse
 
+      # everparse expects PULSE_HOME to be the root of the installation,
+      # not the root of the repo
+      - run: echo "PULSE_HOME=$PULSE_HOME/out" >> $GITHUB_ENV
+
       - name: Checkout everparse (cbor branch)
         uses: actions/checkout@master
         with:

diff --git a/src/Makefile b/src/Makefile
@@ -28,7 +28,11 @@ clean_boot:
 # And ocaml-output/Makefile, to actually build the compiler in OCaml
 # --------------------------------------------------------------------------------
 ocaml:
-	$(Q)+$(MAKE) -f Makefile.boot all-ml
+	# Note: we add all-checked in support of Pulse and other
+	# projects that code against compiler internals, to make
+	# sure we generate all possible .checked files, instead of
+	# just the ones needed for extracting.
+	$(Q)+$(MAKE) -f Makefile.boot all-ml all-checked
 
 clean-ocaml: clean_boot
 	+$(Q)$(MAKE) -C ocaml-output clean

diff --git a/src/Makefile.boot b/src/Makefile.boot
@@ -109,3 +109,4 @@ depend: .depend
 include .depend
 
 all-ml: $(ALL_ML_FILES)
+all-checked: $(ALL_CHECKED_FILES)
diff --git a/src/extraction/FStarC.Extraction.ML.PrintML.fst b/src/extraction/FStarC.Extraction.ML.PrintML.fst
@@ -29,4 +29,4 @@ This file is here for the F# build. *)
 let print (_: option string) (ext: string) (l: mllib) =
     let newDoc = FStarC.Extraction.ML.Code.doc_of_mllib l in
     List.iter (fun (n,d) ->
-        FStarC.Compiler.Util.write_file (FStarC.Options.prepend_output_dir (n^ext)) (FStarC.Extraction.ML.Code.pretty 120 d)) newDoc
+        FStarC.Compiler.Util.write_file (FStarC.Find.prepend_output_dir (n^ext)) (FStarC.Extraction.ML.Code.pretty 120 d)) newDoc
Original file line number	Diff line number	Diff line change
Expand Up		@@ -109,3 +109,4 @@ depend: .depend
		include .depend

		all-ml: $(ALL_ML_FILES)
		all-checked: $(ALL_CHECKED_FILES)