merging master in

FStarLang · Jul 2, 2019 · 769b1087c3ed74e27ec7838594c9379b145451a5 · 769b108
1 parent 56c9552
commit 769b1087c3ed74e27ec7838594c9379b145451a5
Unified Split

Showing 1,183 changed files with 144,468 additions and 145,765 deletions.
diff --git a/.docker/build/build.sh b/.docker/build/build.sh
@@ -295,6 +295,14 @@ function build_fstar() {
                     }
             } &
 
+	    # The LowParse test suite is now in project-everest/everparse
+	    {
+		$gnutime make -C qd -j $threads -k lowparse-fstar-test || {
+		    echo "Error - LowParse"
+		    echo " - min-test (LowParse)" >>$ORANGE_FILE
+		}
+	    } &
+
             # We now run all (hardcoded) tests in mitls-fstar@master
             {
                 # First regenerate dependencies and parsers (maybe not

diff --git a/.docker/build/config-binaries.json b/.docker/build/config-binaries.json
@@ -3,8 +3,11 @@
 
     "BaseContainerIsEverestImage" : true,
     "BaseContainerImageName" : "fstar",
-    "BaseContainerImageTagOrCommitId": "latest",
-    "BranchName" : "master",
+
+    "_ABOUT_NEXT_TWO_VARS": "These variables are commented out. When these variables are undefined, builds use Azure DevOps variables instead. Uncomment them to specify a different base image",
+    "_BaseContainerImageTagOrCommitId": "latest",
+    "_BranchName" : "master",
+
     "GithubCommitUrl" : "https://github.com/FStarLang/FStar/commit",
     "OnDemandBuildDefinition" : "FStar\\FStar-{agentOS}",
 
@@ -18,8 +21,9 @@
     "CIBuildTarget" : "fstar-binary-build",
     "NightlyBuildTarget" : "fstar-binary-build",
     "HasLogsToExtract" : true,
+    "HasQueryStats" : false,
 
     "NotificationEnabled" : true,
     "NotificationChannel" : "#fstar-build",
     "PublicBranches" : [ "master" ]
-}
+}
diff --git a/.docker/build/config-docs.json b/.docker/build/config-docs.json
@@ -3,8 +3,11 @@
 
     "BaseContainerIsEverestImage" : true,
     "BaseContainerImageName" : "fstar",
-    "BaseContainerImageTagOrCommitId": "latest",
-    "BranchName" : "master",
+
+    "_ABOUT_NEXT_TWO_VARS": "These variables are commented out. When these variables are undefined, builds use Azure DevOps variables instead. Uncomment them to specify a different base image",
+    "_BaseContainerImageTagOrCommitId": "latest",
+    "_BranchName" : "master",
+
     "GithubCommitUrl" : "https://github.com/FStarLang/FStar/commit",
     "OnDemandBuildDefinition" : "FStar\\FStar-{agentOS}",
 
@@ -18,8 +21,9 @@
     "CIBuildTarget" : "fstar-docs",
     "NightlyBuildTarget" : "fstar-docs",
     "HasLogsToExtract" : true,
+    "HasQueryStats" : false,
 
     "NotificationEnabled" : true,
     "NotificationChannel" : "#fstar-build",
     "PublicBranches" : [ "master" ]
-}
+}
diff --git a/.docker/build/config.json b/.docker/build/config.json
@@ -27,7 +27,7 @@
     "FolderToCompress" : "FStar",
     "FoldersToExclude" : [ ],
 
