Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 2 additions & 3 deletions .docker/build/build-standalone.sh
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,5 @@ build_home="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
rootPath=$(pwd)
export_home KRML "$rootPath"
result_file="result.txt"
exec_build $target

grep Success < "$result_file"
out_file="log.txt"
{ { { { { { exec_build ; } 3>&1 1>&2 2>&3 ; } | sed -u 's!^![STDERR]!' ; } 3>&1 1>&2 2>&3 ; } | sed -u 's!^![STDOUT]!' ; } 2>&1 ; } | awk '{ print strftime("[%Y-%m-%d %H:%M:%S]"), $0 }' | tee $out_file
46 changes: 39 additions & 7 deletions .docker/standalone.Dockerfile
Original file line number Diff line number Diff line change
@@ -1,13 +1,41 @@
# This Dockerfile should be run from the root FStar directory
# This Dockerfile should be run from the root Karamel directory

ARG ocaml_version=4.12
FROM ocaml/opam:ubuntu-ocaml-$ocaml_version
FROM ubuntu:22.04

ADD --chown=opam:opam ./ karamel/
WORKDIR karamel
# CI dependencies: opam, jq (to identify F* branch)
RUN apt-get update && \
apt-get install -y --no-install-recommends \
jq \
ca-certificates \
curl \
wget \
git \
gawk \
coreutils \
sudo \
opam

# CI dependencies: jq (to identify F* branch)
RUN sudo apt-get install -y --no-install-recommends jq

# Create a new user and give them sudo rights
# NOTE: we give them the name "opam" to keep compatibility with
# derived hierarchical CI
RUN useradd -d /home/opam opam
RUN echo 'opam ALL=NOPASSWD: ALL' >> /etc/sudoers
RUN mkdir /home/opam
RUN chown opam:opam /home/opam
USER opam
ENV HOME /home/opam
WORKDIR $HOME
SHELL ["/bin/bash", "--login", "-c"]

# Install OCaml
ARG OCAML_VERSION=4.12.0
RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing
RUN opam env --set-switch | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile
ENV OPAMYES=1

ADD --chown=opam:opam ./ $HOME/karamel/
WORKDIR $HOME/karamel

# Dependencies (F* and opam packages)
ENV FSTAR_HOME=$HOME/FStar
Expand All @@ -29,3 +57,7 @@ RUN sudo pip3 install sphinx==1.7.2 jinja2==3.0.0 sphinx_rtd_theme
ARG CI_THREADS=24
ARG CI_BRANCH=master
RUN --mount=type=secret,id=DZOMO_GITHUB_TOKEN eval $(opam env) && DZOMO_GITHUB_TOKEN=$(sudo cat /run/secrets/DZOMO_GITHUB_TOKEN) .docker/build/build-standalone.sh $CI_THREADS $CI_BRANCH
# RUN eval $(opam env) && .docker/build/build-standalone.sh $CI_THREADS $CI_BRANCH

WORKDIR $HOME
ENV KRML_HOME=$HOME/karamel
20 changes: 15 additions & 5 deletions .github/workflows/linux-x64-hierarchic.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -23,14 +23,24 @@ jobs:
if docker image inspect fstar:local-branch-$FSTAR_BRANCH ; then echo KRML_CI_FLAVOR=hierarchic >> $GITHUB_ENV ; else echo KRML_CI_FLAVOR=standalone >> $GITHUB_ENV ; fi
- name: Build Karamel and its dependencies
run: |
if { echo $GITHUB_REF_NAME | grep '/' ; } ; then
docker_build_tag_opt=
else
docker_build_tag_opt="-t karamel:local-branch-$GITHUB_REF_NAME"
ci_docker_image_tag=karamel:local-run-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT
docker buildx build --secret id=DZOMO_GITHUB_TOKEN -t $ci_docker_image_tag -f .docker/$KRML_CI_FLAVOR.Dockerfile --build-arg FSTAR_BRANCH=$FSTAR_BRANCH --build-arg CI_BRANCH=$GITHUB_REF_NAME .
if docker run $ci_docker_image_tag /bin/bash -c 'cat $KRML_HOME/result.txt' | grep Success ; then ci_docker_status=true ; else ci_docker_status=false ; fi
if $ci_docker_status ; then
if ! { echo $GITHUB_REF_NAME | grep '/' ; } ; then
docker tag $ci_docker_image_tag karamel:local-branch-$GITHUB_REF_NAME
fi
docker tag $ci_docker_image_tag karamel:local-commit-$GITHUB_SHA
fi
docker buildx build --secret id=DZOMO_GITHUB_TOKEN $docker_build_tag_opt -t karamel:local-commit-$GITHUB_SHA -f .docker/$KRML_CI_FLAVOR.Dockerfile --build-arg FSTAR_BRANCH=$FSTAR_BRANCH --build-arg CI_BRANCH=$GITHUB_REF_NAME .
docker run $ci_docker_image_tag /bin/bash -c 'cat $KRML_HOME/log.txt' > log.txt
$ci_docker_status
env:
DZOMO_GITHUB_TOKEN: ${{ secrets.DZOMO_GITHUB_TOKEN }}
- name: Archive build log
uses: actions/upload-artifact@v3
with:
name: log
path: log.txt
- name: Compute elapsed time
if: ${{ always() }}
run: |
Expand Down
2 changes: 1 addition & 1 deletion karamel.opam
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ depends: [
"process"
"fix"
"visitors"
"wasm" {>= "1.1.1"}
"wasm" {>= "2.0.0"}
"ppx_deriving"
"ppx_deriving_yojson"
"fstar"
Expand Down
44 changes: 22 additions & 22 deletions krmllib/hints/C.Endianness.fst.hints

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions krmllib/hints/C.Failure.fst.hints

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading