Skip to content

Commit

Permalink
Merge pull request #2889 from FStarLang/taramana_no_steel
Browse files Browse the repository at this point in the history
Remove Steel from the F* code base
  • Loading branch information
mtzguido authored May 3, 2023
2 parents 271ac37 + 4ab5019 commit e7c930d
Show file tree
Hide file tree
Showing 1,726 changed files with 30,291 additions and 222,600 deletions.
1 change: 0 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,6 @@ tests/*/*.ml
tests/incl/*.neg/error.log

_build/
/ulib/ml/_taclib_build/
/ulib/fs/obj
/ulib/fs/bin

Expand Down
18 changes: 10 additions & 8 deletions bin/run_benchmark.sh
Original file line number Diff line number Diff line change
Expand Up @@ -146,16 +146,16 @@ function clean_slate () {
# build fstar compiler bootstrap
T0=`date +'%Y%m%d_%H%M%S'`
echo "Starting fstar compiler bootstrap ${T0}"
make -j${JLEVEL} -C src ocaml-fstar-ocaml 2>&1 | tee ${BENCH_OUTDIR}/build_fstar.log
make -j${JLEVEL} dune-full-bootstrap 2>&1 | tee ${BENCH_OUTDIR}/build_fstar.log
T1=`date +'%Y%m%d_%H%M%S'`
echo "Finished fstar compiler boostrap ${T1} (started at ${T0})"

# verify ulib and install
# build library
T0=`date +'%Y%m%d_%H%M%S'`
echo "Starting fstarlib build ${T0}"
make -j${JLEVEL} -C src .fstarlib 2>&1 | tee ${BENCH_OUTDIR}/build_fstarlib.log
echo "Starting library build ${T0}"
make -j${JLEVEL} 2>&1 | tee ${BENCH_OUTDIR}/build_fstarlib.log
T1=`date +'%Y%m%d_%H%M%S'`
echo "Finished fstar compiler boostrap ${T1} (started at ${T0})"
echo "Finished library build ${T1} (started at ${T0})"

ls -ltr ulib >> ${BENCH_OUTDIR}/build_fstarlib.log
}
Expand All @@ -171,7 +171,8 @@ function bench_dir () {
# Remove old .bench files
find "${BENCH_DIR}" -name '*.bench' -delete

${BENCH_WRAP} make -j${JLEVEL} -C "${BENCH_DIR}" "${RULE}" BENCHMARK_CMD=orun OTHERFLAGS="${BENCH_OTHERFLAGS}" 2>&1 | tee ${BENCH_OUTDIR}/${NAME}.log
# We explicitly add -f since we have previously built F* and its library, we are re-checking here.
${BENCH_WRAP} make -j${JLEVEL} -C "${BENCH_DIR}" "${RULE}" BENCHMARK_CMD=orun OTHERFLAGS="${BENCH_OTHERFLAGS} -f" 2>&1 | tee ${BENCH_OUTDIR}/${NAME}.log
fi

cat_benches_into "${BENCH_DIR}" "${BENCH_OUTDIR}/${NAME}.bench"
Expand Down Expand Up @@ -380,9 +381,10 @@ check_for jq "Try to install it via your package manager, or see https://stedola

check_for orun "\
To install a local pinned copy of orun do the following:
$ git clone https://github.com/ocaml-bench/sandmark.git sandmark
$ git clone https://github.com/ocaml-bench/orun.git sandmark
$ cd sandmark/orun
$ opam install ."
$ opam install .
You may need to install libdw-dev via your package manager before."

# Second pass for options, only handles --custom which needs to run after the others
OPTIONS=
Expand Down
18 changes: 9 additions & 9 deletions doc/book/code/AdHocEffectPolymorphism.fst.hints

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

28 changes: 14 additions & 14 deletions doc/book/code/Alex.fst.hints

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

14 changes: 7 additions & 7 deletions doc/book/code/AlexOpaque.fst.hints

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

Loading

0 comments on commit e7c930d

Please sign in to comment.