Merge branch 'master' into guido_norm

bin/run_benchmark.sh

@@ -71,25 +71,27 @@ EOF
 
 write_simple_summary() {
     IN=${1}
-    OUT=${1}.summary
-    echo ${IN} > ${OUT}
-
-    if ! $PERFILE; then
-        # Default, sum everything and summarize
-        awk -F',' '
-            BEGIN {total=0; user=0; sys=0; mem=0}
-            BEGIN {printf "%-10s %10s %10s %10s %10s\n", "N_benches", "total", "user", "system", "mem(mb)"}
-            NR>1 {total+=$2; user+=$3; sys+=$4; mem+=$5}
-            END { printf "%-10d %10g %10g %10g %10d\n", NR-1,total, user, sys, mem/1000}' \
-            < ${IN}.csv >> ${OUT}
-    else
-        # One line per file
-        awk -F',' '
-            BEGIN {printf "%-40s %10s %10s %10s %10s\n", "file", "total", "user", "system", "mem(kb)"}
-            NR>1  {printf "%-40s %10g %10g %10g %10d\n", $1, $2, $3, $4, $5}' \
-            < ${IN}.csv >> ${OUT}
-    fi
-    echo "Wrote results in ${OUT}"
+    AGG=${1}.summary
+    IND=${1}.perfile
+
+    # Sum everything and summarize into X.summary
+    awk -F',' '
+        BEGIN {total=0; user=0; sys=0; mem=0}
+        BEGIN {printf "%-10s %10s %10s %10s %10s\n", "N_benches", "total", "user", "system", "mem(mb)"}
+        NR>1 {total+=$2; user+=$3; sys+=$4; mem+=$5}
+        END { printf "%-10d %10g %10g %10g %10d\n", NR-1,total, user, sys, mem/1000}' \
+        < ${IN}.csv > ${AGG}
+    echo "Wrote ${AGG}"
+
+    # Place individual results into X.perfile, sorted by total time
+    cat ${IN}.csv |
+    tail -n+2 |
+    sort -n -k 2 -t, -r |
+    awk -F',' '
+        BEGIN {printf "%-40s %10s %10s %10s %10s\n", "file", "total", "user", "system", "mem(kb)"}
+        NR>1  {printf "%-40s %10g %10g %10g %10d\n", $1, $2, $3, $4, $5}' \
+        > ${IND}
+    echo "Wrote ${IND}"
 }
 
 write_csv() {
@@ -158,7 +160,7 @@ bench_dir () {
 
     if $RUN; then
         # Remove old .bench files
-        find "${BENCH_DIR}/" -name '*.bench' -delete
+        find "${BENCH_DIR}" -name '*.bench' -delete
 
         ${BENCH_WRAP} make -j${JLEVEL} -C "${BENCH_DIR}" "${RULE}" BENCHMARK_CMD=orun OTHERFLAGS="${BENCH_OTHERFLAGS}" 2>&1 | tee ${BENCH_OUTDIR}/${NAME}.log
     fi
@@ -176,17 +178,16 @@ BENCH_OTHERFLAGS=${BENCH_OTHERFLAGS-"--admit_smt_queries true"}
 BENCH_WRAP=${BENCH_WRAP-}
 
 # BENCH_OUTDIR is the location of the output directory
-BENCH_OUTDIR=${BENCH_OUTDIR-"./bench_results/"`date +'%Y%m%d_%H%M%S'`}
+BENCH_OUTDIR="./bench_results/"`date +'%Y%m%d_%H%M%S'`
 
 CLEAN=false
 AUTO=true
-PERFILE=false
 RUN=true
 JLEVEL=1
 
 # First pass for options
-OPTIONS=co:h1nj:
-LONGOPTS=clean,odir:,help,custom:,perfile,norun
+OPTIONS=co:hnj:
+LONGOPTS=clean,odir:,help,custom:,norun
 PARSED=$(getopt --options=$OPTIONS --longoptions=$LONGOPTS --name "$0" -- "$@")
 
 eval set -- "$PARSED"
@@ -208,11 +209,6 @@ while true; do
             exit 1
             ;;
 
-        -1|--perfile)
-            PERFILE=true
-            shift
-            ;;
-
         -n|--norun)
             RUN=false
             shift
