Merge pull request #3978 from mtzguido/ocaml-unit-tests

Restore internal (OCaml) unit tests

Author: mtzguido

.github/workflows/tests.yml

@@ -76,7 +76,7 @@ jobs:
       - name: Run tests, without forcing a build
         run: make -skj$(nproc) _test
 
-  # This runs the bare tests over the bare stage1 compiler.
+  # This runs the bare tests over the bare stage2 compiler.
   # We start from the built repo.
   bare:
     runs-on: ubuntu-latest
@@ -91,7 +91,24 @@ jobs:
         with:
           name: fstar-repo
 
-      - run: make -skj$(nproc) test-1-bare
+      - run: make -skj$(nproc) test-2-bare
+        working-directory: FStar
+
+  # The internal tests (src/tests)
+  internal:
+    runs-on: ubuntu-latest
+    container: mtzguido/dev-base
+    steps:
+      - name: Cleanup
+        run: sudo find . -delete
+      - run: echo "HOME=/home/user" >> $GITHUB_ENV
+      - uses: mtzguido/set-opam-env@master
+
+      - uses: mtzguido/gci-download@master
+        with:
+          name: fstar-repo
+
+      - run: make -skj$(nproc) stage2-unit-tests
         working-directory: FStar
 
   binary-smoke:

Makefile

@@ -9,7 +9,7 @@ include mk/common.mk
 FSTAR_DEFAULT_GOAL ?= build
 .DEFAULT_GOAL := $(FSTAR_DEFAULT_GOAL)
 
-all: stage1 stage2 stage3-bare lib-fsharp
+all: stage1 stage2 1.tests 2.tests stage3-bare lib-fsharp
 all-packages: package-1 package-2 package-src-1 package-src-2
 
 ### STAGES
@@ -38,12 +38,14 @@ FSTAR0_EXE ?= stage0/out/bin/fstar.exe
 # stage 1 libraries for the stage 2, which does not need them at all (currently?).
 #
 # I'd love a better alternative.
-FSTAR1_BARE_EXE := stage1/dune/_build/default/fstarc-bare/fstarc1_bare.exe
-FSTAR1_FULL_EXE := stage1/dune/_build/default/fstarc-full/fstarc1_full.exe
+FSTAR1_BARE_EXE           := stage1/dune/_build/default/fstarc-bare/fstarc1_bare.exe
+FSTAR1_FULL_EXE           := stage1/dune/_build/default/fstarc-full/fstarc1_full.exe
 INSTALLED_FSTAR1_FULL_EXE := stage1/out/bin/fstar.exe
-FSTAR2_BARE_EXE := stage2/dune/_build/default/fstarc-bare/fstarc2_bare.exe
-FSTAR2_FULL_EXE := stage2/dune/_build/default/fstarc-full/fstarc2_full.exe
+FSTAR2_BARE_EXE           := stage2/dune/_build/default/fstarc-bare/fstarc2_bare.exe
+FSTAR2_FULL_EXE           := stage2/dune/_build/default/fstarc-full/fstarc2_full.exe
 INSTALLED_FSTAR2_FULL_EXE := stage2/out/bin/fstar.exe
+TESTS1_EXE                := stage1/dune/_build/default/tests/fstarc1_tests.exe
+TESTS2_EXE                := stage2/dune/_build/default/tests/fstarc2_tests.exe
 
 .PHONY: .force
 .force:
@@ -59,10 +61,12 @@ endif
 build: 2
 
 0: $(FSTAR0_EXE)
-1.bare: $(FSTAR1_BARE_EXE)
-1.full: $(FSTAR1_FULL_EXE)
-2.bare: $(FSTAR2_BARE_EXE)
-2.full: $(FSTAR2_FULL_EXE)
+1.bare:  $(FSTAR1_BARE_EXE)
+1.tests: $(TESTS1_EXE)
+1.full:  $(FSTAR1_FULL_EXE)
+2.bare:  $(FSTAR2_BARE_EXE)
+2.tests: $(TESTS2_EXE)
+2.full:  $(FSTAR2_FULL_EXE)
 
 # This file's timestamp is updated whenever anything in stage0/
 # (excluding some build directories)
@@ -92,13 +96,27 @@ stage0/out/bin/fstar.exe: .stage0.touch
 	env \
 	  SRC=src/ \
 	  FSTAR_EXE=$(FSTAR0_EXE) \
