Merge pull request #4193 from FStarLang/gebner_switch_boot_order

Reorder bootstrapping: use current ulib for compiler and plugins

Author: gebner

Makefile

@@ -41,22 +41,16 @@ endif
 FSTAR0_EXE ?= stage0/out/bin/fstar.exe
 
 # This is hardcoding some dune paths, with internal (non-public) names.
-# This is motivated by dune installing packages as a unit, so I could not
-# install simply the bare compiler and then use it to build the full compiler
-# without splitting into many packages, which complicates the namespaces.
 #
-# Also, when we want to extract src/ for stage 2, we must call FSTAR1_FULL_EXE,
+# When we want to extract src/ for stage 2, we must call FSTAR1_FULL_EXE,
 # but it's in a bad location (without a library next to it). So, we must
-# pass FSTAR_LIB explicitly. This is the only case where this is needed, the rest
-# of stages don't need a library. The alternative is to install it, and use
+# pass FSTAR_LIB explicitly. The alternative is to install it, and use
 # $(INSTALLED_FSTAR1_FULL_EXE), but that introduces a spurious dependency to the
 # 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
 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
 INSTALLED_FSTAR2_FULL_EXE := stage2/out/bin/fstar.exe
 # Stage3 = Stage2 + Pulse
@@ -79,13 +73,11 @@ endif
 build: 3
 
 0: $(FSTAR0_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)
-# No tests or bare for stage3
+# No tests for stage3
 3.full:  $(FSTAR3_FULL_EXE)
 
 
@@ -108,15 +100,15 @@ build: 3
 
 stage0/out/bin/fstar.exe: .stage0.touch
 	$(call bold_msg, "STAGE 0")
-	mkdir -p stage0/ulib/.cache # prevent warnings
-	$(MAKE) -C stage0 minimal # build: only fstar.exe and set-up lib sources
+	$(MAKE) -C stage0 install_bin # build: only fstar.exe
 	$(MAKE) -C stage0 trim # We don't need OCaml build files.
 
 .bare1.src.touch: $(FSTAR0_EXE) .force
-	$(call bold_msg, "EXTRACT", "STAGE 1 FSTARC-BARE")
+	$(call bold_msg, "EXTRACT", "STAGE 1 FSTARC")
 	env \
 	  SRC=src/ \
 	  FSTAR_EXE=$(FSTAR0_EXE) \
+	  FSTAR_LIB=$(abspath ulib) \
 	  CACHE_DIR=stage1/fstarc.checked/ \
 	  OUTPUT_DIR=stage1/fstarc.ml/ \
 	  CODEGEN=OCaml \
@@ -129,6 +121,7 @@ stage0/out/bin/fstar.exe: .stage0.touch
 	env \
 	  SRC=src/ \
 	  FSTAR_EXE=$(FSTAR0_EXE) \
+	  FSTAR_LIB=$(abspath ulib) \
 	  CACHE_DIR=stage1/tests.checked/ \
 	  OUTPUT_DIR=stage1/tests.ml/ \
 	  CODEGEN=PluginNoLib \
@@ -143,11 +136,6 @@ stage0/out/bin/fstar.exe: .stage0.touch
 	[ -e $@ ] || touch $@
 	find -L src/ml -newer $@ -exec touch $@ \; -quit
 
