Skip to content

Commit 8462874

Browse files
committed
1 parent b3e498e commit 8462874

File tree

2 files changed

+7
-2
lines changed

2 files changed

+7
-2
lines changed

dev/bench/bench.sh

+6-2
Original file line numberDiff line numberDiff line change
@@ -35,8 +35,8 @@ check_variable () {
3535

3636
: "${coq_pr_number:=}"
3737
: "${coq_pr_comment_id:=}"
38-
: "${new_ocaml_version:=4.14.1}"
39-
: "${old_ocaml_version:=4.14.1}"
38+
: "${new_ocaml_version:=5.2.0}"
39+
: "${old_ocaml_version:=5.2.0}"
4040
: "${new_ocaml_flambda:=0}"
4141
: "${old_ocaml_flambda:=0}"
4242
: "${new_coq_repository:=${CI_REPOSITORY_URL:-.}}"
@@ -386,6 +386,10 @@ create_opam() {
386386
opam var --global jobs=$number_of_processors >/dev/null
387387
if [ ! -z "$BENCH_DEBUG" ]; then opam config list; fi
388388

389+
if [ $RUNNER = NEW ]; then
390+
opam pin add -y ocaml-base-compiler https://github.com/gasche/ocaml.git#gc-rampup-control-5.2
391+
fi
392+
389393
opam repo add -q --this-switch coq-core-dev "$OPAM_COQ_DIR/core-dev" # For rocq-stdlib
390394
opam repo add -q --this-switch coq-extra-dev "$OPAM_COQ_DIR/extra-dev"
391395
opam repo add -q --this-switch coq-released "$OPAM_COQ_DIR/released"

vernac/library.ml

+1
Original file line numberDiff line numberDiff line change
@@ -262,6 +262,7 @@ module Intern = struct
262262
end
263263

264264
let intern_from_file file =
265+
fst @@ Gc.ramp_up @@ fun () ->
265266
let ch = raw_intern_library file in
266267
let lsd, digest_lsd = ObjFile.marshal_in_segment ch ~segment:summary_seg in
267268
let lmd, digest_lmd = ObjFile.marshal_in_segment ch ~segment:library_seg in

0 commit comments

Comments
 (0)