From 814cfa3657ea21386279d385cd482d4de774bd96 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Mon, 21 Aug 2023 15:22:55 -0700 Subject: [PATCH] install-other-deps should install everything except F* --- .docker/build/build-hierarchic.sh | 4 +--- .docker/build/build-standalone.sh | 12 ----------- .docker/build/build_funs.sh | 3 --- .docker/build/install-deps.sh | 23 --------------------- .docker/build/install-krml-funs.sh | 31 ----------------------------- .docker/build/install-other-deps.sh | 25 +++++++++++++++++++++++ .docker/build/install-steel-funs.sh | 19 ------------------ .docker/hierarchic.Dockerfile | 3 ++- 8 files changed, 28 insertions(+), 92 deletions(-) delete mode 100644 .docker/build/install-krml-funs.sh delete mode 100644 .docker/build/install-steel-funs.sh diff --git a/.docker/build/build-hierarchic.sh b/.docker/build/build-hierarchic.sh index 0dd6d8193..4d54d6c1e 100755 --- a/.docker/build/build-hierarchic.sh +++ b/.docker/build/build-hierarchic.sh @@ -9,9 +9,7 @@ branchname=$2 build_home="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" . "$build_home"/build_funs.sh -. "$build_home"/install-krml-funs.sh -. "$build_home"/install-steel-funs.sh - +gi # Clear EVERPARSE_HOME, which was set by F*'s build unset EVERPARSE_HOME sed -i -E "s|^EVERPARSE_HOME=.*||" ~/.bashrc diff --git a/.docker/build/build-standalone.sh b/.docker/build/build-standalone.sh index d10578d7e..26d83ca29 100755 --- a/.docker/build/build-standalone.sh +++ b/.docker/build/build-standalone.sh @@ -10,18 +10,6 @@ branchname=$2 build_home="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" . "$build_home"/build_funs.sh -function fetch_and_make_karamel() { - # Karamel is already supposed to have been built and fetched before - # (e.g. by install-deps.sh) - true -} - -function fetch_and_make_steel() { - # steel is already supposed to have been built and fetched before - # (e.g. by install-deps.sh) - true -} - rootPath=$(pwd) result_file="result.txt" status_file="status.txt" diff --git a/.docker/build/build_funs.sh b/.docker/build/build_funs.sh index c44147e80..c23161d68 100644 --- a/.docker/build/build_funs.sh +++ b/.docker/build/build_funs.sh @@ -61,7 +61,6 @@ function rebuild_doc () { } function test_mitls_parsers () { - fetch_and_make_karamel && OTHERFLAGS='--admit_smt_queries true' make -j $threads quackyducky lowparse && export_home EVERPARSE "$(pwd)" && fetch_mitls && @@ -80,8 +79,6 @@ function build_and_test_quackyducky() { # Rebuild the EverParse documentation and push it to project-everest.github.io rebuild_doc && # Test EverParse proper - fetch_and_make_karamel && - fetch_and_make_steel && make -j $threads -k ci && # Build incrementality test pushd tests/sample && { diff --git a/.docker/build/install-deps.sh b/.docker/build/install-deps.sh index 8783178c8..6c01b84d6 100755 --- a/.docker/build/install-deps.sh +++ b/.docker/build/install-deps.sh @@ -19,28 +19,5 @@ git clone --branch $FSTAR_BRANCH https://github.com/FStarLang/FStar "$FSTAR_HOME opam install --deps-only "$FSTAR_HOME/fstar.opam" OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$FSTAR_HOME" -# Identify the Karamel branch -if [[ -z "$KRML_BRANCH" ]] ; then -KRML_BRANCH=$(jq -c -r '.RepoVersions.karamel_version' "$build_home"/config.json | sed 's!^origin/!!') -fi - -# Install Karamel and its dependencies -[[ -n "$KRML_HOME" ]] -git clone --branch $KRML_BRANCH https://github.com/FStarLang/karamel "$KRML_HOME" -pushd $KRML_HOME -.docker/build/install-other-deps.sh -popd -OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$KRML_HOME" - -# Identify the Steel branch -if [[ -z "$STEEL_BRANCH" ]] ; then -STEEL_BRANCH=$(jq -c -r '.RepoVersions.steel_version' "$build_home"/config.json | sed 's!^origin/!!') -fi - -# Install Steel and its dependencies -[[ -n "$STEEL_HOME" ]] -git clone --branch $STEEL_BRANCH https://github.com/FStarLang/steel "$STEEL_HOME" -OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$STEEL_HOME" - # Install other EverParse deps "$build_home"/install-other-deps.sh diff --git a/.docker/build/install-krml-funs.sh b/.docker/build/install-krml-funs.sh deleted file mode 100644 index dc6f0f9b1..000000000 --- a/.docker/build/install-krml-funs.sh +++ /dev/null @@ -1,31 +0,0 @@ -# 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 - fi - - cd karamel - git fetch origin - local ref=$(jq -c -r '.RepoVersions["karamel_version"]' "$rootPath/.docker/build/config.json" ) - echo Switching to KaRaMeL $ref - git reset --hard $ref - cd .. - export_home KRML "$(pwd)/karamel" -} - -function fetch_and_make_karamel() { - fetch_karamel - - # Default build target is minimal, unless specified otherwise - local target - if [[ $1 == "" ]]; then - target="minimal" - else - target="$1" - fi - - make -C karamel -j $threads $target || - (cd karamel && git clean -fdx && make -j $threads $target) - OTHERFLAGS='--admit_smt_queries true' make -C karamel/krmllib -j $threads - export PATH="$(pwd)/karamel:$PATH" -} diff --git a/.docker/build/install-other-deps.sh b/.docker/build/install-other-deps.sh index 70930962d..e2684e3e5 100755 --- a/.docker/build/install-other-deps.sh +++ b/.docker/build/install-other-deps.sh @@ -3,4 +3,29 @@ set -e set -x +build_home="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" + +# Identify the Karamel branch +if [[ -z "$KRML_BRANCH" ]] ; then +KRML_BRANCH=$(jq -c -r '.RepoVersions.karamel_version' "$build_home"/config.json | sed 's!^origin/!!') +fi + +# Install Karamel and its dependencies +[[ -n "$KRML_HOME" ]] +git clone --branch $KRML_BRANCH https://github.com/FStarLang/karamel "$KRML_HOME" +pushd $KRML_HOME +.docker/build/install-other-deps.sh +popd +OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$KRML_HOME" + +# Identify the Steel branch +if [[ -z "$STEEL_BRANCH" ]] ; then +STEEL_BRANCH=$(jq -c -r '.RepoVersions.steel_version' "$build_home"/config.json | sed 's!^origin/!!') +fi + +# Install Steel and its dependencies +[[ -n "$STEEL_HOME" ]] +git clone --branch $STEEL_BRANCH https://github.com/FStarLang/steel "$STEEL_HOME" +OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$STEEL_HOME" + opam install hex re ctypes sha diff --git a/.docker/build/install-steel-funs.sh b/.docker/build/install-steel-funs.sh deleted file mode 100644 index 6ec84d95b..000000000 --- a/.docker/build/install-steel-funs.sh +++ /dev/null @@ -1,19 +0,0 @@ -# By default, karamel master works against F* stable. Can also be overridden. -function fetch_steel() { - if [ ! -d steel ]; then - git clone https://github.com/FStarLang/steel steel - fi - - cd steel - git fetch origin - local ref=$(jq -c -r '.RepoVersions["steel_version"]' "$rootPath/.docker/build/config.json" ) - echo Switching to Steel $ref - git reset --hard $ref - cd .. - export_home STEEL "$(pwd)/steel" -} - -function fetch_and_make_steel() { - fetch_steel - OTHERFLAGS='--admit_smt_queries true' make -C steel -j $threads -} diff --git a/.docker/hierarchic.Dockerfile b/.docker/hierarchic.Dockerfile index d6e8f2cbe..f05915fb0 100644 --- a/.docker/hierarchic.Dockerfile +++ b/.docker/hierarchic.Dockerfile @@ -7,6 +7,8 @@ ADD --chown=opam:opam ./ $HOME/everparse/ WORKDIR $HOME/everparse # Dependencies (opam packages) +ENV KRML_HOME=$HOME/everparse/karamel +ENV STEEL_HOME=$HOME/everparse/steel RUN sudo apt-get update && eval $(opam env) && .docker/build/install-other-deps.sh # CI dependencies: sphinx (for the docs) @@ -21,5 +23,4 @@ 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-hierarchic.sh $CI_THREADS $CI_BRANCH WORKDIR $HOME -ENV KRML_HOME $HOME/everparse/karamel ENV EVERPARSE_HOME $HOME/everparse