-$(FSTAR1_BARE_EXE): .bare1.src.touch .src.ml.touch $(MAYBEFORCE)
-	$(call bold_msg, "BUILD", "STAGE 1 FSTARC-BARE")
-	$(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 BUILD_FSTAR_OCAML_TESTS=true
@@ -156,11 +144,11 @@ $(TESTS1_EXE): .tests1.src.touch .src.ml.touch $(MAYBEFORCE)
 stage1-unit-tests: $(TESTS1_EXE)
 	FSTAR_LIB=$(CURDIR)/ulib $(TESTS1_EXE)
 
-.full1.src.touch: $(FSTAR1_BARE_EXE) .force
+.full1.src.touch: $(FSTAR0_EXE) .force
 	$(call bold_msg, "EXTRACT", "STAGE 1 PLUGINS")
 	env \
 	  SRC=ulib/ \
-	  FSTAR_EXE=$(FSTAR1_BARE_EXE) \
+	  FSTAR_EXE=$(FSTAR0_EXE) \
 	  CACHE_DIR=stage1/plugins.checked/ \
 	  OUTPUT_DIR=stage1/plugins.ml/ \
 	  CODEGEN=PluginNoLib \
@@ -241,14 +229,6 @@ $(FSTAR1_FULL_EXE): .bare1.src.touch .full1.src.touch .src.ml.touch $(MAYBEFORCE
 	  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
-	touch -c $@
-	# ^ Note, even if we don't release fstar-bare itself,
-	# 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 BUILD_FSTAR_OCAML_TESTS=true
@@ -257,11 +237,12 @@ $(TESTS2_EXE): .tests2.src.touch .src.ml.touch $(MAYBEFORCE)
 stage2-unit-tests: $(TESTS2_EXE)
 	FSTAR_LIB=$(CURDIR)/ulib $(TESTS2_EXE)
 
-.full2.src.touch: $(FSTAR2_BARE_EXE) .force
+.full2.src.touch: $(FSTAR1_FULL_EXE) .force
 	$(call bold_msg, "EXTRACT", "STAGE 2 PLUGINS")
 	env \
 	  SRC=ulib/ \
-	  FSTAR_EXE=$(FSTAR2_BARE_EXE) \
+	  FSTAR_EXE=$(FSTAR1_FULL_EXE) \
+	  FSTAR_LIB=$(abspath ulib) \
 	  CACHE_DIR=stage2/plugins.checked/ \
 	  OUTPUT_DIR=stage2/plugins.ml/ \
 	  CODEGEN=PluginNoLib \
@@ -376,6 +357,12 @@ endif
 .stage2.src.touch: .bare2.src.touch .full2.src.touch .alib2.src.touch .plib2.src.touch .src.ml.touch
 	touch $@
 
+.stage1-for-bump.src.touch: .bare1.src.touch .full1.src.touch .src.ml.touch
+	touch $@
+
+.stage2-for-bump.src.touch: .bare2.src.touch .full2.src.touch .src.ml.touch
+	touch $@
+
 .pulse-plugin.src.touch: stage2
 	env \
 	  FSTAR_EXE=$(abspath $(INSTALLED_FSTAR2_FULL_EXE)) \
@@ -548,15 +535,15 @@ package-src-3: .stage3.src.touch .tests2.src.touch .force
 package: package-3
 package-src: package-src-3
 
-test-1-bare: override FSTAR_EXE := $(abspath $(FSTAR1_BARE_EXE))
+test-1-bare: override FSTAR_EXE := $(abspath $(INSTALLED_FSTAR1_FULL_EXE))
 test-1-bare: override FSTAR_LIB := $(abspath ulib)
-test-1-bare: $(FSTAR1_BARE_EXE)
-	$(MAKE) -C bare-tests
+test-1-bare: stage1
+	$(MAKE) -C bare-tests FSTAR_EXE=$(FSTAR_EXE) FSTAR_LIB=$(FSTAR_LIB)
 
-test-2-bare: override FSTAR_EXE := $(abspath $(FSTAR2_BARE_EXE))
+test-2-bare: override FSTAR_EXE := $(abspath $(INSTALLED_FSTAR2_FULL_EXE))
 test-2-bare: override FSTAR_LIB := $(abspath ulib)
-test-2-bare: $(FSTAR2_BARE_EXE)
-	$(MAKE) -C bare-tests
+test-2-bare: stage2
+	$(MAKE) -C bare-tests FSTAR_EXE=$(FSTAR_EXE) FSTAR_LIB=$(FSTAR_LIB)
 
 test: test-3
 
@@ -640,46 +627,53 @@ ci: .force
 
 save: stage0_new
 
-stage0_new: TO=stage0_new
-stage0_new: .stage2.src.touch
+# Shared logic for creating a stage0 snapshot from a given stage.
+define do-stage0-snapshot
 	$(call bold_msg, "SNAPSHOT", "$(TO)")
 	rm -rf "$(TO)"
-	.scripts/src-install.sh "stage2" "$(TO)"
+	mkdir -p "$(1)"/ulib.ml "$(1)"/ulib.pluginml  # rsync fails with dangling symlinks
+	.scripts/src-install.sh "$(1)" "$(TO)"
 	# Trim it a bit...
 	rm -rf "$(TO)/src"            # no need for compiler F* sources
-	rm -rf "$(TO)/ulib/.hints"    # this library won't be checked
-	rm -rf "$(TO)/ulib.pluginml"  # we won't build plugins against stage0
+	rm -rf "$(TO)/ulib"*          # stage0 does not need its own ulib copy
 	rm -rf "$(TO)/dune/libplugin" # idem
 	rm -rf "$(TO)/dune/libapp"    # we won't even build apps
 	rm -rf "$(TO)/dune/tests"     # we won't build tests
 	rm -rf "$(TO)/karamel"        # only needed in source packages
+endef
 
-bump-stage0: stage0_new
+stage0_new: TO=stage0_new
+stage0_new: .stage2-for-bump.src.touch
+	$(call do-stage0-snapshot,stage2)
+
+# Faster alternative: snapshot from stage1 (only requires building stage1).
+stage0_new_from_stage1: TO=stage0_new
+stage0_new_from_stage1: .stage1-for-bump.src.touch
+	$(call do-stage0-snapshot,stage1)
+
+# Shared logic for finalizing a stage0 bump.
+define do-bump-stage0
 	$(call bold_msg, "BUMP!")
 	# Replace stage0
 	rm -rf stage0
 	mv stage0_new stage0
 	echo 'out' >> stage0/.gitignore
 	echo '** -diff -merge linguist-generated=true' >> stage0/.gitattributes
 	# Now that stage0 supports all features, we can return to a clean state
-	# where the 01 makefile is equal to the 12 makefile. Same for stage1
-	# support and config code, we just take it from the stage2.
+	# where the 01 makefile is equal to the 12 makefile.
 	rm -f mk/generic-0.mk
 	ln -sf generic-1.mk mk/generic-0.mk
 	cp mk/fstar-12.mk mk/fstar-01.mk
 	sed -i 's,include mk/generic-1.mk,include mk/generic-0.mk,' mk/fstar-01.mk
-	rm -rf stage1
-	cp -r stage2 stage1
-	rm -rf stage1/dune/_build
-	# Rename dune executables: stage1 must use fstarc1_*, not fstarc2_*
-	sed -i 's/fstarc2_/fstarc1_/g' stage1/dune/fstarc-bare/dune
-	sed -i 's/fstarc2_/fstarc1_/g' stage1/dune/fstarc-full/dune
-	sed -i 's/fstarc2_/fstarc1_/g' stage1/dune/tests/dune
-	mv stage1/dune/fstarc-bare/fstarc2_bare.ml stage1/dune/fstarc-bare/fstarc1_bare.ml
-	mv stage1/dune/fstarc-full/fstarc2_full.ml stage1/dune/fstarc-full/fstarc1_full.ml
-	mv stage1/dune/tests/fstarc2_tests.ml      stage1/dune/tests/fstarc1_tests.ml
 	rm -f stage1/dune/fstar-guts/app
-	ln -Trsf stage0/ulib/ml/app stage1/dune/fstar-guts/app
+	ln -Trsf ulib/ml/app stage1/dune/fstar-guts/app
+endef
+
+bump-stage0: stage0_new
+	$(do-bump-stage0)
+
+bump-stage0-from-stage1: stage0_new_from_stage1
+	$(do-bump-stage0)
 
 # This rule brings a stage0 from an OLD fstar repo. Only useful for migrating.
 bring-stage0: .force
@@ -688,9 +682,6 @@ bring-stage0: .force
 	mkdir stage0
 	cp -r $(FROM)/ocaml -T stage0
 	ln -Tsrf mk/stage0.mk stage0/Makefile
-	cp -r $(FROM)/ulib -T stage0/ulib
-	find stage0/ulib -name '*.checked' -delete
-	find stage0/ulib -name '*.hints' -delete
 	echo '/lib' >> stage0/.gitignore
 	echo '** -diff -merge' >> stage0/.gitattributes
 	echo '** linguist-generated=true' >> stage0/.gitattributes
@@ -718,7 +709,6 @@ clean-depend: .force
 clean-0: .force
 	$(call bold_msg, "CLEAN", "STAGE 0")
 	$(MAKE) -C stage0 clean
-	rm -rf stage0/ulib/.cache # created only to prevent warnings, always empty
 
 define clean-stage
 	$(call bold_msg, "CLEAN", "STAGE $(1)")

bare-tests/Cfg.fst.config.json

@@ -1,5 +1,5 @@
 {
-  "fstar_exe": "../stage1/dune/_build/default/fstarc-bare/fstarc1_bare.exe",
+  "fstar_exe": "../stage1/dune/_build/default/fstarc-full/fstarc1_full.exe",
   "options": [
     "--no_prelude"
   ],

bare-tests/Makefile

@@ -16,7 +16,7 @@ OTHERFLAGS += --warn_error -241
 # warnings about missing checked files since it will mess up the output.
 
 FSTAR_ROOT ?= ..
-FSTAR_EXE ?= $(abspath $(FSTAR_ROOT)/stage1/dune/_build/default/fstarc-bare/fstarc1_bare.exe)
+FSTAR_EXE ?= $(abspath $(FSTAR_ROOT)/stage1/dune/_build/default/fstarc-full/fstarc1_full.exe)
 export FSTAR_LIB ?= $(abspath $(FSTAR_ROOT)/ulib)
 include $(FSTAR_ROOT)/mk/test.mk
 

doc/ref/bootstrapping.md

@@ -0,0 +1,86 @@
+# Bootstrapping
+
+The F\* compiler is written in F\*, extracted to OCaml, and compiled
+with dune.  The build uses a multi-stage bootstrapping process to
+ensure that the compiler can compile itself.
+
+## Components
+
+The compiler has three main components:
+
+- **Compiler** (`src/`): The F\* compiler source code (FStarC.\*
+  modules), extracted to OCaml.
+- **Plugins** (`ulib/`): Tactic and metaprogramming plugins
+  (FStar.Tactics.\*, etc.), extracted from the standard library using
+  `--codegen PluginNoLib`.
+- **Standard library** (`ulib/`): The F\* standard library (Prims,
+  FStar.\* modules), verified and extracted to OCaml.
+
+## Stages
+
+### Stage 0
+
+A pre-built OCaml snapshot of the compiler, stored in `stage0/`.  It
+contains extracted OCaml sources and a dune build configuration, but
+no copy of the standard library.  Stage 0 is periodically updated via
+`make bump-stage0`.
+
+### Stage 1
+
+Built by the stage 0 compiler using the current ulib:
+
+1. **Extract compiler**: stage 0 lax-checks `src/` using the current
+   `ulib/` (via `FSTAR_LIB`) and extracts OCaml.
+2. **Extract plugins**: stage 0 lax-checks the plugin modules in
+   `ulib/` and extracts them.
+3. **Build**: dune compiles the extracted compiler + plugins into the
+   stage 1 executable.
+4. **Verify ulib**: stage 1 fully verifies and extracts the standard
+   library.
+
+### Stage 2
+
+Same structure as stage 1, but built by the stage 1 compiler.  This
+is the stage that is checked for bootstrapping stability: the
+`boot-diff` target re-extracts the compiler with the stage 2 compiler
+and verifies that the output matches stage 2's own extracted sources.
+
+### Stage 3
+
+Stage 2 plus the Pulse separation logic DSL (baked-in as a plugin).
+This is the compiler that is released and tested.
+
+## Key Make targets
+
+| Target | Description |
+|---|---|
+| `make build` (= `make 3`) | Build through stage 3 |
+| `make 1` / `make 2` | Build stage 1 / stage 2 and set `out/` symlink |
+| `make ci` | Build stage 2, run tests, boot-diff, fsharp |
+| `make test` | Run tests with stage 3 |
+| `make boot-diff` | Verify bootstrapping stability (stage 2 vs 2+1) |
+| `make bump-stage0` | Update stage 0 snapshot from stage 2 ML files |
+| `make bump-stage0-from-stage1` | Update stage 0 snapshot from stage 1 (faster) |
+
+## Bumping stage 0
+
+When changes to the compiler source (`src/`) or standard library
+(`ulib/`) require updating the stage 0 snapshot:
+
+```sh
+make bump-stage0              # snapshot from stage 2 (full bootstrap)
+make bump-stage0-from-stage1  # snapshot from stage 1 (faster)
+```
+
+The stage 1 variant is faster since it only requires building one
+stage instead of two.  Both snapshot the extracted OCaml into
+`stage0/` and reset `mk/fstar-01.mk` and `mk/generic-0.mk` to
+match their stage 1→2 counterparts.
+
+## Source packages
+
+Source packages (built via `make package-src`) are self-contained
+OCaml distributions that can be built without a pre-existing F\*
+compiler.  They use `stage0/Makefile` (= `mk/src_package_mk.mk`)
+which builds the compiler, verifies the library, and installs
+everything.

examples/algorithms/StringMatching.fst

@@ -124,7 +124,7 @@ let lemma_mod_add_3 (a b c:int) (p:pos)
 = lemma_mod_add_distr_l (a + b) c p;
   lemma_mod_add_distr_l (a + c) b p
 
-#push-options "--z3rlimit_factor 10 --ifuel 0 --fuel 2 --split_queries no"
+#push-options "--z3rlimit_factor 10 --ifuel 0 --fuel 2 --split_queries always"
 #restart-solver
 // This is the main utility lemma on the hash function
 // It allows inverting the hash to inspect the most significant digit

mk/stage.mk

@@ -28,9 +28,6 @@ else
 DUNE=dune
 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
 

stage1/dune/fstar-guts/app

@@ -1 +1 @@
-../../../stage0/ulib/ml/app
+../../../ulib/ml/app