merge with master

.completion/fish/fstar.exe.fish

@@ -34,7 +34,6 @@ complete -c fstar.exe -l max_fuel -r --description "Number of unrolling of recur
 complete -c fstar.exe -l max_ifuel -r --description "Number of unrolling of inductive datatypes to try at most (default 2)"
 complete -c fstar.exe -l min_fuel -r --description "Minimum number of unrolling of recursive functions to try (default 1)"
 complete -c fstar.exe -l MLish --description "Trigger various specializations for compiling the F* compiler itself (not meant for user code)"
-complete -c fstar.exe -l n_cores -r --description "Maximum number of cores to use for the solver (implies detail_errors = false) (default 1)"
 complete -c fstar.exe -l no_default_includes --description "Ignore the default module search paths"
 complete -c fstar.exe -l no_extract -r --description "Do not extract code from this module"
 complete -c fstar.exe -l no_location_info --description "Suppress location information in the generated OCaml output (only relevant with --codegen OCaml)"

.docker/base/Dockerfile

@@ -1,37 +1,36 @@
-FROM ubuntu:bionic
+FROM ubuntu:18.04
 
-MAINTAINER Benjamin Beurdouche <[email protected]>; Daniel Fabian <[email protected]>
+MAINTAINER Benjamin Beurdouche <[email protected]>; Victor Dumitrescu <[email protected]>; Daniel Fabian <[email protected]>;
 
-# Define versions of dependencies
-ENV opamv 4.05.0
-ENV z3v 4.5.1.1f29cebd4df6-x64-ubuntu-14.04
-
-# Install required packages and set versions
+# Install required packages
+RUN apt-get -qq update
+RUN apt-get install -y software-properties-common
+RUN add-apt-repository -y ppa:avsm/ppa # for opam 2
 RUN apt-get -qq update
-RUN apt-get install --yes sudo wget libssl-dev libsqlite3-dev g++ gcc m4 make opam pkg-config python libgmp3-dev unzip
+RUN apt-get install -y sudo wget libssl-dev libsqlite3-dev g++ gcc m4 make opam pkg-config python libgmp3-dev unzip cmake
 
 # Create user
-RUN useradd -ms /bin/bash FStar
-RUN echo "FStar ALL=(ALL:ALL) NOPASSWD:ALL" >> /etc/sudoers
-USER FStar
-WORKDIR /home/FStar
+RUN useradd -ms /bin/bash build
+RUN echo "build ALL=(ALL:ALL) NOPASSWD:ALL" >> /etc/sudoers
+USER build
+WORKDIR /home/build
 
-# Prepare build (OCaml packages)
-ENV OPAMYES true
-RUN opam init
-RUN echo ". /home/FStar/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true" >> .bashrc
-RUN opam switch ${opamv}
-RUN opam install ocamlfind batteries sqlite3 fileutils stdint zarith yojson pprint menhir ulex ppx_deriving ppx_deriving_yojson process
+# Prepare and build OPAM and OCaml
+RUN opam init -y --disable-sandboxing --compiler=4.07.0
+RUN opam update
+RUN opam install -y ocamlbuild ocamlfind batteries stdint zarith yojson fileutils pprint menhir ulex ppx_deriving ppx_deriving_yojson process pprint visitors fix wasm
 
 # Prepare and build Z3
-RUN wget https://github.com/FStarLang/binaries/raw/master/z3-tested/z3-${z3v}.zip
-RUN unzip z3-${z3v}.zip
-RUN mv z3-${z3v} z3
-ENV PATH "/home/FStar/z3/bin:$PATH"
-WORKDIR /home/FStar
+ENV z3=z3-4.8.5-x64-debian-8.11
+ADD https://github.com/FStarLang/binaries/raw/master/z3-tested/${z3}.zip .
+RUN sudo unzip ${z3}.zip
+ENV PATH=/home/build/${z3}/bin:${PATH}
+WORKDIR /home/build
 
 # Prepare and build F*
 ADD update-fstar.sh .
 RUN git clone https://github.com/FStarLang/FStar.git --depth=1
-ENV PATH "~/FStar/bin:$PATH"
-RUN opam config exec -- make -C FStar/src/ocaml-output
+ENV FSTAR_HOME=/home/build/FStar
+WORKDIR $FSTAR_HOME
+RUN opam config exec -- make
+WORKDIR /home/build

.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

.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" ]
-}
+}

.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" ]
-}
+}

.docker/build/config.json

@@ -27,7 +27,7 @@
     "FolderToCompress" : "FStar",
     "FoldersToExclude" : [ ],
 
-    "TrackPerformance" : true,
+    "TrackPerformance" : false,
 
     "RepoVersions" : {
         "hacl_version" : "origin/fstar-master",

.gitignore

@@ -8,6 +8,7 @@
 *.sav
 *.hints.fsval
 *.hints.mlval
+*.bench
 dump*
 cache/
 /VS/packages

.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 --"

CHANGES.md

@@ -18,6 +18,18 @@ Guidelines for the changelog:
   * Friend modules (https://github.com/FStarLang/FStar/wiki/Friend-modules)
 
 ## Core typechecker
+  * Cf. issue https://github.com/FStarLang/FStar/issues/1055,
+    F* now enforces that unannotated, effectful functions have a
+    trivial precondition (this is already the case for pure functions).
+
+    See some testcases in `examples/bug-reports/Bug1055.fst`.
+
+    The check is performed under a new flag `--trivial_pre_for_unannotated_effectful_fns`,
+    which is `true` by-default.
+
+    This is a breaking change, see this commit for how we fixed the F* examples:
+    https://github.com/FStarLang/FStar/commit/24bbae4b93a9937695160dff381625adb6565d28
+
 
   * Revised typechecking of nested patterns and ascriptions on
     patterns, fixing unsoundnesses (issue #238, for example)
@@ -177,6 +189,14 @@ Guidelines for the changelog:
      is not already_cached in a location that is not the same as its
      expected output location, we raise Warning 321.
 
+## Command line options
+
+   * [PR #1711](https://github.com/FStarLang/FStar/pull/1711): Where
+     options take lists of namespaces as arguments
+     (`--already_cached`, `--extract`, `--using_facts_from`, etc.),
+     those lists of namespaces can be given under the form `+A -B +C`
+     (space-separated) or `+A,-B,+C` (comma-separated).
+
 # Version 0.9.6.0
 
 ## Command line options

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).
@@ -186,7 +191,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 ####
 
@@ -199,7 +204,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
@@ -227,7 +232,7 @@ The steps require a working OCaml setup. OCaml version 4.04.X, 4.05.X, 4.06.X, o
 4. F\* depends on a bunch of external OCaml packages which you should install using OPAM:
 
   ```sh
-  $ opam install ocamlbuild ocamlfind batteries stdint zarith yojson fileutils pprint menhir ulex ppx_deriving ppx_deriving_yojson process pprint
+  $ opam install ocamlbuild ocamlfind batteries stdint zarith yojson fileutils pprint menhir ulex ppx_deriving ppx_deriving_yojson process
   ```
 
   **Note:** this list of packages is longer than the list in the

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