Merge branch 'master' into nik_wf

.devcontainer/devcontainer.json

@@ -0,0 +1,29 @@
+{
+  "name": "F* minimal devcontainer",
+  "build": {
+    "dockerfile": "minimal.Dockerfile"
+  },
+  "customizations": {
+    "vscode": {
+      "extensions": [
+        "FStarLang.fstar-vscode-assistant"
+      ]
+    }
+  },
+  "remoteEnv": {
+    "FSTAR_DEVCONTAINER": "minimal"
+    // ^ We just set this in case we ever need to distinguish
+    // we are running in a codespace.
+  },
+  // Runs only once when container is prepared
+  "onCreateCommand": {
+    "link_to_home_bin" : "ln -s $(realpath bin/fstar.exe) ~/bin/fstar.exe"
+  },
+  // Runs periodically and/or when content of repo changes
+  "updateContentCommand": {
+    "make": "bash -i .devcontainer/onUpdate.sh"
+  },
+  // These run only when the container is assigned to a user
+  "postCreateCommand": {
+  }
+}

.devcontainer/minimal.Dockerfile

@@ -0,0 +1,65 @@
+FROM ubuntu:latest
+
+SHELL ["/bin/bash", "-c"]
+
+# Base dependencies: opam
+# CI dependencies: jq (to identify F* branch)
+# python3 (for interactive tests)
+# libicu (for .NET, cf. https://aka.ms/dotnet-missing-libicu )
+RUN apt-get update \
+    && apt-get install -y --no-install-recommends \
+      ca-certificates \
+      curl \
+      wget \
+      git \
+      gnupg \
+      sudo \
+      python3 \
+      python-is-python3 \
+      libicu70 \
+      libgmp-dev \
+      opam \
+    && apt-get clean -y
+# FIXME: libgmp-dev should be installed automatically by opam,
+# but it is not working, so just adding it above.
+
+# Create a new user and give them sudo rights
+ARG USER=vscode
+RUN useradd -d /home/$USER -s /bin/bash -m $USER
+RUN echo "$USER ALL=NOPASSWD: ALL" >> /etc/sudoers
+USER $USER
+ENV HOME /home/$USER
+WORKDIR $HOME
+RUN mkdir -p $HOME/bin
+
+# Make sure ~/bin is in the PATH
+RUN echo 'export PATH=$HOME/bin:$PATH' | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile
+
+# Install dotnet
+ENV DOTNET_ROOT /home/$USER/dotnet
+RUN wget -nv https://download.visualstudio.microsoft.com/download/pr/cd0d0a4d-2a6a-4d0d-b42e-dfd3b880e222/008a93f83aba6d1acf75ded3d2cfba24/dotnet-sdk-6.0.400-linux-x64.tar.gz && \
+    mkdir -p $DOTNET_ROOT && \
+    tar xf dotnet-sdk-6.0.400-linux-x64.tar.gz -C $DOTNET_ROOT && \
+    echo 'export PATH=$PATH:$DOTNET_ROOT:$DOTNET_ROOT/tools' | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile && \
+    rm -f dotnet-sdk*.tar.gz
+
+# Install OCaml
+ARG OCAML_VERSION=4.12.0
+RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing
+RUN opam option depext-run-installs=true
+ENV OPAMYES=1
+RUN opam install --yes batteries zarith stdint yojson dune menhir menhirLib pprint sedlex ppxlib process ppx_deriving ppx_deriving_yojson
+
+# Get compiled Z3
+RUN wget -nv https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip \
+ && unzip z3-4.8.5-x64-ubuntu-16.04.zip \
+ && cp z3-4.8.5-x64-ubuntu-16.04/bin/z3 $HOME/bin/z3 \
+ && rm -r z3-4.8.5-*
+
+WORKDIR $HOME
+
+# Instrument .bashrc to set the opam switch. Note that this
+# just appends the *call* to eval $(opam env) in these files, so we
+# compute the new environments fter the fact. Calling opam env here
+# would perhaps thrash some variables set by the devcontainer infra.
+RUN echo 'eval $(opam env --set-switch)' | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile

.devcontainer/onUpdate.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+# Prebuild F* and library
+make -j$(nproc) ADMIT=1 |& tee .devcontainer_build.log

.docker/build/build_funs.sh

