include ulib .checked files again

FStarLang · May 26, 2021 · 2b25586 · 2b25586
1 parent d11d4be
commit 2b25586
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 25 deletions.
diff --git a/.docker/package.Dockerfile b/.docker/package.Dockerfile
@@ -32,9 +32,6 @@ RUN tar xzf fstar.tar.gz
 ENV FSTAR_HOME /home/opam/fstar
 ENV PATH="${FSTAR_HOME}/bin:${PATH}"
 
-# Reverify ulib, which was not in the package
-RUN eval $(opam env) && make -C $FSTAR_HOME/ulib clean_checked && make -C $FSTAR_HOME/ulib -j $opamthreads
-
 # Test the F* binary package
 
 # Case 1: test the fresh package
@@ -51,8 +48,8 @@ RUN eval $(opam env) && make -C $FSTAR_HOME/ulib clean_checked && make -C $FSTAR
 RUN eval $(opam env) && make -C $FSTAR_HOME/examples -j $opamthreads
 RUN eval $(opam env) && make -C $FSTAR_HOME/doc/tutorial -j $opamthreads regressions
 
-# Case 3: test the fresh package without OCaml
-FROM ubuntu:20.04
+# Test the fresh package without OCaml
+FROM ubuntu:20.04 AS fstarnoocaml
 ENV DEBIAN_FRONTEND=noninteractive
 RUN apt-get update
 RUN apt-get --yes install --no-install-recommends make sudo libgomp1
@@ -72,9 +69,16 @@ COPY --from=fstarbuild /home/opam/FStar/src/ocaml-output/fstar.tar.gz /home/test
 RUN tar xzf fstar.tar.gz
 ENV FSTAR_HOME /home/test/fstar
 ENV PATH="${FSTAR_HOME}/bin:${PATH}"
-RUN make -C $FSTAR_HOME/ulib clean_checked && make -C $FSTAR_HOME/ulib -j $opamthreads
 
-# Run tests
+# Case 3: test F* package without OCaml
+FROM fstarnoocaml
+RUN make -C $FSTAR_HOME/tests/micro-benchmarks -j $opamthreads
+RUN make -C $FSTAR_HOME/examples -j $opamthreads
+RUN make -C $FSTAR_HOME/doc/tutorial -j $opamthreads regressions
+
+# Case 4: test F* package without OCaml, but recheck ulib
+FROM fstarnoocaml
+RUN make -C $FSTAR_HOME/ulib clean_checked && make -C $FSTAR_HOME/ulib -j $opamthreads
 RUN make -C $FSTAR_HOME/tests/micro-benchmarks -j $opamthreads
 RUN make -C $FSTAR_HOME/examples -j $opamthreads
 RUN make -C $FSTAR_HOME/doc/tutorial -j $opamthreads regressions
diff --git a/.scripts/process_build.sh b/.scripts/process_build.sh
@@ -110,15 +110,6 @@ diag "-- Versions --"
 bin/fstar.exe --version
 bin/z3 --version
 
-diag "-- Verify ulib --"
-make -j6 -C ulib
-if [ $? -ne 0 ]; then
-  echo -e "* ${RED}FAIL!${NC} for ulib - make returned $?"
-  exit 1
-else
-  echo -e "* ${GREEN}PASSED!${NC} for ulib"
-fi
-
 diag "-- Verify micro benchmarks --"
 make -C tests/micro-benchmarks
 if [ $? -ne 0 ]; then

diff --git a/Makefile b/Makefile
@@ -2,12 +2,10 @@
 
 include .common.mk
 
-all: no-ulib-checked
-	$(Q)+$(MAKE) -C ulib
-
-no-ulib-checked:
+all:
 	$(Q)+$(MAKE) -C src/ocaml-output
 	$(Q)+$(MAKE) -C ulib/ml
+	$(Q)+$(MAKE) -C ulib
 
 install:
 	$(Q)+$(MAKE) -C src/ocaml-output install
@@ -27,10 +25,10 @@ uninstall:
 	  $(PREFIX)/bin/fstar.exe \
 	  $(PREFIX)/share/fstar
 
-package: no-ulib-checked
+package: all
 	$(Q)+$(MAKE) -C src/ocaml-output package
 
-package_unknown_platform: no-ulib-checked
+package_unknown_platform: all
 	$(Q)+$(MAKE) -C src/ocaml-output package_unknown_platform
 
 clean:

diff --git a/src/ocaml-output/Makefile b/src/ocaml-output/Makefile
@@ -264,9 +264,7 @@ package:
 	@# Install the F* binary
 	$(call fexport-all,bin)
 	@# Then the standard library.
-	$(call fexport,ulib)
-	$(INSTALL_EXEC) -m 644 ../../ulib/ml/FStar_Int*.ml $(PREFIX)/ulib/ml
-	$(INSTALL_EXEC) -m 644 ../../ulib/ml/FStar_UInt*.ml $(PREFIX)/ulib/ml
+	$(call fexport-all,ulib)
 	mkdir -p $(PREFIX)/src/ocaml-output/
 	cp ../../src/ocaml-output/FStar_Pervasives.ml $(PREFIX)/src/ocaml-output/
 	cp ../../version.txt $(PREFIX)/