Skip to content

Commit

Permalink
Merge branch 'master' of github:FStarLang/FStar into pristine
Browse files Browse the repository at this point in the history
  • Loading branch information
@mtzguido
mtzguido committed Apr 10, 2023
2 parents e2e70e3 + a8dfd44 commit 986f001
Show file tree
Hide file tree
Showing 1,545 changed files with 71,625 additions and 35,544 deletions.
20 changes: 20 additions & 0 deletions .docker/README.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
In this folder, the following Docker images are in use or can be used:

* `opam.Dockerfile`: tests the F* opam package definition,
`fstar.opam`.

* `package.Dockerfile`: builds a Linux binary package, and tests it
with and without OCaml.

* `release.Dockerfile`: builds, tests and creates a new Linux binary
release. This image is used by the `release.yml` GitHub Actions
workflow.

* `standalone.Dockerfile`: builds and tests F*. This is the main CI
image, used by the `linux-x64.yml` GitHub Actions workflow. It uses
the CI scripts and the configuration files from the `build`
subdirectory (inherited from the previous CI system, but still in
use.)

The Docker images from the `build/*` subdirectories are no longer
used.
154 changes: 2 additions & 152 deletions .docker/build/build_funs.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,154 +60,6 @@ function make_karamel() {
export PATH="$(pwd)/karamel:$PATH"
}

# Update the version number in version.txt and fstar.opam

function update_version_number () {
# version suffix string
local dev='~dev'

# Read the latest version number
last_version_number=$(sed 's!'"$dev"'!!' < version.txt)

# If the only diffs are the snapshot hints and/or CI scripts,
# then we don't need to
# update the version number. This check will fail if the version
# number does not correspond to any existing release. This is
# sound, since if the version number is not a tag, it means that
# it has already been updated since the latest release, so there
# were more than just *.hints diffs, so we can update the version
# number again. Please mind the initial 'v' introducing the
# version tag
if git diff --exit-code v$last_version_number..HEAD -- ':(exclude)*.hints' ':(exclude).docker' ':(exclude).ci' ':(exclude).scripts' ; then
echo "No diffs since latest release other than hints and/or CI scripts"
return 0
fi

# Create a new version number. Fail if it is identical to the
# last version number. In other words, this task should be run at
# most once a day.
this_date=$(date '+%Y.%m.%d')
version_number="$this_date""$dev"
[[ $version_number != $last_version_number ]]

# Update it in version.txt
echo $version_number > version.txt

# Update it in fstar.opam
sed -i 's!^version:.*$!version: "'$version_number'"!' fstar.opam

# Commit the new version number. This is guaranteed to be a
# nonempty change, since version numbers were tested to be
# different
git add -u version.txt fstar.opam
git commit -m "[CI] bump version number to $version_number"
}

function git_add_fstar_snapshot () {
if ! git diff-index --quiet --cached HEAD -- ocaml/*/generated ; then
git ls-files ocaml/*/generated | xargs git add
fi
}

function refresh_fstar_hints() {
[[ -n "$DZOMO_GITHUB_TOKEN" ]] &&
refresh_hints "https://$DZOMO_GITHUB_TOKEN@github.com/FStarLang/FStar.git" "git_add_fstar_snapshot" "regenerate hints + ocaml snapshot" "."
}

# Do we need to update the version number and publish a release?
function is_release_branch () {
[[ "$1" = master || "$1" = _release ]]
}

# Note: this performs an _approximate_ refresh of the hints, in the sense that
# since the hint refreshing job takes about 80 minutes, it's very likely someone
# merged to $CI_BRANCH in the meanwhile, which would invalidate some hints. So, we
# reset to origin/$CI_BRANCH, take in our hints, and push. This is short enough that
# the chances of someone merging in-between fetch and push are low.
function refresh_hints() {
local remote=$1
local extra="$2"
local msg="$3"
local hints_dir="$4"

# Identify the committer
git config --global user.name "Dzomo, the Everest Yak"
git config --global user.email "[email protected]"

# Figure out the branch
CI_BRANCH=${branchname##refs/heads/}
echo "Current branch_name=$CI_BRANCH"

# Record the latest commit
last_commit=$(git rev-parse HEAD)

# Add all the hints, even those not under version control
find $hints_dir/doc -iname '*.hints' | xargs git add
find $hints_dir/examples -iname '*.hints' | xargs git add
find $hints_dir/ulib -iname '*.hints' | xargs git add

# Without the eval, this was doing weird stuff such as,
# when $2 = "git ls-files src/ocaml-output/ | xargs git add",
# outputting the list of files to stdout
eval "$extra"

# Commit only if changes were staged.
# From: https://stackoverflow.com/a/2659808
if ! git diff-index --quiet --cached HEAD -- ; then
git commit -m "[CI] $msg"
else
echo "Hints/snapshot update: no diff"
fi

# Update the version number in version.txt and fstar.opam, and if
# so, commit. Do this only for the master branch.
if is_release_branch $CI_BRANCH ; then
update_version_number
fi

# Memorize the latest commit (which might have been a version number update)
commit=$(git rev-parse HEAD)

# If nothing has been committed (neither hints nor version number), then exit.
if [[ $commit = $last_commit ]] ; then
echo "Nothing has been committed"
return 0
fi

# Drop any other files that were modified as part of the build (e.g.
# parse.fsi)
git reset --hard HEAD
# Move to whatever is the most recent master (that most likely changed in the
# meantime)
git fetch
git checkout $CI_BRANCH
git reset --hard origin/$CI_BRANCH
# Silent, always-successful merge
export GIT_MERGE_AUTOEDIT=no
git merge $commit -Xtheirs

# Check if build hints branch exist on remote and remove it if it exists
exist=$(git branch -a | egrep 'remotes/origin/BuildHints-'$CI_BRANCH | wc -l)
if [ $exist == 1 ]; then
git push $remote :BuildHints-$CI_BRANCH
fi

# Push.
git checkout -b BuildHints-$CI_BRANCH
git push $remote BuildHints-$CI_BRANCH

# Publish a release
if is_release_branch $CI_BRANCH ; then
# Make and test a release
FSTAR_HOME= KRML_HOME= GH_TOKEN=$DZOMO_GITHUB_TOKEN CI_BRANCH=$CI_BRANCH .scripts/process_build.sh
fi
}

function fstar_binary_build () {
fetch_karamel
./.scripts/process_build.sh && echo true >$status_file
}

function fstar_docs_build () {
# First - get fstar built
# Second - run fstar with the --doc flag
Expand Down Expand Up @@ -261,7 +113,7 @@ function fstar_default_build () {

# We should not generate hints when building on Windows
if [[ $localTarget == "uregressions-ulong" && "$OS" != "Windows_NT" ]]; then
refresh_fstar_hints || echo false >$status_file
.scripts/advance.sh refresh_fstar_hints || echo false >$status_file
fi
}

Expand All @@ -288,9 +140,7 @@ function build_fstar() {
return
fi

if [[ $localTarget == "fstar-binary-build" ]]; then
fstar_binary_build
elif [[ $localTarget == "fstar-docs" ]]; then
if [[ $localTarget == "fstar-docs" ]]; then
fstar_docs_build
else
fstar_default_build $target
Expand Down
98 changes: 50 additions & 48 deletions .docker/package.Dockerfile
View file
Original file line number Diff line number Diff line change
@@ -1,20 +1,30 @@
# This Dockerfile should be run from the root FStar directory
# It builds and tests a binary package for F*.
# It is a potential alternative to .scripts/process_build.sh

# Build the package
ARG ocaml_version=4.12
ARG opamthreads=24
ARG CI_THREADS=24

FROM ocaml/opam:ubuntu-20.04-ocaml-$ocaml_version AS fstarbuild

# FIXME: the `opam depext` command should be unnecessary with opam 2.1
RUN opam depext conf-gmp z3.4.8.5 conf-m4
RUN opam depext conf-gmp conf-m4

ADD --chown=opam:opam ./fstar.opam fstar.opam

# Install opam dependencies only
RUN opam install --deps-only ./fstar.opam
# Install opam dependencies only, but not z3
RUN grep -v z3 < fstar.opam > fstar-no-z3.opam && \
rm fstar.opam && \
opam install --deps-only ./fstar-no-z3.opam && \
rm fstar-no-z3.opam

# Install GitHub CLI
# From https://github.com/cli/cli/blob/trunk/docs/install_linux.md#debian-ubuntu-linux-raspberry-pi-os-apt
RUN { type -p curl >/dev/null || sudo apt-get install curl -y ; } \
&& curl -fsSL https://cli.github.com/packages/githubcli-archive-keyring.gpg | sudo dd of=/usr/share/keyrings/githubcli-archive-keyring.gpg \
&& sudo chmod go+r /usr/share/keyrings/githubcli-archive-keyring.gpg \
&& echo "deb [arch=$(dpkg --print-architecture) signed-by=/usr/share/keyrings/githubcli-archive-keyring.gpg] https://cli.github.com/packages stable main" | sudo tee /etc/apt/sources.list.d/github-cli.list > /dev/null \
&& sudo apt-get update \
&& sudo apt-get install gh -y

# Install .NET
RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends \
Expand All @@ -26,28 +36,35 @@ RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends \
# So, we use manual install instead, from https://docs.microsoft.com/en-us/dotnet/core/install/linux-scripted-manual#manual-install
ENV DOTNET_ROOT /home/opam/dotnet
RUN sudo apt-get install --yes --no-install-recommends \
wget

RUN wget https://download.visualstudio.microsoft.com/download/pr/cd0d0a4d-2a6a-4d0d-b42e-dfd3b880e222/008a93f83aba6d1acf75ded3d2cfba24/dotnet-sdk-6.0.400-linux-x64.tar.gz && \
wget \
&& \
wget 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

ENV PATH=${PATH}:$DOTNET_ROOT:$DOTNET_ROOT/tools

ADD --chown=opam:opam ./ FStar/
# Configure the git user
RUN git config --global user.name "Dzomo, the Everest Yak" && \
git config --global user.email "[email protected]"

# Build the package,
RUN eval $(opam env) && env Z3_LICENSE="$(opam config expand '%{prefix}%')/.opam-switch/sources/z3.4.8.5/LICENSE.txt" OTHERFLAGS='--admit_smt_queries true' make -C FStar -j $opamthreads package
# Download and extract z3, but do not add it in the PATH
# We download a z3 that does not depend on libgomp
ADD --chown=opam:opam https://github.com/tahina-pro/z3/releases/download/z3-4.8.5-linux-clang/z3-4.8.5-linux-clang-x86_64.tar.gz z3.tar.gz
RUN tar xf z3.tar.gz

# Create a separate image to test the package
ADD --chown=opam:opam ./ FStar/

# Test the F* binary package
# Build the package with our Z3
RUN eval $(opam env) && env OTHERFLAGS='--admit_smt_queries true' PATH=$HOME/z3:$PATH make -j $CI_THREADS -C FStar package

# Test the fresh package without OCaml
# Test the package with its Z3, without OCaml or any other dependency
FROM ubuntu:20.04 AS fstarnoocaml
ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update
RUN apt-get --yes install --no-install-recommends make sudo libgomp1

# Install some dependencies
RUN apt-get update && \
apt-get install --yes --no-install-recommends \
make

# Create a new user and give them sudo rights
RUN useradd -d /home/test test
Expand All @@ -59,33 +76,18 @@ ENV HOME /home/test
WORKDIR $HOME
SHELL ["/bin/bash", "--login", "-c"]

# Copy the package
COPY --from=fstarbuild /home/opam/FStar/src/ocaml-output/fstar.tar.gz /home/test/fstar.tar.gz
RUN tar xzf fstar.tar.gz

# Copy tests, examples and docs
ADD --chown=test:test examples/ fstar_examples/
ADD --chown=test:test doc/ fstar_doc/

# Case 3: test F* package without OCaml

# Test the package with FSTAR_HOME defined
# Move z3 elsewhere
# FROM fstarnoocaml
# ENV FSTAR_HOME=$HOME/fstar
# RUN mkdir -p $HOME/bin && ln -s $FSTAR_HOME/bin/z3 $HOME/bin/
# ENV PATH="${HOME}/bin:${PATH}"
# RUN make -C fstar_examples -j $opamthreads
# RUN make -C fstar_doc/tutorial -j $opamthreads regressions

# Test the package with F* in the PATH instead
FROM fstarnoocaml
ENV PATH="/home/test/fstar/bin:${PATH}"
RUN make -C fstar_examples -j $opamthreads
RUN make -C fstar_doc/tutorial -j $opamthreads regressions

FROM fstarnoocaml
# This is the last image. So we can also copy the file that contains
# the desired filename for the package, to be extracted via
# `docker cp`
COPY --from=fstarbuild /home/opam/FStar/src/ocaml-output/version_platform.txt /home/test/version_platform.txt
# Copy the package and the test script
COPY --from=fstarbuild /home/opam/FStar/src/ocaml-output/fstar.tar.gz /home/test/FStar/src/ocaml-output/fstar.tar.gz
COPY --from=fstarbuild /home/opam/FStar/.scripts/test_package.sh /home/test/FStar/.scripts/test_package.sh

# Test the package
ARG CI_THREADS
RUN env CI_THREADS=$CI_THREADS /home/test/FStar/.scripts/test_package.sh

# Test the package with its Z3, with OCaml
FROM fstarbuild
ARG CI_THREADS
# Copy a dummy file to introduce an artificial dependence to the fstarnoocaml stage
# to force buildx to build that stage as well
COPY --from=fstarnoocaml /home/test/FStar/.scripts/test_package.sh /tmp/dummy
RUN eval $(opam env) && env CI_THREADS=$CI_THREADS ./FStar/.scripts/test_package.sh
Loading

0 comments on commit 986f001

Please sign in to comment.