Skip to content

Commit

Permalink
Fix bench on old commits with no rocq-runtime
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Dec 4, 2024
1 parent 8236a61 commit dd1877e
Showing 1 changed file with 8 additions and 1 deletion.
9 changes: 8 additions & 1 deletion dev/bench/bench.sh
Original file line number Diff line number Diff line change
Expand Up @@ -346,6 +346,8 @@ git clone -q --depth 1 -b "$new_coq_opam_archive_git_branch" "$new_coq_opam_arch

initial_opam_packages="num ocamlfind dune"

installable_rocq_runtime=rocq-runtime

# Create an opam root and install Coq
# $1 = root_name {ex: NEW / OLD}
# $2 = compiler name
Expand Down Expand Up @@ -427,6 +429,11 @@ create_opam() {
if [ ! -z "$coq_native" ]; then opam install coq-native; fi

for package in rocq-runtime coq-core coq-stdlib coqide-server coq; do
if [ $package = rocq-runtime ] && ! [ -e rocq-runtime.opam ]; then
echo "No rocq-runtime in $RUNNER"
installable_rocq_runtime=
continue
fi
export COQ_OPAM_PACKAGE=$package
export COQ_ITERATION=1

Expand Down Expand Up @@ -469,7 +476,7 @@ old_coq_commit_long="$COQ_HASH_LONG"

# Packages which appear in the rendered table
# Deliberately don't include the "coqide-server" and "coq" packages
installable_coq_opam_packages="rocq-runtime coq-core coq-stdlib"
installable_coq_opam_packages="$installable_rocq_runtime coq-core coq-stdlib"

echo "DEBUG: $render_results $log_dir $num_of_iterations 0 user_time_pdiff $installable_coq_opam_packages"
rendered_results="$($render_results "$log_dir" $num_of_iterations 0 user_time_pdiff $installable_coq_opam_packages)"
Expand Down

0 comments on commit dd1877e

Please sign in to comment.