@@ -30,7 +30,7 @@ function fetch_karamel() {
     git fetch origin
     local ref=$(jq -c -r '.RepoVersions["karamel_version"]' "$rootPath/.docker/build/config.json" )
     if [[ $ref == "null" ]]; then
-        echo "Unale to find RepoVersions.karamel_version on $rootPath/.docker/build/config.json"
+        echo "Unable to find RepoVersions.karamel_version on $rootPath/.docker/build/config.json"
         return -1
     fi
 
@@ -41,11 +41,11 @@ function fetch_karamel() {
 
     # Install the Karamel dependencies
     pushd $KRML_HOME
-    .docker/build/install-other-deps.sh
+    OPAMYES=true .docker/build/install-other-deps.sh
     popd
 }
 
-function make_karamel() {
+function make_karamel_pre() {
     # Default build target is minimal, unless specified otherwise
     local localTarget
     if [[ $1 == "" ]]; then
@@ -56,6 +56,9 @@ function make_karamel() {
 
     make -C karamel -j $threads $localTarget ||
         (cd karamel && git clean -fdx && make -j $threads $localTarget)
+}
+
+function make_karamel_post() {
     OTHERFLAGS='--admit_smt_queries true' make -C karamel/krmllib -j $threads
     export PATH="$(pwd)/karamel:$PATH"
 }
@@ -75,9 +78,10 @@ function fstar_default_build () {
         export OTHERFLAGS="--record_hints $OTHERFLAGS"
     fi
 
-    # Start fetching while we build F*
+    # Start fetching and building karamel while we build F*
     if [[ -z "$CI_NO_KARAMEL" ]] ; then
         fetch_karamel
+        make_karamel_pre
     fi &
 
     # Build F*, along with fstarlib
@@ -95,13 +99,15 @@ function fstar_default_build () {
 
     wait # for fetches above
 
-    # Build karamel if enabled
+    # Build the rest of karamel if enabled (i.e. verify krmllib)
     if [[ -z "$CI_NO_KARAMEL" ]] ; then
         # The commands above were executed in sub-shells and their EXPORTs are not
         # propagated to the current shell. Re-do.
         export_home KRML "$(pwd)/karamel"
-        make_karamel
+        make_karamel_post
     fi
+    # NOTE: We cannot run this in parallel with F* regressions as some
+    # examples depend on having krmllib checked.
 
     # Once F* is built, run its main regression suite.
     $gnutime make -j $threads -k ci-$localTarget && echo true >$status_file

.github/workflows/linux-x64-rebuild-base.yaml

@@ -42,7 +42,7 @@ jobs:
           echo "ci_docker_image_tag=$ci_docker_image_tag" >> $GITHUB_ENV
 
           CI_TARGET=uregressions
-          docker build --no-cache -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg FSTAR_CI_BASE=$TEMP_IMAGE_NAME --build-arg CI_TARGET="$CI_TARGET" . |& tee BUILDLOG
+          docker build --no-cache -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg FSTAR_CI_BASE=$TEMP_IMAGE_NAME --build-arg CI_TARGET="$CI_TARGET" --build-arg CI_THREADS=$(nproc) . |& tee BUILDLOG
           ci_docker_status=$(docker run $ci_docker_image_tag /bin/bash -c 'cat $FSTAR_HOME/status.txt' || echo false)
           $ci_docker_status
 

.github/workflows/linux-x64.yaml

@@ -63,16 +63,16 @@ jobs:
             CI_IMAGEBUILD_INITIAL_TIMESTAMP=$(date '+%s')
             docker build -f .docker/base.Dockerfile -t fstar_ci_base .
             CI_IMAGEBUILD_FINAL_TIMESTAMP=$(date '+%s')
-            echo "CI_IMAGEBUILD_INITIAL_TIMESTAMP='$CI_IMAGEBUILD_INITIAL_TIMESTAMP'" >> $GITHUB_ENV
-            echo "CI_IMAGEBUILD_FINAL_TIMESTAMP='$CI_IMAGEBUILD_FINAL_TIMESTAMP'" >> $GITHUB_ENV
+            echo "CI_IMAGEBUILD_INITIAL_TIMESTAMP=$CI_IMAGEBUILD_INITIAL_TIMESTAMP" >> $GITHUB_ENV
+            echo "CI_IMAGEBUILD_FINAL_TIMESTAMP=$CI_IMAGEBUILD_FINAL_TIMESTAMP" >> $GITHUB_ENV
           fi
 
       - name: Build FStar and its dependencies
         run: |
           ci_docker_image_tag=fstar:local-run-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT
           echo "ci_docker_image_tag=$ci_docker_image_tag" >> $GITHUB_ENV
           if [[ -z $CI_TARGET ]] ; then CI_TARGET=uregressions ; fi
-          docker build -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg CI_BRANCH=$GITHUB_REF_NAME --build-arg CI_TARGET="$CI_TARGET" --build-arg RESOURCEMONITOR=$RESOURCEMONITOR $CI_DO_NO_KARAMEL . |& tee BUILDLOG
+          docker build -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg CI_BRANCH=$GITHUB_REF_NAME --build-arg CI_TARGET="$CI_TARGET" --build-arg RESOURCEMONITOR=$RESOURCEMONITOR --build-arg CI_THREADS=$(nproc) $CI_DO_NO_KARAMEL . |& tee BUILDLOG
           ci_docker_status=$(docker run $ci_docker_image_tag /bin/bash -c 'cat $FSTAR_HOME/status.txt' || echo false)
           if $ci_docker_status && [[ -z "$CI_SKIP_IMAGE_TAG" ]] ; then
             if ! { echo $GITHUB_REF_NAME | grep '/' ; } ; then

.gitignore

@@ -98,3 +98,6 @@ nubuild.progress
 
 # Nuget packages
 nuget/
+
+# devcontainer temp files
+/.devcontainer_build.log

CHANGES.md

@@ -83,6 +83,15 @@ Guidelines for the changelog:
     collects all those refinement goals and presents them to the user
     tactic for furhter processing.
 
+  * A new version of the tactics and reflection engine was started by
+    PR https://github.com/FStarLang/FStar/pull/2960. The new version is
+    under the `FStar.Tactics.V2` and `FStar.Reflection.V2` namespaces
+    and should be considered *experimental* and subject to change. The
+    old version is still supported, available under the corresponding V1
+    namespaces. All the old, unqualified modules point to V1, so users
+    should not need to make any change to their code to continue using
+    V1.
+
 ## Typeclass argument syntax
 
   * The syntax for a typeclass argument (a.k.a. constraint) is now `{| ... |}`

Makefile

@@ -24,7 +24,7 @@ fstar:
 	@echo "  DUNE INSTALL"
 	$(Q)cd $(DUNE_SNAPSHOT) && dune install --profile=$(FSTAR_BUILD_PROFILE) --prefix=$(FSTAR_CURDIR)
 
-.PHONY: verify-ulin
+.PHONY: verify-ulib
 verify-ulib:
 	+$(Q)$(MAKE) -C ulib
 
@@ -132,24 +132,37 @@ output:
 	+$(Q)$(MAKE) -C tests/ide/emacs accept
 	+$(Q)$(MAKE) -C tests/bug-reports output-accept
 
+# This rule is meant to mimic what the docker based CI does, but it
+# is not perfect. In particular it will not look for a diff on the
+# snapshot, nor run the build-standalone script.
 .PHONY: ci
 ci:
-	+$(Q)FSTAR_HOME=$(CURDIR) $(MAKE) ci-pre
-	+$(Q)FSTAR_HOME=$(CURDIR) $(MAKE) ci-post
+	+$(Q)OTHERFLAGS="--use_hints" FSTAR_HOME=$(CURDIR) $(MAKE) ci-pre
+	+$(Q)OTHERFLAGS="--use_hints" FSTAR_HOME=$(CURDIR) $(MAKE) ci-post
 
+# This rule runs a CI job in a local container, exactly like is done for
+# CI.
 .PHONY: docker-ci
 docker-ci:
 	docker build -f .docker/standalone.Dockerfile --build-arg CI_THREADS=$(shell nproc) .
 
 .PHONY: ci-pre
-ci-pre:
+ci-pre: ci-rebootstrap
+
+.PHONY: ci-rebootstrap
+ci-rebootstrap:
 	+$(Q)$(MAKE) full-bootstrap FSTAR_BUILD_PROFILE=test
+
+.PHONY: ci-ocaml-test
+ci-ocaml-test:
 	+$(Q)$(MAKE) -C src ocaml-unit-tests
-	+$(Q)$(MAKE) -C ulib ulib-in-fsharp    #build ulibfs
+
+.PHONY: ci-ulib-in-fsharp
+ci-ulib-in-fsharp:
+	+$(Q)$(MAKE) -C ulib ulib-in-fsharp
 
 .PHONY: ci-post
-ci-post: ci-uregressions
-	+if [ -n "${FSTAR_CI_UREGRESSIONS_ULONG}" ]; then $(MAKE) ci-uregressions-ulong; fi
+ci-post: ci-ulib-in-fsharp ci-ocaml-test ci-uregressions
 
 .PHONY: ci-uregressions
 ci-uregressions: