Merge pull request #2956 from FStarLang/guido_build

Some build+test system tweaks

Makefile

@@ -132,24 +132,37 @@ output:
 	+$(Q)$(MAKE) -C tests/ide/emacs accept
 	+$(Q)$(MAKE) -C tests/bug-reports output-accept
 
+# This rule is meant to mimic what the docker based CI does, but it
+# is not perfect. In particular it will not look for a diff on the
+# snapshot, nor run the build-standalone script.
 .PHONY: ci
 ci:
 	+$(Q)FSTAR_HOME=$(CURDIR) $(MAKE) ci-pre
 	+$(Q)FSTAR_HOME=$(CURDIR) $(MAKE) ci-post
 
+# This rule runs a CI job in a local container, exactly like is done for
+# CI.
 .PHONY: docker-ci
 docker-ci:
 	docker build -f .docker/standalone.Dockerfile --build-arg CI_THREADS=$(shell nproc) .
 
 .PHONY: ci-pre
-ci-pre:
+ci-pre: ci-rebootstrap ci-ocaml-test ci-ulib-in-fsharp
+
+.PHONY: ci-rebootstrap
+ci-rebootstrap:
 	+$(Q)$(MAKE) full-bootstrap FSTAR_BUILD_PROFILE=test
+
+.PHONY: ci-ocaml-test
+ci-ocaml-test: ci-rebootstrap
 	+$(Q)$(MAKE) -C src ocaml-unit-tests
-	+$(Q)$(MAKE) -C ulib ulib-in-fsharp    #build ulibfs
+
+.PHONY: ci-ulib-in-fsharp
+ci-ulib-in-fsharp: ci-rebootstrap
+	+$(Q)$(MAKE) -C ulib ulib-in-fsharp
 
 .PHONY: ci-post
 ci-post: ci-uregressions
-	+if [ -n "${FSTAR_CI_UREGRESSIONS_ULONG}" ]; then $(MAKE) ci-uregressions-ulong; fi
 
 .PHONY: ci-uregressions
 ci-uregressions:

examples/Makefile

@@ -5,16 +5,18 @@ include Makefile.include
 # These examples are excluded since the binary package can't verify
 # them.
 
+# Scheduling these first as some files take very long.
+ALL_EXAMPLE_DIRS += layeredeffects
+ALL_EXAMPLE_DIRS += dsls
+ALL_EXAMPLE_DIRS += data_structures
+
 ALL_EXAMPLE_DIRS += algorithms
 ALL_EXAMPLE_DIRS += calc
 ALL_EXAMPLE_DIRS += crypto
-ALL_EXAMPLE_DIRS += data_structures
 ALL_EXAMPLE_DIRS += demos
 ALL_EXAMPLE_DIRS += doublylinkedlist
-ALL_EXAMPLE_DIRS += dsls
 ALL_EXAMPLE_DIRS += generic
 ALL_EXAMPLE_DIRS += indexed_effects
-ALL_EXAMPLE_DIRS += layeredeffects
 ALL_EXAMPLE_DIRS += low-mitls-experiments
 ALL_EXAMPLE_DIRS += maths
 ALL_EXAMPLE_DIRS += metatheory

examples/tactics/Canon.fst

@@ -60,25 +60,25 @@ let lem4 (a b c : int) =
 (* The following tests should pass, but it's too slow to run them on every regression build, *)
 (* and the previous ones are probably enough *)
 
-let lem5 (a b c d e : int) =
-    assert
-        ((a+b+c+d+e)*(a+b+c+d+e) ==
-                a * a + a * b + a * c + a * d + a * e
-              + b * a + b * b + b * c + b * d + b * e
-              + c * a + c * b + c * c + c * d + c * e
-              + d * a + d * b + d * c + d * d + d * e
-              + e * a + e * b + e * c + e * d + e * e)
-        by check_canon ()
-
-let lem6 (a b c d e : int) =
-    assert
-        ((a+b+c+d+e)*(e+d+c+b+a) ==
-                a * a + a * b + a * c + a * d + a * e
-              + b * a + b * b + b * c + b * d + b * e
-              + c * a + c * b + c * c + c * d + c * e
-              + d * a + d * b + d * c + d * d + d * e
-              + e * a + e * b + e * c + e * d + e * e)
-        by check_canon ()
+// let lem5 (a b c d e : int) =
+//     assert
+//         ((a+b+c+d+e)*(a+b+c+d+e) ==
+//                 a * a + a * b + a * c + a * d + a * e
+//               + b * a + b * b + b * c + b * d + b * e
+//               + c * a + c * b + c * c + c * d + c * e
+//               + d * a + d * b + d * c + d * d + d * e
+//               + e * a + e * b + e * c + e * d + e * e)
+//         by check_canon ()
+//
+// let lem6 (a b c d e : int) =
+//     assert
+//         ((a+b+c+d+e)*(e+d+c+b+a) ==
+//                 a * a + a * b + a * c + a * d + a * e
+//               + b * a + b * b + b * c + b * d + b * e
+//               + c * a + c * b + c * c + c * d + c * e
+//               + d * a + d * b + d * c + d * d + d * e
+//               + e * a + e * b + e * c + e * d + e * e)
+//         by check_canon ()
 
 let lem7 (a b c d : int) =
     assert