diff options
Diffstat (limited to 'dev')
27 files changed, 242 insertions, 158 deletions
diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh index d2e150be9a..7796ae3b01 100755 --- a/dev/bench/gitlab.sh +++ b/dev/bench/gitlab.sh @@ -52,7 +52,7 @@ check_variable "CI_JOB_URL" : "${new_coq_opam_archive_git_branch:=master}" : "${old_coq_opam_archive_git_branch:=master}" : "${num_of_iterations:=1}" -: "${coq_opam_packages:=coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast}" +: "${coq_opam_packages:=coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast coq-perennial}" new_coq_commit=$(git rev-parse HEAD^2) old_coq_commit=$(git merge-base HEAD^1 $new_coq_commit) @@ -269,6 +269,9 @@ create_opam() { opam repo add -q --this-switch coq-extra-dev "$OPAM_COQ_DIR/extra-dev" opam repo add -q --this-switch coq-released "$OPAM_COQ_DIR/released" + # Pinning for packages that are not in a repository + opam pin add -ynq coq-perennial.dev git+https://github.com/mit-pdos/perennial#coq/tested + opam install -qy -j$number_of_processors $initial_opam_packages if [ ! -z "$BENCH_DEBUG" ]; then opam repo list; fi diff --git a/dev/bench/render_results b/dev/bench/render_results index 72affd70b2..bd4308837b 100755 --- a/dev/bench/render_results +++ b/dev/bench/render_results @@ -76,25 +76,13 @@ let run_and_read cmd = ;; let ( %> ) f g x = g (f x) -;; let run = run_and_read %> snd -;; module Float = struct let nan = Pervasives.nan end -module Tuple4 = struct - - let first (x,_,_,_) = x - let second (_,y,_,_) = y - let third (_,_,z,_) = z - let fourth (_,_,_,z) = z - -end -;; - module List = struct include List @@ -149,6 +137,151 @@ module String = struct end ;; +module Table : +sig + type header = string + type row = string list list + val print : header list -> row list -> string +end = +struct + type header = string + + type row = string list list + + let val_padding = 2 + (* Padding between data in the same row *) + let row_padding = 1 + (* Padding between rows *) + + let homogeneous b = if b then () else failwith "Heterogeneous data" + + let vert_split (ls : 'a list list) = + let split l = match l with + | [] -> failwith "vert_split" + | x :: l -> (x, l) + in + let ls = List.map split ls in + List.split ls + + let rec last = function + | [] -> assert false + | [x] -> [], x + | x :: l -> + let (l, y) = last l in + (x :: l, y) + + let justify n s = + let len = String.length s in + let () = assert (len <= n) in + let lft = (n - len) / 2 in + let rgt = n - lft - len in + String.make lft ' ' ^ s ^ String.make rgt ' ' + + let justify_row layout data = + let map n s = + let len = String.length s in + let () = assert (len <= n) in + (* Right align *) + let pad = n - len in + String.make pad ' ' ^ s + in + let data = List.map2 map layout data in + String.concat (String.make val_padding ' ') data + + let angle hkind vkind = match hkind, vkind with + | `Lft, `Top -> "┌" + | `Rgt, `Top -> "┐" + | `Mid, `Top -> "┬" + | `Lft, `Mid -> "├" + | `Rgt, `Mid -> "┤" + | `Mid, `Mid -> "┼" + | `Lft, `Bot -> "└" + | `Rgt, `Bot -> "┘" + | `Mid, `Bot -> "┴" + + let print_separator vkind col_size = + let rec dashes n = if n = 0 then "" else "─" ^ dashes (n - 1) in + let len = List.length col_size in + let pad = dashes row_padding in + let () = assert (0 < len) in + let map n = dashes n in + angle `Lft vkind ^ pad ^ + String.concat (pad ^ angle `Mid vkind ^ pad) (List.map map col_size) ^ + pad ^ angle `Rgt vkind + + let print_blank col_size = + let len = List.length col_size in + let () = assert (0 < len) in + let pad = String.make row_padding ' ' in + let map n = String.make n ' ' in + "│" ^ pad ^ String.concat (pad ^ "│" ^ pad) (List.map map col_size) ^ pad ^ "│" + + let print_row row = + let len = List.length row in + let () = assert (0 < len) in + let pad = String.make row_padding ' ' in + "│" ^ pad ^ String.concat (pad ^ "│" ^ pad) row ^ pad ^ "│" + + (* Invariant : all rows must have the same shape *) + + let print (headers : header list) (rows : row list) = + (* Sanitize input *) + let ncolums = List.length headers in + let shape = ref None in + let check row = + let () = homogeneous (List.length row = ncolums) in + let rshape : int list = List.map (fun data -> List.length data) row in + match !shape with + | None -> shape := Some rshape + | Some s -> homogeneous (rshape = s) + in + let () = List.iter check rows in + (* Compute layout *) + let rec layout n (rows : row list) = + if n = 0 then [] + else + let (col, rows) = vert_split rows in + let ans = layout (n - 1) rows in + let data = ref None in + let iter args = + let size = List.map String.length args in + match !data with + | None -> data := Some size + | Some s -> + data := Some (List.map2 (fun len1 len2 -> max len1 len2) s size) + in + let () = List.iter iter col in + let data = match !data with None -> [] | Some s -> s in + data :: ans + in + let layout = layout ncolums rows in + let map hd shape = + let data_size = match shape with + | [] -> 0 + | n :: shape -> List.fold_left (fun accu n -> accu + n + val_padding) n shape + in + max (String.length hd) data_size + in + let col_size = List.map2 map headers layout in + (* Justify the data *) + let headers = List.map2 justify col_size headers in + let rows = List.map (fun row -> List.map2 justify col_size (List.map2 justify_row layout row)) rows in + (* Print the table *) + let rows, last = last rows in + let sep = print_separator `Mid col_size in + let rows = List.concat @@ List.map (fun r -> [print_row r; sep]) rows in + let lines = + print_separator `Top col_size :: + print_row headers :: + print_blank col_size :: + rows @ + print_row last :: + print_separator `Bot col_size :: + [] + in + String.concat "\n" lines +end + (******************************************************************************) (* END Copied from batteries, to remove *) (******************************************************************************) @@ -203,10 +336,6 @@ let proportional_difference_of_integers new_value old_value = else float_of_int (new_value - old_value) /. float_of_int old_value *. 100.0 in -let count_number_of_digits_before_decimal_point = - log10 %> floor %> int_of_float %> succ %> max 1 -in - (* parse the *.time and *.perf files *) coq_opam_packages |> List.map @@ -259,138 +388,39 @@ coq_opam_packages (* Below we take the measurements and format them to stdout. *) +|> List.map begin fun (package_name, new_t, old_t, perc) -> + + let precision = 2 in + let prf f = Printf.sprintf "%.*f" precision f in + let pri n = Printf.sprintf "%d" n in + + [ + [ package_name ]; + [ prf new_t.user_time; prf old_t.user_time; prf perc.user_time ]; + [ pri new_t.num_cycles; pri old_t.num_cycles; prf perc.num_cycles ]; + [ pri new_t.num_instr; pri old_t.num_instr; prf perc.num_instr ]; + [ pri new_t.num_mem; pri old_t.num_mem; prf perc.num_mem ]; + [ pri new_t.num_faults; pri old_t.num_faults; prf perc.num_faults ]; + ] + + end + |> fun measurements -> - let precision = 2 in - - (* the labels that we will print *) - let package_name__label = "package_name" in - let new__label = "NEW" in - let old__label = "OLD" in - let proportional_difference__label = "PDIFF" in - - (* the lengths of labels that we will print *) - let new__label__length = String.length new__label in - let proportional_difference__label__length = String.length proportional_difference__label in - - (* widths of individual columns of the table *) - let package_name__width = - max (measurements |> List.map (Tuple4.first %> String.length) |> List.max) - (String.length package_name__label) in - - let llf proj = - let lls = count_number_of_digits_before_decimal_point (List.max proj) + 1 + precision in - max lls new__label__length in - - let lli proj = - let lls = count_number_of_digits_before_decimal_point (float_of_int (List.(max proj))) + 1 + precision in - max lls new__label__length in - - let new_timing_width = reduce_pkg_timings llf lli @@ List.map Tuple4.second measurements in - let old_timing_width = reduce_pkg_timings llf lli @@ List.map Tuple4.third measurements in - - let llp proj = - let lls = - count_number_of_digits_before_decimal_point List.(max List.(map abs_float proj)) + 2 + precision in - max lls proportional_difference__label__length in - - let perc_timing_width = reduce_pkg_timings llp llp @@ List.map Tuple4.fourth measurements in - - (* print the table *) - let rec make_dashes = function - | 0 -> "" - | count -> "─" ^ make_dashes (pred count) - in - - let vertical_separator left_glyph middle_glyph right_glyph = - sprintf "%s─%s─%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s\n" - left_glyph - (make_dashes package_name__width) - middle_glyph - (make_dashes new_timing_width.user_time) - (make_dashes old_timing_width.user_time) - (make_dashes perc_timing_width.user_time) - middle_glyph - (make_dashes new_timing_width.num_cycles) - (make_dashes old_timing_width.num_cycles) - (make_dashes perc_timing_width.num_cycles) - middle_glyph - (make_dashes new_timing_width.num_instr) - (make_dashes old_timing_width.num_instr) - (make_dashes perc_timing_width.num_instr) - middle_glyph - (make_dashes new_timing_width.num_mem) - (make_dashes old_timing_width.num_mem) - (make_dashes perc_timing_width.num_mem) - middle_glyph - (make_dashes new_timing_width.num_faults) - (make_dashes old_timing_width.num_faults) - (make_dashes perc_timing_width.num_faults) - right_glyph - in - - let center_string string width = - let string_length = String.length string in - let width = max width string_length in - let left_hfill = (width - string_length) / 2 in - let right_hfill = width - left_hfill - string_length in - String.make left_hfill ' ' ^ string ^ String.make right_hfill ' ' - in - printf "\n"; - print_string (vertical_separator "┌" "┬" "┐"); - "│" ^ String.make (1 + package_name__width + 1) ' ' ^ "│" - ^ center_string "user time [s]" (1 + new_timing_width.user_time + 1 + old_timing_width.user_time + 1 + perc_timing_width.user_time + 3) ^ "│" - ^ center_string "CPU cycles" (1 + new_timing_width.num_cycles + 1 + old_timing_width.num_cycles + 1 + perc_timing_width.num_cycles + 3) ^ "│" - ^ center_string "CPU instructions" (1 + new_timing_width.num_instr + 1 + old_timing_width.num_instr + 1 + perc_timing_width.num_instr + 3) ^ "│" - ^ center_string "max resident mem [KB]" (1 + new_timing_width.num_mem + 1 + old_timing_width.num_mem + 1 + perc_timing_width.num_mem + 3) ^ "│" - ^ center_string "mem faults" (1 + new_timing_width.num_faults + 1 + old_timing_width.num_faults + 1 + perc_timing_width.num_faults + 3) - ^ "│\n" |> print_string; - printf "│%*s │ %*s│ %*s│ %*s│ %*s│ %*s│\n" - (1 + package_name__width) "" - (new_timing_width.user_time + 1 + old_timing_width.user_time + 1 + perc_timing_width.user_time + 3) "" - (new_timing_width.num_cycles + 1 + old_timing_width.num_cycles + 1 + perc_timing_width.num_cycles + 3) "" - (new_timing_width.num_instr + 1 + old_timing_width.num_instr + 1 + perc_timing_width.num_instr + 3) "" - (new_timing_width.num_mem + 1 + old_timing_width.num_mem + 1 + perc_timing_width.num_mem + 3) "" - (new_timing_width.num_faults + 1 + old_timing_width.num_faults + 1 + perc_timing_width.num_faults + 3) ""; - printf "│ %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │\n" - package_name__width package_name__label - new_timing_width.user_time new__label - old_timing_width.user_time old__label - perc_timing_width.user_time proportional_difference__label - new_timing_width.num_cycles new__label - old_timing_width.num_cycles old__label - perc_timing_width.num_cycles proportional_difference__label - new_timing_width.num_instr new__label - old_timing_width.num_instr old__label - perc_timing_width.num_instr proportional_difference__label - new_timing_width.num_mem new__label - old_timing_width.num_mem old__label - perc_timing_width.num_mem proportional_difference__label - new_timing_width.num_faults new__label - old_timing_width.num_faults old__label - perc_timing_width.num_faults proportional_difference__label; - measurements |> List.iter - (fun (package_name, new_t, old_t, perc) -> - print_string (vertical_separator "├" "┼" "┤"); - printf "│ %*s │ %*.*f %*.*f %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │\n" - package_name__width package_name - new_timing_width.user_time precision new_t.user_time - old_timing_width.user_time precision old_t.user_time - perc_timing_width.user_time precision perc.user_time - new_timing_width.num_cycles new_t.num_cycles - old_timing_width.num_cycles old_t.num_cycles - perc_timing_width.num_cycles precision perc.num_cycles - new_timing_width.num_instr new_t.num_instr - old_timing_width.num_instr old_t.num_instr - perc_timing_width.num_instr precision perc.num_instr - new_timing_width.num_mem new_t.num_mem - old_timing_width.num_mem old_t.num_mem - perc_timing_width.num_mem precision perc.num_mem - new_timing_width.num_faults new_t.num_faults - old_timing_width.num_faults old_t.num_faults - perc_timing_width.num_faults precision perc.num_faults); - -print_string (vertical_separator "└" "┴" "┘"); + let headers = [ + ""; + "user time [s]"; + "CPU cycles"; + "CPU instructions"; + "max resident mem [KB]"; + "mem faults"; + ] in + + let descr = ["NEW"; "OLD"; "PDIFF"] in + let top = [ [ "package_name" ]; descr; descr; descr; descr; descr ] in + + printf "%s%!" (Table.print headers (top :: measurements)) +; (* ejgallego: disable this as it is very verbose and brings up little info in the log. *) if false then begin diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index fc8921e63d..6f6b3cd6d2 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -404,8 +404,7 @@ function build_prep { # ------------------------------------------------------------------------------ # Like build_prep, but gets the data from an entry in ci-basic-overlay.sh -# This assumes the following definitions exist in ci-basic-overlay.sh, -# or in a file in the user-overlays folder: +# This assumes the following definitions exist in ci-basic-overlay.sh # $1_CI_REF # $1_CI_ARCHIVEURL # $1_CI_GITURL @@ -432,7 +431,7 @@ function build_prep_overlay { } # ------------------------------------------------------------------------------ -# Load overlay version variables from ci-basic-overlay.sh and user-overlays/*.sh +# Load overlay version variables from ci-basic-overlay.sh # ------------------------------------------------------------------------------ function load_overlay_data { @@ -448,9 +447,6 @@ function load_overlay_data { export CI_PULL_REQUEST="" fi - for overlay in /build/user-overlays/*.sh; do - . "$overlay" - done . /build/ci-basic-overlay.sh } @@ -1441,7 +1437,6 @@ function make_coq { # Copy these files somewhere the plugin builds can find them logn copy-basic-overlays cp dev/ci/ci-basic-overlay.sh /build/ - logn copy-user-overlays cp -r dev/ci/user-overlays /build/ build_post fi diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh index 8570c34194..524555b69c 100755 --- a/dev/ci/ci-bedrock2.sh +++ b/dev/ci/ci-bedrock2.sh @@ -6,4 +6,5 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download bedrock2 +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make && make install ) diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index a0094b1006..72fc613c43 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download color +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/color" && make ) diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 9cb7a65ab5..6b09726606 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -5,6 +5,7 @@ ci_dir="$(dirname "$0")" git_download compcert +export COQCOPTS='-native-compiler no -w -undeclared-scope -w -omega-is-deprecated' ( cd "${CI_BUILD_DIR}/compcert" && \ ./configure -ignore-coq-version x86_32-linux && \ make && \ diff --git a/dev/ci/ci-coqprime.sh b/dev/ci/ci-coqprime.sh index a4fd296896..e12c36e6a7 100755 --- a/dev/ci/ci-coqprime.sh +++ b/dev/ci/ci-coqprime.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download coqprime +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/coqprime" && make && make install) diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh index ac3978dc8d..785ff4c2ad 100755 --- a/dev/ci/ci-corn.sh +++ b/dev/ci/ci-corn.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download corn +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/corn" && ./configure.sh && make && make install ) diff --git a/dev/ci/ci-engine_bench.sh b/dev/ci/ci-engine_bench.sh index fda7649f88..d976356dd4 100755 --- a/dev/ci/ci-engine_bench.sh +++ b/dev/ci/ci-engine_bench.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download engine_bench +export COQEXTRAFLAGS='-native-compiler ondemand' ( cd "${CI_BUILD_DIR}/engine_bench" && make coq && make coq-perf-Sanity ) diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index 30047e624b..3eda7161c1 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download equations +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci && make install ) diff --git a/dev/ci/ci-fiat_crypto.sh b/dev/ci/ci-fiat_crypto.sh index 3ecdb32a51..e8fa8c0be4 100755 --- a/dev/ci/ci-fiat_crypto.sh +++ b/dev/ci/ci-fiat_crypto.sh @@ -18,6 +18,7 @@ fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1" fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} pre-standalone-extracted printlite lite" fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all-except-compiled" +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ ulimit -s ${fiat_crypto_CI_STACKSIZE} && \ make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} ) diff --git a/dev/ci/ci-fiat_crypto_legacy.sh b/dev/ci/ci-fiat_crypto_legacy.sh index 6d0a803401..57cc121bb4 100755 --- a/dev/ci/ci-fiat_crypto_legacy.sh +++ b/dev/ci/ci-fiat_crypto_legacy.sh @@ -9,5 +9,6 @@ git_download fiat_crypto_legacy fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite-hardcoded old-pipeline-lite-hardcoded lite-display-hardcoded" fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem-hardcoded old-pipeline-nobigmem-hardcoded nonautogenerated-specific nonautogenerated-specific-display selected-specific selected-specific-display" +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \ make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/dev/ci/ci-fiat_crypto_ocaml.sh b/dev/ci/ci-fiat_crypto_ocaml.sh index 20d3deb14f..c63690d5c9 100755 --- a/dev/ci/ci-fiat_crypto_ocaml.sh +++ b/dev/ci/ci-fiat_crypto_ocaml.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1" +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/fiat_crypto" && make ${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml lite-generated-files ) diff --git a/dev/ci/ci-fiat_parsers.sh b/dev/ci/ci-fiat_parsers.sh index ac74ebf667..8409e25bdc 100755 --- a/dev/ci/ci-fiat_parsers.sh +++ b/dev/ci/ci-fiat_parsers.sh @@ -6,4 +6,5 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download fiat_parsers +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/fiat_parsers" && make parsers parsers-examples && make fiat-core ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 4b92c8cb4d..679bef3b5e 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -5,4 +5,6 @@ ci_dir="$(dirname "$0")" git_download hott -( cd "${CI_BUILD_DIR}/hott" && ./autogen.sh -skip-submodules && ./configure && make && make validate ) +( cd "${CI_BUILD_DIR}/hott" && ./autogen.sh -skip-submodules && ./configure \ + && sed -i.bak 's/\(HOQC =.*\)/\1 -native-compiler no/' Makefile \ + && make && make validate ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 27876d68de..813ea9b07a 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download metacoq +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make .merlin && make ci-local && make install ) diff --git a/dev/ci/ci-perennial.sh b/dev/ci/ci-perennial.sh index 306cbdf63c..43add8254a 100755 --- a/dev/ci/ci-perennial.sh +++ b/dev/ci/ci-perennial.sh @@ -6,4 +6,5 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download perennial +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/perennial" && git submodule update --init --recursive && make TIMED=false lite ) diff --git a/dev/ci/ci-rewriter.sh b/dev/ci/ci-rewriter.sh index 235482ffeb..ec7ac5bddc 100755 --- a/dev/ci/ci-rewriter.sh +++ b/dev/ci/ci-rewriter.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download rewriter +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/rewriter" && make && make install) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 704e278a4b..3d320617f2 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download unimath +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/unimath" && make BUILD_COQ=no ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 4a332406a2..a151cf0ba6 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -7,4 +7,5 @@ git_download vst export COMPCERT=bundled +sed -i.bak 's/\(COQC=.*\)/\1 -native-compiler no/' ${CI_BUILD_DIR}/vst/Makefile ( cd "${CI_BUILD_DIR}/vst" && make IGNORECOQVERSION=true ) diff --git a/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh b/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh new file mode 100644 index 0000000000..3bdbcf7d6e --- /dev/null +++ b/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "13312" ] || [ "$CI_BRANCH" = "attributes+bool_single" ]; then + + overlay unicoq https://github.com/ejgallego/unicoq attributes+bool_single + overlay elpi https://github.com/ejgallego/coq-elpi attributes+bool_single + +fi diff --git a/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh b/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh new file mode 100644 index 0000000000..95f0de2bd3 --- /dev/null +++ b/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "13386" ] || [ "$CI_BRANCH" = "master+fix9971-primproj-canonical-structure-on-evar-type" ]; then + + unicoq_CI_REF=master+adapting-coq-pr13386 + unicoq_CI_GITURL=https://github.com/herbelin/unicoq + + elpi_CI_REF=coq-master+adapting-coq-pr13386 + elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + +fi diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 37619833ac..79c2155823 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -312,6 +312,26 @@ Conversion machines risk: none without using -allow-sprop (off by default in 8.10.0), otherwise could be exploited by mistake + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: buffer overflow on large accumulators + introduced: 8.1 + impacted released versions: 8.1-8.12.1 + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: 8.13.0 + found by: Dolan, Roux, Melquiond + GH issue number: ocaml/ocaml#6385, #11170 + risk: medium, as it can happen for large irreducible applications + + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: buffer overflow on large records and closures + introduced: 8.1 + impacted released versions: 8.1-now + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: + found by: Dolan, Roux, Melquiond + GH issue number: ocaml/ocaml#6385, #11170 + risk: unlikely to be activated by chance, might happen for autogenerated code + Side-effects component: side-effects diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index 2e8a7455de..7701264ad1 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -9,10 +9,10 @@ CODE=0 -if [[ $(git log -n 1 --pretty='format:%s') == "Bot merge"* ]]; then - # The FIRST parent of bot merges is from the PR, the second is +if [[ $(git log -n 1 --pretty='format:%s') == "[CI merge]"* ]]; then + # The second parent of bot merges is from the PR, the first is # current master - head=$(git rev-parse HEAD~) + head=$(git rev-parse HEAD^2) else head=$(git rev-parse HEAD) fi diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index 21d6fbe9aa..bfc186c862 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -46,6 +46,7 @@ install_printer Top_printers.pp_idpred install_printer Top_printers.pp_cpred install_printer Top_printers.pp_transparent_state install_printer Top_printers.pp_stack_t +install_printer Top_printers.pp_estack_t install_printer Top_printers.pp_state_t install_printer Top_printers.ppmetas install_printer Top_printers.ppevm diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e4dd7ef52c..a9438c4aca 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -165,6 +165,7 @@ let pp_idpred s = pp (pr_idpred s) let pp_cpred s = pp (pr_cpred s) let pp_transparent_state s = pp (pr_transparent_state s) let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> pr_econstr) n) +let pp_estack_t n = pp (Reductionops.Stack.pr pr_econstr n) let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n) (* proof printers *) diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 712f66112c..50495dc0a4 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -108,6 +108,7 @@ val pp_cpred : Names.Cpred.t -> unit val pp_transparent_state : TransparentState.t -> unit val pp_stack_t : Constr.t Reductionops.Stack.t -> unit +val pp_estack_t : EConstr.t Reductionops.Stack.t -> unit val pp_state_t : Reductionops.state -> unit val ppmetas : Evd.Metaset.t -> unit |