Merge pull request #4163 from mtzguido/fsharp

Fix F# lib, rules, and wire it in CI

Author: mtzguido

.github/workflows/tests.yml

@@ -81,6 +81,32 @@ jobs:
         # as that runs after the normal build and takes ~10 minutes.
         run: make -skj$(nproc) _test _test_pulse
 
+  # Build the F# library and the examples.
+  fsharp:
+    runs-on: ubuntu-latest
+    container: mtzguido/dev-base:v2
+    steps:
+      - name: Cleanup
+        run: sudo find . -delete
+      - run: echo "HOME=/home/user" >> $GITHUB_ENV
+      - uses: mtzguido/set-opam-env@master
+
+      - name: Checkout
+        uses: actions/checkout@master
+        with:
+          submodules: true
+
+      - name: Get fstar package
+        uses: actions/download-artifact@v8
+        with:
+          name: fstar.tar.gz
+
+      - name: Set up package locally
+        run: tar xzf fstar.tar.gz && ln -s fstar out
+
+      - name: Run tests, without forcing a build
+        run: make -skj$(nproc) fsharp-all FSTAR_EXE=$(pwd)/out/bin/fstar.exe
+
   # This runs the bare tests over the bare stage2 compiler.
   # We start from the built repo.
   bare:

Makefile

@@ -313,19 +313,23 @@ $(FSTAR2_FULL_EXE): .bare2.src.touch .full2.src.touch .src.ml.touch $(MAYBEFORCE
 	touch $@
 
 # F# library
-fsharp-lib.src: export FSTAR_EXE ?= $(FSTAR3_FULL_EXE)
-fsharp-lib.src: .alib2.src.touch .force
+fsharp-lib.src: export FSTAR_EXE ?= $(INSTALLED_FSTAR3_FULL_EXE)
+fsharp-lib.src: .force
 	# NB: shares checked files from .alib2.src,
 	# hence the dependency, though it is not quite precise.
 	$(call bold_msg, "EXTRACT", "FSHARP LIB")
 	# Note: FStar.Map and FStar.Set are special-cased
+	# Also note: we explicitly add an include for F*'s own library so it can
+	# find the checked files for it, and make this run about extraction
+	# only. The lib.mk makefile passes --no_default_includes.
 	env \
 	  SRC=ulib/ \
-	  CACHE_DIR=stage2/ulib.checked/ \
 	  OUTPUT_DIR=fsharp/extracted/ \
+	  CACHE_DIR=fsharp/_cached/ \
 	  CODEGEN=FSharp \
 	  TAG=fsharplib \
-	  DEPFLAGS='--extract -FStar.Map,-FStar.Set' \
+	  DEPFLAGS='--extract -FStar.Map,-FStar.Set --already_cached Prims,FStar' \
+	  OTHERFLAGS='--include $(shell $(FSTAR_EXE) --locate_lib)' \
 	  $(MAKE) -f mk/lib.mk all-fs
 
 .PHONY: fsharp-lib

fsharp/base/FStar_CommonST.fs

@@ -22,9 +22,6 @@
     <Compile Include="base/FStar_Dyn.fs" Link="FStar_Dyn.fs" />
     <Compile Include="base/FStar_Float.fs" Link="FStar_Float.fs" />
     <Compile Include="base/FStar_Ghost.fs" Link="FStar_Ghost.fs" />
-    <Compile Include="base/FStar_Monotonic_Heap.fs" Link="FStar_Monotonic_Heap.fs" />
-    <Compile Include="base/FStar_CommonST.fs" Link="FStar_CommonST.fs" />
-    <Compile Include="base/FStar_Heap.fs" Link="FStar_Heap.fs" />
     <Compile Include="base/FStar_Int16.fs" Link="FStar_Int16.fs" />
     <Compile Include="base/FStar_Int32.fs" Link="FStar_Int32.fs" />
     <Compile Include="base/FStar_Int64.fs" Link="FStar_Int64.fs" />
@@ -43,7 +40,6 @@
                2. Add 'type ordered = Type{hasOrder 'a}' or similar and use it instead of 'eqtype' in Set/Map interface.
     -->
     <Compile Include="base/FStar_Set.fs" Link="FStar_Set.fs" />
-    <Compile Include="base/FStar_ST.fs" Link="FStar_ST.fs" />
     <Compile Include="base/FStar_Exn.fs" Link="FStar_Exn.fs" />
     <Compile Include="base/FStar_String.fs" Link="FStar_String.fs" />
     <Compile Include="base/FStar_UInt16.fs" Link="FStar_UInt16.fs" />
@@ -62,7 +58,6 @@
     <Compile Link="FStar_StrongExcludedMiddle.fs" Include="extracted\FStar_StrongExcludedMiddle.fs" />
     <Compile Link="FStar_PropositionalExtensionality.fs" Include="extracted\FStar_PropositionalExtensionality.fs" />
     <Compile Link="FStar_PredicateExtensionality.fs" Include="extracted\FStar_PredicateExtensionality.fs" />
-    <Compile Link="FStar_Monotonic_Witnessed.fs" Include="extracted\FStar_Monotonic_Witnessed.fs" />
     <!-- TODO: (Warning 341) Expected parameter 'state of witnessed to be unused in its definition and eliminated -->
     <Compile Link="FStar_List_Tot_Properties.fs" Include="extracted\FStar_List_Tot_Properties.fs" />
     <Compile Include="base/FStar_Map.fs" Link="FStar_Map.fs" />
@@ -85,7 +80,6 @@
     <Compile Link="FStar_BigOps.fs" Include="extracted\FStar_BigOps.fs" />
     <Compile Link="FStar_Int128.fs" Include="extracted\FStar_Int128.fs" />
     <Compile Link="FStar_Integers.fs" Include="extracted\FStar_Integers.fs" />
-    <Compile Link="FStar_Ref.fs" Include="extracted\FStar_Ref.fs" />
    </ItemGroup>
   <ItemGroup>
     <PackageReference Update="FSharp.Core" Version="4.3.4" />