-    "TrackPerformance" : true,
+    "TrackPerformance" : false,
 
     "RepoVersions" : {
         "hacl_version" : "origin/fstar-master",

diff --git a/.scripts/process_build.sh b/.scripts/process_build.sh
@@ -91,7 +91,7 @@ else
   fi
 fi
 
-diag "*** Make the examples ***"
+diag "*** Test the binary package ***"
 cd fstar
 
 # We need two FSTAR_HOMEs in this script: one for the host (from where
@@ -103,16 +103,47 @@ cd fstar
 # to export it from here.
 export FSTAR_HOME="$PWD"
 
-diag "-- Verify hello ocaml -- should output Hello F*! --"
-make -C examples/hello ocaml | tee HelloOcamlOutput.log
+diag "-- Versions --"
+bin/fstar.exe --version
+bin/z3 --version
+
+diag "-- Verify micro benchmarks --"
+make -C examples/micro-benchmarks
+if [ $? -ne 0 ]; then
+  echo -e "* ${RED}FAIL!${NC} for micro benchmarks - make returned $?"
+  exit 1
+else
+  echo -e "* ${GREEN}PASSED!${NC} for micro benchmarks"
+fi
+
+diag "-- Rebuilding ulib/ml (to make sure it works) --"
+make -C ulib/ml clean && make -C ulib install-fstarlib
+if [ $? -ne 0 ]; then
+  echo -e "* ${RED}FAIL!${NC} for install-fstarlib - make returned $?"
+  exit 1
+else
+  echo -e "* ${GREEN}PASSED!${NC} for install-fstarlib"
+fi
+
+diag "-- Execute examples/hello via OCaml -- should output Hello F*! --"
+make -C examples/hello hello | tee HelloOcamlOutput.log
 if [ $? -ne 0 ]; then
-  echo -e "* ${RED}FAIL!${NC} for examples/hello ocaml - make failed withexit code $?"
+  echo -e "* ${RED}FAIL!${NC} for examples/hello - make failed withexit code $?"
   exit 1
 elif ! egrep -q 'Hello F\*!' HelloOcamlOutput.log; then
-  echo -e "* ${RED}FAIL!${NC} for examples/hello ocaml - 'Hello F*!' was not found in HelloOcamlOutput.log"
+  echo -e "* ${RED}FAIL!${NC} for examples/hello - 'Hello F*!' was not found in HelloOcamlOutput.log"
+  exit 1
+else
+  echo -e "* ${GREEN}PASSED!${NC} for examples/hello"
+fi
+
+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 examples/hello ocaml"
+  echo -e "* ${GREEN}PASSED!${NC} for ulib"
 fi
 
 diag "-- Verify all examples --"

diff --git a/CONTRIBUTIONS.md → CONTRIBUTING.md b/CONTRIBUTIONS.md → CONTRIBUTING.md
diff --git a/INSTALL.md b/INSTALL.md
@@ -28,13 +28,17 @@ or our new [even cooler online editor] (experimental).
 
 ## OPAM package ##
 
-If the OCaml package manager is present on your platform, you can
+If the OCaml package manager (OPAM) is present on your platform, you can
 install the latest development version of F\* (`master` branch) and
 required dependencies (except for Z3) using the following commands:
 
         $ opam pin add fstar --dev-repo
         $ opam install fstar
 
+Note: To install OCaml and OPAM on your platform please read the
+[Working OCaml setup](#prerequisite-for-steps-2-and-3-working-ocaml-setup)
+section further below, steps 0 to 3.
+
 ## Binary releases ##
 
 Every now and then we release [F\* binaries on GitHub] (for Windows, Mac, and Linux)
@@ -65,7 +69,7 @@ following commands. (On Windows this requires Cygwin and `make`)
         date=yyyy-mm-ddThh:nn:ss+02:00
         commit=xxxxxxxx
         $ z3 --version
-        Z3 version 4.5.1 - 64 bit - build hashcode 1f29cebd4df6
+        Z3 version 4.8.5 - 64 bit
 
    Note: if you are using the binary package and extracted it to,
    say, the `fstar` directory, then both `fstar.exe` and `z3` are in
@@ -75,12 +79,17 @@ following commands. (On Windows this requires Cygwin and `make`)
 
         $ make -C examples/micro-benchmarks
 
-3. If you have OCaml installed the following command should print "Hello F\*!"
-   You need the same version of OCaml as was used to create the
-   `fstar.exe` binary (which you can see with `fstar.exe --version`,
-    as illustrated above).
+3. If you have OCaml installed and intend to extract and compile OCaml code
+   against the F* library, please rebuild it with:
+
+        $ make -C ulib install-fstarlib
+
+   Then the following command should print "Hello F\*!"
+
+        $ make -C examples/hello hello
 
-        $ make -C examples/hello ocaml
+   See [here](https://github.com/FStarLang/FStar/wiki/Executing-F*-code) for
+   further documentation on extracting and executing F* code.
 
    Note: to have a working OCaml install, please first read the
    [Working OCaml
@@ -91,16 +100,12 @@ following commands. (On Windows this requires Cygwin and `make`)
 
         $ opam install ocamlfind batteries stdint zarith ppx_deriving ppx_deriving_yojson ocaml-migrate-parsetree process
 
-   Note: If you hand-rolled your own F* binary then remember that you need to
-         also build our OCaml support library, as further documented
-         [here](https://github.com/FStarLang/FStar/wiki/Executing-F*-code):
-
-        $ make -C ulib/ml
-
 4. You can verify the F* library and all the examples,
    keeping in mind that this might take a long time.
 
-        $ make -j6 -C ulib examples
+        $ make -j6 -C ulib
+        $ echo $?    # non-zero means build failed! scroll up for error message!
+        $ make -j6 -C examples
         $ echo $?    # non-zero means build failed! scroll up for error message!
 
    Note: Some of the examples require having OCaml installed (as for step 3 above).
@@ -180,7 +185,7 @@ Some convenience Makefile targets are available:
 
 ### Prerequisites: Working OCaml setup  ###
 
-The steps require a working OCaml setup. OCaml version 4.04.X, 4.05.X, 4.06.X, or 4.07.0 should work.
+The steps require a working OCaml setup. OCaml version 4.04.X, 4.05.X, 4.06.X, or 4.07.X should work.
 
 #### Instructions for Windows ####
 
@@ -193,7 +198,7 @@ The steps require a working OCaml setup. OCaml version 4.04.X, 4.05.X, 4.06.X, o
    - Can be installed using either your package manager or using OPAM
      (see below).
 
-1. Install OPAM (version 1.2.x).
+1. Install OPAM (version 1.2.x or later).
 
    - Installation instructions are available at various places
      (e.g., https://dev.realworldocaml.org/install.html

diff --git a/README.md b/README.md
@@ -69,7 +69,6 @@ various F* announcements are made to the general public (e.g. for
 releases, new papers, etc) and where users can ask questions, ask for
 help, discuss, provide feedback, announce jobs requiring at least 10
 years of F* experience, etc.
-
 [List archives] are public and [searchable], but only members can post.
 [Join here][fstar-club mailing list]!
 
@@ -99,27 +98,11 @@ that your problem still exists on the `master` branch.
 
 ### Contributing
 
-See [CONTRIBUTIONS.md](https://github.com/FStarLang/FStar/blob/master/CONTRIBUTIONS.md)
+See [CONTRIBUTING.md](https://github.com/FStarLang/FStar/blob/master/CONTRIBUTING.md)
 
 ### License
 
-This new variant of F* is released under the [Apache 2.0 license];
-see `LICENSE` for more details.
+F* is released under the [Apache 2.0 license]; for more details
+see [LICENSE](https://github.com/FStarLang/FStar/blob/master/LICENSE)
 
 [Apache 2.0 license]: https://www.apache.org/licenses/LICENSE-2.0
-
-### Towards F* version 1.0
-
-This is a new variant of F* (carrying version 0.9.x) that is still in
-development and we hope will eventually lead to a 1.0 release. This
-new variant is incompatible and quite different compared to the
-previously released [0.7 versions and earlier].
-
-[0.7 versions and earlier]: https://github.com/FStarLang/FStar#old-f-versions-v071-and-earlier
-
-### Old F* versions (v0.7.1 and earlier) ###
-
-[F\* v0.7.1] and earlier are no longer maintained, so please do not
-create any issues here about those versions.
-
-[F\* v0.7.1]: https://github.com/FStarLang/FStar/blob/stratified_last/.old/fstar-0.7.1-alpha.zip?raw=true
diff --git a/_tags b/_tags
@@ -10,7 +10,8 @@ true: \
   annot, bin_annot, thread, -traverse, \
   package(batteries), \
   package(zarith), \
-  package(ppx_deriving.std), package(ppx_deriving_yojson)
+  package(ppx_deriving.std), \
+  package(ppx_deriving_yojson)
 
 # ADL: the new unicode lexer
 "src/parser/ml/FStar_Parser_LexFStar.ml": syntax(camlp4o)
@@ -47,3 +48,29 @@ true: \
 
 <**/FStar_Monotonic_Seq.ml>: \
   principal
+
+
+#
+# To use landmarks to profile ocaml code:
+#  - make sure landmarks is installed with opam (opam install landmarks)
+#  - enable the landmarks and landmarks.ppx packages
+#  - select the modules for auto-instrumentation
+#  - build the compiler
+#  - run the compiler with OCAML_LANDMARKS='on,output=landmarks.out'
+#
+# Uncomment the following to add the packages:
+#
+# true: \
+#   package(landmarks), \
+#   package(landmarks.ppx)
+#
+# Uncomment the following to profile specific modules:
+#
+# <src/ocaml-output/FStar_{Main,Dependencies,Universal,TypeChecker_Normalize,TypeChecker_Tc,TypeChecker_Util,SMTEncoding_Encode}.ml>: \
+#    ppx(`ocamlfind query landmarks.ppx`/ppx.exe --as-ppx --auto)
+#
+#
+# NB: the fully inclusive landmarks ppx on ocaml-output/**/*.ml files can cause a stack overflow
+# <src/ocaml-output/**/*.ml>: \
+#   ppx(`ocamlfind query landmarks.ppx`/ppx.exe --as-ppx --auto)
+#
diff --git a/bin/.gitignore b/bin/.gitignore
@@ -8,3 +8,4 @@ fstar.exe
 fstar.fsharp
 FsLexYacc.Runtime.dll
 *.XML
+*lib/META
diff --git a/build_local.sh b/build_local.sh
@@ -1,15 +1,16 @@
 #!/usr/bin/env bash
+set -e
 
 # Look for config.json file
 FILE=".docker/build/config.json"
-if [ ! -f $FILE ]; then
+if [[ ! -f $FILE ]]; then
    echo "File $FILE does not exist."
 fi
 
 # In case you want to build windows, change agentOS here to windows-nt if OSTYPE is not working
 agentOS=linux
 if [[ "$OSTYPE" == "cygwin" ]]; then
-    agentOS=windows-nt
+    agentOS=linux #windows-nt
 fi
 
 DOCKERFILE=$(jq -c -r ".DockerFile" "$FILE")
@@ -31,20 +32,20 @@ REQUESTEDBRANCHNAME=$(jq -c -r ".BranchName" "$FILE")
 REQUESTEDCOMMITID=$(jq -c -r ".BaseContainerImageTagOrCommitId" "$FILE")
 COMMITURL=$(jq -c -r ".GithubCommitUrl" "$FILE")/$REQUESTEDBRANCHNAME
 
-if [ $(jq -c -r ".GithubCommitUrl" "$FILE") -ne "latest" ]; then
+if [[ $(jq -c -r ".BaseContainerImageTagOrCommitId" "$FILE") -ne "latest" ]]; then
     COMMITURL=$(jq -c -r ".GithubCommitUrl" "$FILE")/$REQUESTEDCOMMITID
 fi
 
-CONTENT=$(curl $COMMITURL)
-FULLCOMMITID="$( echo ${CONTENT} | sed 's/.*commit\/\([^"]*\).*/\1/g' )"
+LINE="$( git ls-remote ${COMMITURL%"/commit/master"} HEAD)"
+FULLCOMMITID="$( echo ${LINE} | cut -f1 )"
 COMMITID=${FULLCOMMITID:0:12}
 
 # create fake files ssh key, commitinfofilename.json, etc
 echo "fake" > id_rsa
 echo "fake" > commitinfofilename.json
 
 # build container
-docker build --file Dockerfile --build-arg BUILDLOGFILE="buildlogfile.txt" --build-arg MAXTHREADS="8" --build-arg TARGET="$BUILDTARGET" --build-arg BRANCHNAME="$LOCALBRANCHNAME" --build-arg COMMITID="$COMMITID" --build-arg DOCKERHUBPROJECT="projecteverest/" --tag "$PROJECTNAME:local" .
+docker build --file Dockerfile --build-arg BUILDLOGFILE="buildlogfile.txt" --build-arg MAXTHREADS="8" --build-arg BUILDTARGET="$BUILDTARGET" --build-arg BRANCHNAME="$LOCALBRANCHNAME" --build-arg COMMITID="$COMMITID" --build-arg DOCKERHUBPROJECT="projecteverest/" --tag "$PROJECTNAME:local" .
 
 # delete fake files
 rm -f id_rsa
@@ -54,4 +55,4 @@ rm -f commitinfofilename.json
 for f in $DEPFILES; do rm -f $(basename $f); done
 
 # delete dockerfile
-rm -f Dockerfile
+rm -f Dockerfile
diff --git a/doc/tutorial/code/exercises/Ex01a.fst.hints b/doc/tutorial/code/exercises/Ex01a.fst.hints
@@ -18,7 +18,7 @@
         "projection_inverse_FStar.Pervasives.V_v"
       ],
       0,
-      "6b11d730c8ed4f30624f77e21a6b4737"
+      "a3e60da4f4dbfc76948ca9ba7fa5babc"
     ],
     [
       "Ex01a.checkedRead",
@@ -27,7 +27,7 @@
       1,
       [ "@query", "projection_inverse_BoxBool_proj_0" ],
       0,
-      "968e22e40200dd508b2e075c9f658d60"
+      "3c5bc3e0ec0f84021c8a749de88f8977"
     ]
   ]
 ]