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

.docker/base.Dockerfile

@@ -84,7 +84,7 @@ ADD fstar.opam $HOME/fstar.opam
 RUN opam install --confirm-level=unsafe-yes --deps-only $HOME/fstar.opam && opam clean
 
 # Some karamel dependencies
-RUN opam install --confirm-level=unsafe-yes fix fileutils visitors camlp4 wasm ulex && opam clean
+RUN opam install --confirm-level=unsafe-yes fix fileutils visitors camlp4 wasm ulex uucp && opam clean
 
 # Set up $HOME/bin. Note, binaries here take precedence over OPAM
 RUN mkdir $HOME/bin

.docker/build/build-standalone.sh

@@ -4,9 +4,8 @@ set -x
 
 set -e # abort on errors
 
-target=$1
-threads=$2
-branchname=$3
+threads=$1
+branchname=$2
 
 build_home="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 . "$build_home"/build_funs.sh
@@ -15,7 +14,7 @@ rootPath=$(pwd)
 result_file="result.txt"
 status_file="status.txt"
 ORANGE_FILE="orange_file.txt"
-build_fstar $target
+build_fstar ci
 
 # If RESOURCEMONITOR is defined, then make an rmon/ directory with
 # resource usage information

.docker/build/build_funs.sh

@@ -20,7 +20,7 @@ function export_home() {
 # By default, karamel master works against F* stable. Can also be overridden.
 function fetch_karamel() {
     if [ ! -d karamel ]; then
-        git clone https://github.com/FStarLang/karamel karamel
+        git clone --depth 1 https://github.com/FStarLang/karamel karamel
     fi
 
     cd karamel
@@ -43,16 +43,7 @@ function fetch_karamel() {
 }
 
 function make_karamel_pre() {
-    # Default build target is minimal, unless specified otherwise
-    local localTarget
-    if [[ $1 == "" ]]; then
-        localTarget="minimal"
-    else
-        localTarget="$1"
-    fi
-
-    make -C karamel -j $threads $localTarget ||
-        (cd karamel && git clean -fdx && make -j $threads $localTarget)
+    make -C karamel -j $threads minimal
 }
 
 function fstar_docs_build () {
@@ -64,19 +55,16 @@ function fstar_docs_build () {
 }
 
 function fstar_default_build () {
-    localTarget=$1
-
-    if [[ $localTarget == "uregressions-ulong" ]]; then
+    if [[ -n "$CI_RECORD_HINTS" ]]; then
         export OTHERFLAGS="--record_hints $OTHERFLAGS"
     fi
 
     # Start fetching and building karamel while we build F*
     if [[ -z "$CI_NO_KARAMEL" ]] ; then
-        fetch_karamel
-        make_karamel_pre
-        export_home KRML "$(pwd)/karamel"
         export FSTAR_CI_TEST_KARAMEL=1
-    fi &
+        export_home KRML "$(pwd)/karamel"
+        (fetch_karamel ; make_karamel_pre) &
+    fi
 
     # Build F*, along with fstarlib
     if ! make -j $threads ci-pre; then
@@ -95,7 +83,7 @@ function fstar_default_build () {
 
     # Once F* is built, run its main regression suite. This also runs the karamel
     # test (unless CI_NO_KARAMEL is set).
-    $gnutime make -j $threads -k ci-$localTarget && echo true >$status_file
+    $gnutime make -j $threads -k ci-post && echo true >$status_file
     echo Done building FStar
 
     if [ -z "${FSTAR_CI_NO_GITDIFF}" ]; then
@@ -143,8 +131,8 @@ function build_fstar() {
 
     if [[ $localTarget == "fstar-docs" ]]; then
         fstar_docs_build
-    else
-        fstar_default_build $target
+    elif [[ $localTarget == "ci" ]]; then
+        fstar_default_build
     fi
 
     if [[ $(cat $status_file) != "true" ]]; then

.docker/standalone.Dockerfile

@@ -14,13 +14,12 @@ WORKDIR $HOME/FStar
 RUN opam install --confirm-level=unsafe-yes --deps-only ./fstar.opam && opam clean
 
 # Run CI proper
-ARG CI_TARGET=uregressions
 ARG CI_THREADS=24
 ARG CI_BRANCH=master
 ARG CI_NO_KARAMEL=
 ARG RESOURCEMONITOR=
 ARG FSTAR_CI_NO_GITDIFF=
-RUN eval $(opam env) && Z3_LICENSE="$(opam config expand '%{prefix}%')/.opam-switch/sources/z3.4.8.5/LICENSE.txt" CI_NO_KARAMEL=$CI_NO_KARAMEL .docker/build/build-standalone.sh $CI_TARGET $CI_THREADS $CI_BRANCH
+RUN eval $(opam env) && Z3_LICENSE="$(opam config expand '%{prefix}%')/.opam-switch/sources/z3.4.8.5/LICENSE.txt" CI_NO_KARAMEL=$CI_NO_KARAMEL .docker/build/build-standalone.sh $CI_THREADS $CI_BRANCH
 
 WORKDIR $HOME
 ENV FSTAR_HOME $HOME/FStar

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

@@ -23,7 +23,7 @@ jobs:
 
     steps:
       - name: Check out repo
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Rebuild base image from scratch
         run: |
@@ -41,8 +41,7 @@ jobs:
           ci_docker_image_tag=fstar:update-base-test-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT
           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" --build-arg CI_THREADS=$(nproc) . |& 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_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
 
@@ -111,7 +110,8 @@ jobs:
       - name: Post to the Slack channel
         if: ${{ always() }}
         id: slack
-        uses: slackapi/[email protected]
+        continue-on-error: true
+        uses: slackapi/[email protected]
         with:
           channel-id: ${{ env.CI_SLACK_CHANNEL }}
           payload: |

.github/workflows/linux-x64.yaml

@@ -34,15 +34,15 @@ jobs:
         run: |
           echo "CI_INITIAL_TIMESTAMP=$(date '+%s')" >> $GITHUB_ENV
       - name: Check out repo        
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
       - name: Identify the notification channel
         run: |
           echo "CI_SLACK_CHANNEL=$(jq -c -r '.NotificationChannel' .docker/build/config.json)" >> $GITHUB_ENV
       - name: Set the refresh hints flag
         if: ${{ (github.event_name == 'workflow_dispatch') && inputs.ci_refresh_hints }}
         run: |
           # NOTE: this causes the build to record hints
-          echo "CI_TARGET=uregressions-ulong" >> $GITHUB_ENV
+          echo "CI_RECORD_HINTS_ARG=--build-arg CI_RECORD_HINTS=1" >> $GITHUB_ENV
       - name: Populate no karamel arg
         if: ${{ (github.event_name == 'workflow_dispatch') && inputs.ci_no_karamel }}
         run: |
@@ -71,8 +71,7 @@ jobs:
         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 --build-arg CI_THREADS=$(nproc) $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 RESOURCEMONITOR=$RESOURCEMONITOR --build-arg CI_THREADS=$(nproc) $CI_RECORD_HINTS_ARG $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
@@ -117,7 +116,7 @@ jobs:
       - name: Save resource monitor summary as artifact
         if: ${{ always () && vars.FSTAR_CI_RESOURCEMONITOR == '1' }}
         continue-on-error: true
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: Resource usage information (summary)
           path: |
@@ -126,7 +125,7 @@ jobs:
       - name: Save resource monitor files as artifact
         if: ${{ always () && vars.FSTAR_CI_RESOURCEMONITOR == '1' }}
         continue-on-error: true
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: Resource usage information (individual)
           path: |
@@ -179,7 +178,8 @@ jobs:
       - name: Post to the Slack channel
         if: ${{ always() }}
         id: slack
-        uses: slackapi/[email protected]
+        continue-on-error: true
+        uses: slackapi/[email protected]
         with:
           channel-id: ${{ env.CI_SLACK_CHANNEL }}
           payload: |

.github/workflows/macos-build.yml

@@ -11,16 +11,16 @@ jobs:
 
     steps:
     - name: Checkout FStar
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         path: FStar
     - name: Checkout everest
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         repository: project-everest/everest
         path: FStar/.github/everest
     - name: Install .NET SDK
-      uses: actions/setup-dotnet@v3
+      uses: actions/setup-dotnet@v4
       with:
         dotnet-version: '6.0.x'
     - name: Setup dependencies
@@ -34,7 +34,7 @@ jobs:
         source FStar/.github/env.sh
         PACKAGE_DOCS=0 make -j -C FStar package
     - name: Upload artifact
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: fstar-Darwin_x86_64.tar.gz
         path: FStar/src/ocaml-output/fstar.tar.gz

.github/workflows/nix.yaml

@@ -10,7 +10,7 @@ jobs:
   nix-build:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
     - uses: DeterminateSystems/nix-installer-action@main
     - uses: DeterminateSystems/magic-nix-cache-action@main
     - name: Build

.github/workflows/release.yml

@@ -11,7 +11,7 @@ jobs:
 
     steps:
     - name: Check out repo        
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
     - name: Package and release FStar
       run: |
           ci_docker_image_tag=fstar-release:local-run-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT
@@ -33,16 +33,16 @@ jobs:
 
     steps:
     - name: Checkout FStar
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         path: FStar
     - name: Checkout everest
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         repository: project-everest/everest
         path: FStar/.github/everest
     - name: Install .NET SDK
-      uses: actions/setup-dotnet@v2
+      uses: actions/setup-dotnet@v4
       with:
         dotnet-version: '6.0.x'
     - name: Setup dependencies
@@ -62,7 +62,7 @@ jobs:
 
     steps:
     - name: Check out repo        
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
 
     - name: Package and release FStar
       shell: C:\cygwin64\bin\bash.exe --login '{0}'

.github/workflows/windows.yml

@@ -11,7 +11,7 @@ jobs:
 
     steps:
     - name: Check out repo        
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
 
     - name: Build a package
       shell: C:\cygwin64\bin\bash.exe --login '{0}'
@@ -22,7 +22,7 @@ jobs:
       run: |
         env CI_THREADS=24 $GITHUB_WORKSPACE/.scripts/test_package.sh && echo "There is a CR at the end of this line"
     - name: Upload artifact
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: fstar-Windows_x86_64.zip
         path: src\ocaml-output\fstar.zip

FStar.fst.config.json

@@ -1,5 +1,5 @@
 {
-  "fstar_exe": "fstar.exe",
+  "fstar_exe": "./bin/fstar.exe",
   "options": [
     "--cache_dir", ".cache"
   ],

Makefile

@@ -125,7 +125,7 @@ clean-intermediate:
 .PHONY: hints
 hints:
 	+$(Q)OTHERFLAGS="${OTHERFLAGS} --record_hints" $(MAKE) -C ulib/
-	+$(Q)OTHERFLAGS="${OTHERFLAGS} --record_hints" $(MAKE) ci-uregressions
+	+$(Q)OTHERFLAGS="${OTHERFLAGS} --record_hints" $(MAKE) ci-uregressions ci-ulib-extra
 
 .PHONY: bench
 bench:
@@ -194,7 +194,7 @@ ci-ulib-extra:
 	+$(Q)$(MAKE) -C ulib extra
 
 .PHONY: ci-ulib-in-fsharp
-ci-ulib-in-fsharp: ci-ulib-extra
+ci-ulib-in-fsharp:
 	+$(Q)$(MAKE) -C ulib ulib-in-fsharp
 
 .PHONY: ci-post
@@ -209,10 +209,6 @@ ci-post:						\
 ci-uregressions:
 	+$(Q)$(MAKE) -C src uregressions
 
-.PHONY: ci-uregressions-ulong
-ci-uregressions-ulong:
-	+$(Q)$(MAKE) -C src uregressions-ulong
-
 .PHONY: ci-karamel-test
 ci-karamel-test: ci-krmllib
 	+$(Q)$(MAKE) -C examples krml_tests

examples/layeredeffects/IteSoundness.fst

@@ -133,17 +133,17 @@ let mbind (a:Type) (b:Type) (f:mrepr a) (g:a -> mrepr b) : mrepr b = g f
  *)
 
 let mif_then_else (a:Type)
-  ([@@@ an_attr] phi:Type0)
-  ([@@@ an_attr] bb:squash phi) 
+  (phi:Type0)
+  (bb:squash phi)
   (f:mrepr a)
   (g:mrepr a)
   (b:bool)
   : Type
   = mrepr a
 
 let msubcomp (a:Type)
-  ([@@@ an_attr] phi:Type0)
-  ([@@@ an_attr] bb:squash phi)  (f:mrepr a)
+  (phi:Type0)
+  (bb:squash phi)  (f:mrepr a)
   : mrepr a = f
 
 let an_attr1 = ()