Skip to content

Commit

Permalink
install-other-deps should install everything except F*
Browse files Browse the repository at this point in the history
  • Loading branch information
tahina-pro committed Aug 21, 2023
1 parent 6f6dc88 commit 9e02f60
Show file tree
Hide file tree
Showing 7 changed files with 24 additions and 91 deletions.
4 changes: 1 addition & 3 deletions .docker/build/build-hierarchic.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
12 changes: 0 additions & 12 deletions .docker/build/build-standalone.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
3 changes: 0 additions & 3 deletions .docker/build/build_funs.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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 &&
Expand All @@ -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 && {
Expand Down
23 changes: 0 additions & 23 deletions .docker/build/install-deps.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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
31 changes: 0 additions & 31 deletions .docker/build/install-krml-funs.sh

This file was deleted.

23 changes: 23 additions & 0 deletions .docker/build/install-other-deps.sh
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,27 @@
set -e
set -x

# 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
19 changes: 0 additions & 19 deletions .docker/build/install-steel-funs.sh

This file was deleted.

0 comments on commit 9e02f60

Please sign in to comment.