+	  FSTAR_LIB=$(abspath ulib) \
 	  CACHE_DIR=stage1/fstarc.checked/ \
 	  OUTPUT_DIR=stage1/fstarc.ml/ \
 	  CODEGEN=OCaml \
 	  TAG=fstarc \
 	  TOUCH=$@ \
 	  $(MAKE) -f mk/fstar-01.mk ocaml
 
+.tests1.src.touch: .bare1.src.touch $(FSTAR0_EXE) .force
+	$(call bold_msg, "EXTRACT", "STAGE 1 TESTS")
+	env \
+	  SRC=src/ \
+	  FSTAR_EXE=$(FSTAR0_EXE) \
+	  FSTAR_LIB=$(abspath ulib) \
+	  CACHE_DIR=stage1/tests.checked/ \
+	  OUTPUT_DIR=stage1/tests.ml/ \
+	  CODEGEN=PluginNoLib \
+	  TAG=fstarc \
+	  TOUCH=$@ \
+	  $(MAKE) -f mk/tests-1.mk ocaml
+
 # These files are regenerated as soon as *any* ml file reachable from
 # stage*/dune changes. This makes sure we trigger dune rebuilds when we
 # modify base ML files. However this will not catch deletion of a file.
@@ -111,6 +129,14 @@ $(FSTAR1_BARE_EXE): .bare1.src.touch .src.ml.touch $(MAYBEFORCE)
 	$(MAKE) -C stage1 fstarc-bare
 	touch -c $@
 
+$(TESTS1_EXE): .tests1.src.touch .src.ml.touch $(MAYBEFORCE)
+	$(call bold_msg, "BUILD", "STAGE 1 TESTS")
+	$(MAKE) -C stage1 tests
+	touch -c $@
+
+stage1-unit-tests: $(TESTS1_EXE)
+	FSTAR_LIB=$(CURDIR)/ulib $(TESTS1_EXE)
+
 .full1.src.touch: $(FSTAR1_BARE_EXE) .force
 	$(call bold_msg, "EXTRACT", "STAGE 1 PLUGINS")
 	env \