@@ -262,26 +258,19 @@ To install a local pinned copy of orun do the following:
  $ cd sandmark/orun
  $ opam install  "
 
-mkdir -p ${BENCH_OUTDIR}
-
-if $CLEAN; then
-    clean_slate
-fi
-
 # Second pass for options, only handles --custom which needs to run after the others
 OPTIONS=
 LONGOPTS=custom:
 PARSED=$(getopt --options=$OPTIONS --longoptions=$LONGOPTS --name "$0" -- "$@")
 
+CUSTOMS=
+
 eval set -- "$PARSED"
 
 while true; do
     case "$1" in
         --custom)
-            DIR=$(echo "$2" | cut -d, -f1)
-            NAME=$(echo "$2" | cut -d, -f2)
-            RULE=$(echo "$2" | cut -d, -f3)
-            bench_dir "$DIR" "$NAME" "$RULE"
+            CUSTOMS+=($2)
             AUTO=false
             shift 2
             ;;
@@ -299,10 +288,23 @@ while true; do
 done
 
 if [[ $# -ne 0 ]]; then
-    echo "bad args remaining: $@"
+    echo "Unexpected argument: '$1'"
     exit 0
 fi
 
+mkdir -p ${BENCH_OUTDIR}
+
+if $CLEAN; then
+    clean_slate
+fi
+
+for i in ${CUSTOMS[*]}; do
+    DIR=$(echo "$i" | cut -d, -f1)
+    NAME=$(echo "$i" | cut -d, -f2)
+    RULE=$(echo "$i" | cut -d, -f3)
+    bench_dir "$DIR" "$NAME" "$RULE"
+done
+
 # If not --custom, run the default set of benchmarks
 if $AUTO; then
     bench_dir "tests/micro-benchmarks" "micro-benchmarks" "all"

examples/Makefile.common

@@ -38,7 +38,7 @@ MAYBE_ADMIT = $(if $(ADMIT),--admit_smt_queries true)
 # YOU SHOULDN'T NEED TO TOUCH THE REST
 ################################################################################
 
-MY_FSTAR=$(Q)$(BENCHMARK_PRE)$(FSTAR)                       \
+MY_FSTAR=$(Q)$(BENCHMARK_PRE) $(FSTAR)                      \
 		 $(SIL) --cache_checked_modules             \
 		  --odir $(OUTPUT_DIRECTORY)                \
 		  --cache_dir $(CACHE_DIR)                  \

src/Makefile

@@ -48,12 +48,12 @@ ALL_BOOT=$(addprefix boot/FStar., Util.fsti List.fsti			\
 			          BigInt.fsti Pprint.fsti		\
 			          Tactics.Interpreter.fst		\
 			          Parser.Parse.fsti			\
-			          Tactics.Interpreter.fsti \
+			          Tactics.Interpreter.fsti		 \
 			          Tests.Test.fst \
 			          StringBuffer.fsti)
 
 define from_boot_file
-	@echo "[BOOT      $(basename $(notdir $@))]"
+	@echo "[BOOT      $(notdir $@)]"
 	$(Q)cp $^ $@
 	$(Q)$(SED) -i.bak '/\/\/ *JUST *FSHARP */d' $@
 	$(Q)$(SED) -i.bak 's,^ *// *IN *F\* *:,,g' $@
@@ -77,7 +77,7 @@ boot/FStar.Tests.Test.fst: tests/boot/FStar.Tests.Test.fs | boot_dir
 
 # GM: What's going on here?
 boot/FStar.Parser.Parse.fsti: parser/parse.fsi | boot_dir
-	@echo "[BOOT      $(basename $(notdir $@))]"
+	@echo "[BOOT      $(notdir $@)]"
 	$(Q)echo "#light \"off\"" > $@
 	$(Q)$(HEAD) -n12 $^ >> $@
 	$(Q)touch -r parser/parse.mly $@

src/Makefile.boot

@@ -53,7 +53,7 @@ EXTRACT = $(addprefix --extract_module , $(EXTRACT_MODULES))		\
 # And then, in a separate invocation, from each .checked.lax we
 # extract an .ml file
 ocaml-output/%.ml:
-	@echo "[EXTRACT   $(basename $(notdir $@))]"
+	@echo "[EXTRACT   $(notdir $@)]"
 	$(Q)$(BENCHMARK_PRE) $(FSTAR_C) $(SIL) $(notdir $(subst .checked.lax,,$<)) \
                    --codegen OCaml \
                    --extract_module $(basename $(notdir $(subst .checked.lax,,$<)))

src/basic/ml/FStar_Util.ml

@@ -418,17 +418,15 @@ let pimap_try_find (map: 'value pimap) (key: Z.t) =
   ZMap.Exceptionless.find key map
 let pimap_fold (m:'value pimap) f a = ZMap.fold f m a
 
-(* restore pre-2.11 BatString.nsplit behavior,
-   see https://github.com/ocaml-batteries-team/batteries-included/issues/845 *)
-let batstring_nsplit s t =
-  if s = "" then [] else BatString.nsplit s t
-
 let format (fmt:string) (args:string list) =
-  let frags = batstring_nsplit fmt "%s" in
+  let frags = BatString.split_on_string "%s" fmt in
   if BatList.length frags <> BatList.length args + 1 then
-    failwith ("Not enough arguments to format string " ^fmt^ " : expected " ^ (Pervasives.string_of_int (BatList.length frags)) ^ " got [" ^ (BatString.concat ", " args) ^ "] frags are [" ^ (BatString.concat ", " frags) ^ "]")
+    failwith ("Not enough arguments to format string " ^ fmt
+              ^ " : expected " ^ (Pervasives.string_of_int (BatList.length frags - 1))
+              ^ " got [" ^ (BatString.concat ", " args) ^ "] "
+              ^ "frags are [" ^ (BatString.concat ", " frags) ^ "]")
   else
-    let args = args@[""] in
+    let args = args @ [""] in
     BatList.fold_left2 (fun out frag arg -> out ^ frag ^ arg) "" frags args
 
 let format1 f a = format f [a]
@@ -553,7 +551,7 @@ let replace_chars (s:string) c (by:string) =
   BatString.replace_chars (fun x -> if x = Char.chr c then by else BatString.of_char x) s
 let hashcode s = Z.of_int (StringOps.hash s)
 let compare s1 s2 = Z.of_int (BatString.compare s1 s2)
-let split s sep = if s = "" then [""] else BatString.nsplit s sep
+let split s sep = if s = "" then [""] else BatString.split_on_string sep s
 let splitlines s = split s "\n"
 
 let iof = int_of_float

src/extraction/ml/FStar_Extraction_ML_PrintML.ml

@@ -3,6 +3,7 @@ open Lexing
 open Migrate_parsetree
 open Migrate_parsetree.Ast_405
 open Migrate_parsetree.Ast_405.Parsetree
+open Migrate_parsetree.Versions
 open Location
 open Pprintast
 open Ast_helper

src/ocaml-output/Makefile

@@ -11,10 +11,27 @@ include ../Makefile.common
 MENHIR=menhir #--explain --infer -la 1 --table
 OCAMLLEX=ocamllex
 FSTAR_OCAMLBUILD_EXTRAS ?= -cflag -g
-OCAMLBUILD=cd ../../ && ocamlbuild $(FSTAR_OCAMLBUILD_EXTRAS) -I src/ocaml-output -I src/basic/ml \
-  -I src/parser/ml -I src/fstar/ml -I src/extraction/ml \
-  -I src/prettyprint/ml -I src/tactics/ml -I src/tests/ml -I ulib/ml \
-  -j 24 -build-dir src/ocaml-output/_build -use-ocamlfind
+
+# From the root
+OCAMLBUILD_INCLUDES := \
+	src/ocaml-output \
+	src/basic/ml \
+	src/parser/ml \
+	src/fstar/ml \
+	src/extraction/ml \
+	src/prettyprint/ml \
+	src/tactics/ml \
+	src/tests/ml \
+	ulib/ml
+
+OCAMLBUILD_INCLUDE_FLAGS := $(addprefix -I , $(OCAMLBUILD_INCLUDES))
+
+OCAMLBUILD=cd ../../ &&                                                 \
+             ocamlbuild $(FSTAR_OCAMLBUILD_EXTRAS)                      \
+                      $(OCAMLBUILD_INCLUDE_FLAGS)                       \
+                      -j 4 -build-dir src/ocaml-output/_build           \
+                      -use-ocamlfind
+
 COMPILER_ML_LIB=FStar_Util.cmx FStar_Compiler_Bytes.cmx			\
 		FStar_Getopt.cmx FStar_Range.cmx FStar_Platform.cmx	\
 		FStar_Unionfind.cmx
@@ -57,7 +74,8 @@ parse.mly: ../parser/parse.mly
 ifeq ($(HAS_VALID_MENHIR), 1)
 	@# TODO : call menhir directly when positions are fixed instead of
 	@# letting OCamlbuild go through ocamlyacc
-	$(MENHIR) --only-preprocess-for-ocamlyacc $< > $@
+	@echo "[MENHIR PREPROCESS]"
+	$(Q)$(MENHIR) --only-preprocess-for-ocamlyacc $< > $@
 else
 	$(error Correct version of menhir not found (needs a version newer than $(MENHIR_MIN_VERSION)))
 endif
@@ -95,7 +113,7 @@ FSTAR_MAIN_NATIVE=_build/src/fstar/ml/main.native
 $(FSTAR_MAIN_NATIVE): export OCAMLFIND_IGNORE_DUPS_IN = $(shell ocamlfind query compiler-libs)
 $(FSTAR_MAIN_NATIVE): $(GENERATED_FILES)
 	@echo "[OCAMLBUILD]"
-	$(Q)$(OCAMLBUILD) $(notdir $(FSTAR_MAIN_NATIVE)) src/ocaml-output/FStar_Syntax_Syntax.inferred.mli
+	$(Q)$(OCAMLBUILD) $(notdir $(FSTAR_MAIN_NATIVE)) FStar_Syntax_Syntax.inferred.mli
 
 ../../bin/fstar.exe: $(FSTAR_MAIN_NATIVE)
 	$(Q)cp $^ $@
@@ -168,6 +186,7 @@ COMMITDATE = $(shell git log --pretty=format:%ci -n 1 2>/dev/null || echo unset)
 
 .PHONY: FStar_Version.ml
 FStar_Version.ml:
+	@echo [MAKE      FStar_Version.ml]
 	$(Q)echo 'open FStar_Util' > $@
 	$(Q)echo 'let dummy () = ();;' >> $@
 	$(Q)echo 'FStar_Options._version := "$(VERSION)";;' >> $@
@@ -281,14 +300,13 @@ endif
 
 .PHONY: clean
 # Clean up all files generated by targets in _this_ Makefile
-# Also clean up the standard library
 clean:
-	+$(MAKE) -C ../../ulib clean
-	rm -rf _build
-	rm -f $(GENERATED_FILES)
-	rm -f *.tar.gz *.zip
-	rm -f ../../bin/fstar-compiler-lib/*.cm[aiox]
-	rm -f ../../bin/fstar-compiler-lib/*.cmx[as]
+	@echo "[CLEAN     src/ocaml-output]"
+	$(Q)rm -rf _build
+	$(Q)rm -f $(GENERATED_FILES)
+	$(Q)rm -f *.tar.gz *.zip
+	$(Q)rm -f ../../bin/fstar-compiler-lib/*.cm[aiox]
+	$(Q)rm -f ../../bin/fstar-compiler-lib/*.cmx[as]
 
 # Purge (clean + delete *all* automatically generated files)
 # if you do this you'll need to run `make ocaml` in `src` to get them back

ulib/Makefile

@@ -18,14 +18,15 @@ extra: .cache
 .cache:
 	mkdir -p .cache
 
-include ml/Makefile.include
+include $(FSTAR_HOME)/ulib/ml/Makefile.include
+include $(FSTAR_HOME)/src/Makefile.common
 
 fstarlib.mgen: *.fst *.fsti
 	mkdir -p ml/extracted
 	rm -f .depend.extract
-	OUTPUT_DIRECTORY=ml/extracted \
-	EXTRACT_MODULES="--extract '-Prims +FStar +LowStar +Steel -FStar.Tactics -FStar.Reflection -Steel.Tactics $(NOEXTRACT_MODULES)'" \
-	+$(MAKE) -f Makefile.extract all-ml
+	+OUTPUT_DIRECTORY=ml/extracted \
+	    EXTRACT_MODULES="--extract '-Prims +FStar +LowStar +Steel -FStar.Tactics -FStar.Reflection -Steel.Tactics $(NOEXTRACT_MODULES)'" \
+	    $(MAKE) -f Makefile.extract all-ml
 	# the next cp is done because FStar_Pervasives.ml is needed to bootstrap the compiler
 	# we could follow this style for other files too, e.g., FStar_Option.ml
 	cp ../src/ocaml-output/FStar_Pervasives.ml ml/extracted
@@ -36,10 +37,10 @@ FSTARLIB_LEFTOVERS=$(shell ocaml fstarlib_leftovers.ml +ml +ml/extracted -../bin
 fstartaclib.mgen: fstarlib.mgen
 	mkdir -p tactics_ml/extracted
 	rm -f .depend.extract
-	OUTPUT_DIRECTORY=tactics_ml/extracted \
-	CODEGEN=Plugin \
-	EXTRACT_MODULES="--extract '+FStar.Tactics +FStar.Reflection $(NOEXTRACT_MODULES)'" \
-	+$(MAKE) -f Makefile.extract all-ml
+	+OUTPUT_DIRECTORY=tactics_ml/extracted \
+	    CODEGEN=Plugin \
+	    EXTRACT_MODULES="--extract '+FStar.Tactics +FStar.Reflection $(NOEXTRACT_MODULES)'" \
+	    $(MAKE) -f Makefile.extract all-ml
 	mkdir -p tactics_ml/fstarlib_leftovers
 	cp $(FSTARLIB_LEFTOVERS) tactics_ml/fstarlib_leftovers
 	touch fstartaclib.mgen
@@ -119,16 +120,17 @@ install-fstar-tactics: $(TACLIB_OBJECTS)
 	sed "s/__FSTAR_VERSION__/$$(cat ../version.txt)/" <ml/fstar-tactics-lib-META >$(TACLIB_DIR)/META
 
 clean:
-	rm -f .depend .depend.extract
-	rm -f *.mgen
-	rm -f *.checked *.checked.lax .cache/*.checked .cache/*.checked.lax
-	rm -fr ml/extracted tactics_ml/extracted tactics_ml/fstarlib_leftovers
-	rm -f ml/*.mllib tactics_ml/*.mllib tactics_ml/*.mldylib *~
-	rm -f $(FSTARLIB_DIR)/*.cm[aiox]
-	rm -f $(FSTARLIB_DIR)/*.cmx[as]
-	rm -f $(TACLIB_DIR)/*.cm[aiox]
-	rm -f $(TACLIB_DIR)/*.cmx[as]
-	rm -rf ml/_build tactics_ml/_build # ← ocamlbuild -clean does not work on Cygwin
+	@echo "[CLEAN     ulib/]"
+	$(Q)rm -f .depend .depend.extract
+	$(Q)rm -f *.mgen
+	$(Q)rm -f *.checked *.checked.lax .cache/*.checked .cache/*.checked.lax
+	$(Q)rm -fr ml/extracted tactics_ml/extracted tactics_ml/fstarlib_leftovers
+	$(Q)rm -f ml/*.mllib tactics_ml/*.mllib tactics_ml/*.mldylib *~
+	$(Q)rm -f $(FSTARLIB_DIR)/*.cm[aiox]
+	$(Q)rm -f $(FSTARLIB_DIR)/*.cmx[as]
+	$(Q)rm -f $(TACLIB_DIR)/*.cm[aiox]
+	$(Q)rm -f $(TACLIB_DIR)/*.cmx[as]
+	$(Q)rm -rf ml/_build tactics_ml/_build # ← ocamlbuild -clean does not work on Cygwin
 
 clean_ocaml:
 	rm -f *.mgen

ulib/ml/FStar_String.ml

@@ -5,7 +5,7 @@ let op_Hat s t =  strcat s t
 (* restore pre-2.11 BatString.nsplit behavior,
    see https://github.com/ocaml-batteries-team/batteries-included/issues/845 *)
 let batstring_nsplit s t =
-  if s = "" then [] else BatString.nsplit s t
+  if s = "" then [] else BatString.split_on_string t s
 
 let split seps s =
   let rec repeat_split acc = function