Merge remote-tracking branch 'origin/master' into _refine

.docker/build/build.sh

@@ -25,7 +25,7 @@ function fetch_vale() {
     echo Switching to vale to fstar_ci
     git clean -fdx .
     git reset --hard origin/fstar_ci
-    nuget.exe restore tools/Vale/src/packages.config -PackagesDirectory tools/FsLexYacc
+    nuget restore tools/Vale/src/packages.config -PackagesDirectory tools/FsLexYacc
     cd ..
     export_home VALE "$(pwd)/vale"
 }
@@ -188,6 +188,8 @@ function build_fstar() {
             echo Warm-up failed
             echo Failure >$result_file
         else
+            export_home FSTAR "$(pwd)"
+
             fetch_vale &
             fetch_hacl &
             fetch_and_make_kremlin &
@@ -204,7 +206,6 @@ function build_fstar() {
             # propagated to the current shell. Re-do.
             export_home HACL "$(pwd)/hacl-star"
             export_home KREMLIN "$(pwd)/kremlin"
-            export_home FSTAR "$(pwd)"
 
             # Once F* is built, run its main regression suite, along with more relevant
             # tests.
@@ -219,11 +220,9 @@ function build_fstar() {
                 if [[ "$OS" == "Windows_NT" ]]; then
                     ## This hack for determining the success of a vale run is needed
                     ## because somehow scons is not returning the error code properly
-                    timeout $timeout ./scons_cygwin.sh -j $threads --FSTAR-MY-VERSION --MIN_TEST |& tee vale_output
+                    { timeout $timeout env VALE_SCONS_EXIT_CODE_OUTPUT_FILE=vale_exit_code ./run_scons.sh -j $threads --FSTAR-MY-VERSION --MIN_TEST |& tee vale_output ; } || has_error="true"
 
-                    ## adds "min-test (Vale)" to the ORANGE_FILE
-                    ##      if this string vvvv is present in vale_output
-                    ! grep -qi 'scons: building terminated because of errors.' vale_output || has_error="true"
+                    { [[ -f vale_exit_code ]] && [[ $(cat vale_exit_code) -eq 0 ]] ; } || has_error="true"
                 else
                     timeout $timeout scons -j $threads --FSTAR-MY-VERSION --MIN_TEST || has_error="true"
                 fi
@@ -292,7 +291,8 @@ function build_fstar() {
                 { echo " - snapshot-diff (F*)" >>$ORANGE_FILE; }
             fi
 
-            if [[ $localTarget == "uregressions-ulong" ]]; then
+            # We should not generate hints when building on Windows
+            if [[ $localTarget == "uregressions-ulong" && "$OS" != "Windows_NT" ]]; then
                 refresh_fstar_hints
             fi
         fi

.docker/build/build_helper.sh

@@ -25,9 +25,16 @@ echo $(date -u "+%Y-%m-%d %H:%M:%S") >> $out_file
 eval $(ssh-agent)
 ssh-add -D
 
-# Generate query-stats.
-# List the hints that fail to replay.
-FStar/.scripts/query-stats.py -f $out_file -F html -o log_no_replay.html -n all '--filter=fstar_usedhints=+' '--filter=fstar_tag=-' -g
+# Docs and binaries don't have query stats.
+if [[ $target != "fstar-docs"  && $target != "fstar-binary-build" ]]; then
 
-# Worst offenders (longest times)
-FStar/.scripts/query-stats.py -f $out_file -F html -o log_worst.html -c -g -n 10
+    # Generate query-stats.
+    # List the hints that fail to replay.
+    FStar/.scripts/query-stats.py -f $out_file -F html -o log_no_replay.html -n all '--filter=fstar_usedhints=+' '--filter=fstar_tag=-' -g
+
+    # Worst offenders (longest times)
+    FStar/.scripts/query-stats.py -f $out_file -F html -o log_worst.html -c -g -n 10
+fi
+
+# Generate the container timestamp for debug purposes
+echo $(date -u "+%Y-%m-%d %H:%M:%S") >> "timestamp.txt"

.docker/build/linux/Dockerfile

@@ -13,7 +13,6 @@ RUN chown everest ${MYHOME}/.ssh
 RUN chmod 700 ${MYHOME}/.ssh
 COPY --chown=everest id_rsa ${MYHOME}/.ssh/id_rsa
 RUN chmod 600 ${MYHOME}/.ssh/id_rsa
-RUN eval $(ssh-agent)
 
 # Copy FSTAR source code.
 RUN mkdir ${MYHOME}/FStar

.docker/build/linux/binaries/Dockerfile

@@ -1,10 +1,12 @@
 # Fstar binaries container used to build fstar binaries.
 # Binaries should always use the latest fstar image available.
-FROM fstar:latest
+FROM fstar-linux:latest
 
 ARG BUILDLOGFILE
 ARG MAXTHREADS
 ARG TARGET
+ARG BRANCHNAME
+ARG FSTARSOURCEVERSION
 
 #BUILD FSTAR Binaries
 RUN rm -f ${BUILDLOGFILE}
@@ -21,13 +23,9 @@ RUN chown everest ${MYHOME}/.ssh
 RUN chmod 700 ${MYHOME}/.ssh
 COPY --chown=everest id_rsa ${MYHOME}/.ssh/id_rsa
 RUN chmod 600 ${MYHOME}/.ssh/id_rsa
-RUN eval $(ssh-agent)
 
 # Build FStar Binaries
-RUN echo $(date -u '+%Y-%m-%d %H:%M:%S') >> ${BUILDLOGFILE}
-RUN ./build_helper.sh ${TARGET} ${BUILDLOGFILE} ${MAXTHREADS} || true
-RUN echo $(date -u '+%Y-%m-%d %H:%M:%S') >> ${BUILDLOGFILE}
+RUN ./build_helper.sh ${TARGET} ${BUILDLOGFILE} ${MAXTHREADS} ${BRANCHNAME} ${FSTARSOURCEVERSION} || true
 
 # Remove ssh identities.
-RUN rm ${MYHOME}/.ssh/id_rsa
-RUN eval $(ssh-agent) && ssh-add -D
+RUN rm ${MYHOME}/.ssh/id_rsa

.docker/build/linux/docs/Dockerfile

@@ -1,10 +1,12 @@
 # Fstar docs container used to build fstar documentation.
 # Docs should always use the latest fstar image available.
-FROM fstar:latest
+FROM fstar-linux:latest
 
 ARG BUILDLOGFILE
 ARG MAXTHREADS
 ARG TARGET
+ARG BRANCHNAME
+ARG FSTARSOURCEVERSION
 
 #BUILD FSTAR Docs
 RUN rm -f ${BUILDLOGFILE}
@@ -21,13 +23,9 @@ RUN chown everest ${MYHOME}/.ssh
 RUN chmod 700 ${MYHOME}/.ssh
 COPY --chown=everest id_rsa ${MYHOME}/.ssh/id_rsa
 RUN chmod 600 ${MYHOME}/.ssh/id_rsa
-RUN eval $(ssh-agent)
 
 # Build FStar docs
-RUN echo $(date -u '+%Y-%m-%d %H:%M:%S') >> ${BUILDLOGFILE}
-RUN ./build_helper.sh ${TARGET} ${BUILDLOGFILE} ${MAXTHREADS} || true
-RUN echo $(date -u '+%Y-%m-%d %H:%M:%S') >> ${BUILDLOGFILE}
+RUN ./build_helper.sh ${TARGET} ${BUILDLOGFILE} ${MAXTHREADS} ${BRANCHNAME} ${FSTARSOURCEVERSION} || true
 
 # Remove ssh identities.
-RUN rm ${MYHOME}/.ssh/id_rsa
-RUN eval $(ssh-agent) && ssh-add -D
+RUN rm ${MYHOME}/.ssh/id_rsa

.docker/build/windows-nt/Dockerfile

@@ -1,5 +1,5 @@
 # Fstar build container
-FROM everest_base_image:1
+FROM everest-base-windows-nt:1
 
 ARG BUILDLOGFILE
 ARG MAXTHREADS

.docker/build/windows-nt/binaries/Dockerfile

@@ -0,0 +1,35 @@
+# Fstar binaries container used to build fstar binaries.
+# Binaries should always use the latest fstar image available.
+FROM fstar-windows-nt:latest
+
+ARG BUILDLOGFILE
+ARG MAXTHREADS
+ARG TARGET
+ARG BRANCHNAME
+ARG FSTARSOURCEVERSION
+
+# Add ssh key
+# We cannot copy directly to the .ssh folder, instead we copy to a temp folder
+WORKDIR "everestsshkey"
+COPY id_rsa .
+WORKDIR ".."
+
+# Now, using bash we copy the file, set the correct security and remove the previous folder
+RUN Invoke-BashCmd '"cd .ssh && cp ../everestsshkey/id_rsa . && chmod 600 id_rsa && rm -rf ../everestsshkey"'
+
+# Remove extra files.
+RUN Invoke-BashCmd rm -f $Env:BUILDLOGFILE
+RUN Invoke-BashCmd rm -f log_no_replay.html
+RUN Invoke-BashCmd rm -f log_worst.html
+RUN Invoke-BashCmd rm -f orange_status.txt
+RUN Invoke-BashCmd rm -f result.txt
+RUN Invoke-BashCmd rm -f status.txt
+RUN Invoke-BashCmd rm -f commitinfofilename.json
+
+COPY build.sh build.sh
+COPY build_helper.sh build_helper.sh
+
+RUN Invoke-BashCmd ./build_helper.sh $Env:TARGET $Env:BUILDLOGFILE $Env:MAXTHREADS $Env:BRANCHNAME $Env:FSTARSOURCEVERSION '||' true
+
+# Remove ssh key.
+RUN Invoke-BashCmd rm .ssh/id_rsa

.docker/build/windows-nt/docs/Dockerfile

@@ -0,0 +1,35 @@
+# Fstar docs container used to build fstar documentation.
+# Docs should always use the latest fstar image available.
+FROM fstar-windows-nt:latest
+
+ARG BUILDLOGFILE
+ARG MAXTHREADS
+ARG TARGET
+ARG BRANCHNAME
+ARG FSTARSOURCEVERSION
+
+# Add ssh key
+# We cannot copy directly to the .ssh folder, instead we copy to a temp folder
+WORKDIR "everestsshkey"
+COPY id_rsa .
+WORKDIR ".."
+
+# Now, using bash we copy the file, set the correct security and remove the previous folder
+RUN Invoke-BashCmd '"cd .ssh && cp ../everestsshkey/id_rsa . && chmod 600 id_rsa && rm -rf ../everestsshkey"'
+
+# Remove extra files.
+RUN Invoke-BashCmd rm -f $Env:BUILDLOGFILE
+RUN Invoke-BashCmd rm -f log_no_replay.html
+RUN Invoke-BashCmd rm -f log_worst.html
+RUN Invoke-BashCmd rm -f orange_status.txt
+RUN Invoke-BashCmd rm -f result.txt
+RUN Invoke-BashCmd rm -f status.txt
+RUN Invoke-BashCmd rm -f commitinfofilename.json
+
+COPY build.sh build.sh
+COPY build_helper.sh build_helper.sh
+
+RUN Invoke-BashCmd ./build_helper.sh $Env:TARGET $Env:BUILDLOGFILE $Env:MAXTHREADS $Env:BRANCHNAME $Env:FSTARSOURCEVERSION '||' true
+
+# Remove ssh key.
+RUN Invoke-BashCmd rm .ssh/id_rsa

.gitattributes

@@ -1,6 +1,11 @@
+# Linguist
 *.fst linguist-language=FStar
+*.fst linguist-documentation=false
 *.fsti linguist-language=FStar
+*.fsti linguist-documentation=false
+src/ocaml-output/FStar_*.ml linguist-vendored
 
+# Line endings
 *.fs* eol=lf
 *.ml* eol=lf
 Makefile eol=lf
@@ -10,7 +15,6 @@ configure eol=lf
 kremlin_ref eol=lf
 .gitignore eol=lf
 .ignore eol=lf
-
 /src/tools/* eol=lf
 /src/tests/interactive/* eol=lf
 

.gitignore

@@ -45,6 +45,9 @@ queries*.smt2
 transcript
 dump
 
+# ignore .ml files on the root dir
+/*.ml
+
 *.cmi
 *.cmo
 *.cmx

CHANGES.md

@@ -22,6 +22,36 @@ Guidelines for the changelog:
   * Revised typechecking of nested patterns and ascriptions on
     patterns, fixing unsoundnesses (issue #238, for example)
 
+## Libraries
+
+   * Two core axioms were discovered by Aseem Rastogi to be formulated
+     in an unsound manner.
+
+     FStar.FunctionalExtensionality has been reformulated to prevent
+     equivalence proofs of a function on a given domain to be
+     improperly extended to equivalence on a larger domain. The
+     library was fixed to ensure that domain type used to prove the
+     equivalence was recorded in the axiom. See
+     examples/micro-benchmarks/Test.FunctionalExtensionality.fst for
+     example uses.
+
+     FStar.PropositionalExtensionality was found to be incompatible
+     with the representation of `prop` as the type of all
+     sub-singletons. `prop` has been reformulated as the type of all
+     sub-types of `unit`.
+
+     See issue #1542 for more discussion.
+
+## Syntax
+
+   * We now overload `&` to construct both dependent and non-dependent
+     tuple types. `t1 & t2` is equivalent to `tuple2 t1 t2` whereas
+     `x:t1 & t2` is `dtuple2 t1 (fun x -> t2)`. See
+     examples/micro-benchmarks/TupleSyntax.fst. The main value
+     proposition here is that in contrast to `*`, which clashes with
+     the multiplication on integers, the `&` symbol can be used for
+     tuples while reserving `*` for multiplication.
+
 # Version 0.9.6.0
 
 ## Command line options

INSTALL.md

@@ -24,10 +24,12 @@
 ## Online editor ##
 
 The easiest way to try out F\* quickly is directly in your browser by using
-the [online F\* editor] that's part of the [F\* tutorial].
+either [online F\* editor] that's part of the [F\* tutorial]
+or our new [even cooler online editor] (experimental).
 
 [online F\* editor]: https://www.fstar-lang.org/run.php
 [F\* tutorial]: https://www.fstar-lang.org/tutorial/
+[even cooler online editor]: http://fstar.ht.vc/
 
 ## OPAM package ##
 
@@ -97,15 +99,16 @@ following commands. (On Windows this requires Cygwin and `make`)
 
         $ opam install ocamlfind batteries stdint zarith ppx_deriving ppx_deriving_yojson ocaml-migrate-parsetree process
 
-4. You can verify all the examples, keeping in mind that this might
-   take a long time.
+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
         $ make -j6 -C examples
         $ echo $?    # non-zero means build failed! scroll up for error message!
 
-   Note: This step currently requires having OCaml installed (as for step 3 above).
+   Note: Some of the examples currently require having OCaml installed (as for step 3 above).
 
-   Note: This step currently requires having [KreMLin](https://github.com/FStarLang/kremlin)
+   Note: Some of the examples currently require having [KreMLin](https://github.com/FStarLang/kremlin)
          installed and the `KREMLIN_HOME` variable pointing to its location.
 
    Note: On Linux if you get a file descriptor exhaustion error that looks
@@ -238,9 +241,9 @@ Read on for the more complete solution involving Visual Studio itself.
 
 #### On Linux or Mac OS X using Mono ####
 
-  - Install mono (any version from 4.0.3.0 to 5.10.x),
-            fsharp (version 4.1.x), and
-            msbuild (version 14.1.x-15.6.x)
+  - Install mono (any version from 4.0.3.0 to 5.14.x),
+            fsharp (version 4.1.x, where [on Linux x<=18](https://github.com/FStarLang/FStar/issues/1539)), and
+            msbuild (version 14.1.x-15.8.x)
 
     - On Debian/Ubuntu
 
@@ -249,7 +252,12 @@ Read on for the more complete solution involving Visual Studio itself.
     - On Arch
 
             $ pacman -S mono
-            $ aura -A fsharp msbuild-stable
+            $ aura -A msbuild-stable
+            $ git clone https://github.com/catalin-hritcu/arch-fsharp.git
+            $ cd arch-fsharp
+            $ git checkout fsharp-4.1.18
+            $ makepkg
+            $ pacman -U fsharp-4.1.18-1-any.pkg.tar.xz
 
     - For other Linux distributions check out these links:
       - http://www.mono-project.com/download/#download-lin
@@ -300,7 +308,7 @@ This will install both OCaml and OPAM.
 1. Install OPAM (version 1.2.x).
 
    - Installation instructions are available at various places
-     (e.g., https://github.com/realworldocaml/book/wiki/Installation-Instructions#getting-opam
+     (e.g., https://dev.realworldocaml.org/install.html
      or http://opam.ocaml.org/doc/Install.html).
 
 #### Instructions for all OSes ####
@@ -325,7 +333,7 @@ This will install both OCaml and OPAM.
 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
+  $ opam install ocamlbuild ocamlfind batteries stdint zarith yojson fileutils pprint menhir ulex ppx_deriving ppx_deriving_yojson process pprint ulex
   ```
   Some of the examples also require the `sqlite3` opam package, which depends
   on SQLite itself that you can install with `opam depext sqlite3` (at least on Linux)

Makefile

@@ -13,13 +13,13 @@ clean:
 	$(MAKE) -C ulib clean
 	$(MAKE) -C src/ocaml-output clean
 
-# Shortcuts
+# Shortcuts for developers
 
 # Build the F# version
 0:
 	$(MAKE) -C src/
 
-# Build the OCaml snapshot
+# Build the OCaml snapshot. NOTE: This will not build the standard library, and native tactics will not run
 1:
 	$(MAKE) -C src/ocaml-output