@@ -183,6 +209,19 @@ $(FSTAR1_FULL_EXE): .bare1.src.touch .full1.src.touch .src.ml.touch $(MAYBEFORCE
 	  TOUCH=$@ \
 	  $(MAKE) -f mk/fstar-12.mk ocaml
 
+.tests2.src.touch: .bare2.src.touch $(FSTAR1_FULL_EXE) .force
+	$(call bold_msg, "EXTRACT", "STAGE 2 TESTS")
+	env \
+	  SRC=src/ \
+	  FSTAR_EXE=$(FSTAR1_FULL_EXE) \
+	  FSTAR_LIB=$(abspath ulib) \
+	  CACHE_DIR=stage2/tests.checked/ \
+	  OUTPUT_DIR=stage2/tests.ml/ \
+	  CODEGEN=PluginNoLib \
+	  TAG=fstarc \
+	  TOUCH=$@ \
+	  $(MAKE) -f mk/tests-2.mk ocaml
+
 $(FSTAR2_BARE_EXE): .bare2.src.touch .src.ml.touch $(MAYBEFORCE)
 	$(call bold_msg, "BUILD", "STAGE 2 FSTARC-BARE")
 	$(MAKE) -C stage2 fstarc-bare FSTAR_DUNE_RELEASE=1
@@ -191,6 +230,14 @@ $(FSTAR2_BARE_EXE): .bare2.src.touch .src.ml.touch $(MAYBEFORCE)
 	# it is still part of the build of the full fstar, so
 	# we set the release flag to have a more incremental build.
 
+$(TESTS2_EXE): .tests2.src.touch .src.ml.touch $(MAYBEFORCE)
+	$(call bold_msg, "BUILD", "STAGE 2 TESTS")
+	$(MAKE) -C stage2 tests
+	touch -c $@
+
+stage2-unit-tests: $(TESTS2_EXE)
+	FSTAR_LIB=$(CURDIR)/ulib $(TESTS2_EXE)
+
 .full2.src.touch: $(FSTAR2_BARE_EXE) .force
 	$(call bold_msg, "EXTRACT", "STAGE 2 PLUGINS")
 	env \
@@ -385,14 +432,14 @@ package-2: .stage2.src.touch .force
 	  INSTALL_RULE=__do-install-stage2 \
 	  $(MAKE) __do-archive
 
-package-src-1: .stage1.src.touch .force
+package-src-1: .stage1.src.touch .tests1.src.touch .force
 	env \
 	  PKGTMP=_srcpak1 \
 	  BROOT=stage1/ \
 	  ARCHIVE=fstar$(FSTAR_TAG)-stage1-src \
 	  $(MAKE) __do-src-archive
 
-package-src-2: .stage2.src.touch .force
+package-src-2: .stage2.src.touch .tests2.src.touch .force
 	env \
 	  PKGTMP=_srcpak2 \
 	  BROOT=stage2/ \
@@ -451,7 +498,7 @@ _examples: need_fstar_exe .force
 
 ci: .force
 	+$(MAKE) 2
-	+$(MAKE) test lib-fsharp stage3-diff
+	+$(MAKE) test lib-fsharp stage3-diff test-2-bare stage2-unit-tests
 
 save: stage0_new
 

mk/stage.mk

@@ -31,6 +31,9 @@ endif
 fstarc-bare: _force
 	cd dune && $(DUNE) build $(FSTAR_DUNE_BUILD_OPTIONS) fstarc-bare
 
+tests: _force
+	cd dune && $(DUNE) build $(FSTAR_DUNE_BUILD_OPTIONS) tests
+
 fstarc-full: _force
 	cd dune && $(DUNE) build $(FSTAR_DUNE_BUILD_OPTIONS) fstarc-full
 

mk/tests-1.mk

@@ -0,0 +1,26 @@
+FSTAR_OPTIONS += --lax
+# HACK ALERT! --MLish passed by generic.mk to FStarC modules
+# only. Passing it here would mean the library is checked with
+# --MLish, which fails.
+FSTAR_OPTIONS += --MLish_effect 'FStarC.Effect'
+
+DEPFLAGS += --already_cached '+Prims,+FStar,+FStarC,-FStarC.Tests'
+
+DEPFLAGS += --already_cached '-FStar'
+# ^ FIXME: This should be removed. All of the modules we *actually* depend on
+# in the FStar namespace are indeed already checked. But, if we claim that, the
+# dependency analysis will complain about modules such as
+# FStar.Stubs.Reflection.V2.Builtins not being checked, which is irrelevant.
+
+# All other files have been extracted already into fstar-guts.
+EXTRACT :=
+EXTRACT += --extract +FStarC.Tests
+
+# hack, reuse checked files from guts
+OTHERFLAGS += --include $(CACHE_DIR)/../fstarc.checked
+DEPFLAGS += --include $(CACHE_DIR)/../fstarc.checked
+
+ROOTS :=
+ROOTS += $(SRC)/tests/FStarC.Tests.Test.fst
+
+include mk/generic-0.mk

mk/tests-2.mk

@@ -0,0 +1,20 @@
+FSTAR_OPTIONS += --lax
+# HACK ALERT! --MLish passed by generic.mk to FStarC modules
+# only. Passing it here would mean the library is checked with
+# --MLish, which fails.
+FSTAR_OPTIONS += --MLish_effect 'FStarC.Effect'
+
+DEPFLAGS += --already_cached '+FStarC.*,-FStarC.Tests.*'
+
+# All other files have been extracted already into fstar-guts.
+EXTRACT :=
+EXTRACT += --extract +FStarC.Tests
+
+# hack, reuse checked files from guts
+OTHERFLAGS += --include $(CACHE_DIR)/../fstarc.checked
+DEPFLAGS += --include $(CACHE_DIR)/../fstarc.checked
+
+ROOTS :=
+ROOTS += $(SRC)/tests/FStarC.Tests.Test.fst
+
+include mk/generic-1.mk

src/basic/FStarC.Options.fst

@@ -43,12 +43,6 @@ module Ext = FStarC.Options.Ext
 let debug_embedding = mk_ref false
 let eager_embedding = mk_ref false
 
-(* A FLAG TO INDICATE THAT WE'RE RUNNING UNIT TESTS *)
-let __unit_tests__ = mk_ref false
-let __unit_tests() = !__unit_tests__
-let __set_unit_tests () = __unit_tests__ := true
-let __clear_unit_tests () = __unit_tests__ := false
-
 let as_bool = function
   | Bool b -> b
   | _ -> failwith "Impos: expected Bool"

src/basic/FStarC.Options.fsti

@@ -102,9 +102,6 @@ val set_verification_options    : optionstate -> unit
 "--z3rlimit 25 --include /some/path" *)
 val show_options                : unit -> string
 
-val __unit_tests                : unit    -> bool
-val __set_unit_tests            : unit    -> unit
-val __clear_unit_tests          : unit    -> unit
 val parse_cmd_line              : unit    -> parse_cmdline_res & list string
 val add_verify_module           : string  -> unit