What might cause
COQNATIVE theories/max_all_logits.vo ocamlopt.opt got signal and exited Error: Native compiler exited with status 2 (in case of stack overflow, increasing stack size (typically with "ulimit -s") often helps) Command exited with non-zero status 1 theories/max_all_logits.vo.native (real: 33.81, user: 32.70, sys: 1.09, mem: 2702144 ko)
(is this a memkill?)
Imports, the file only contains two definitions:
Time Definition all_tokens_logits_concrete : PArray.concrete_tensor _ _ := Eval native_compute in PArray.concretize (logits all_tokens). Definition all_tokens_logits : tensor _ _ := PArray.abstract all_tokens_logits_concrete.
so I'm a bit confused why ocamlopt is sad... (It is true that
all_tokens_logits_concrete has type
array (array (array float)) of shape
(4096, 2, 64), so there are 524,288 floats; is that too many?)
Have you tried increasing stack size as suggested / reducing size of the array?
seems easily reproduced with
Require Import PArray Uint63 PrimFloat. Definition arrays := Eval cbv in make 128 (make 128 0%float). (* native compile error when doing the ahead of time compile *)
the generated code looks like
open Nativevalues open Nativecode open Nativelib open Nativeconv let symbols_tbl = let Refl = Nativevalues.t_eq in (str_decode "8495a6be0000000100000000000000000000000080") (* Time spent generating this code: 0.00132s *) let const_NTmp_foo_arrays : Nativevalues.t = let Refl = Nativevalues.t_eq in parray_of_array (Obj.magic (parray_of_array (Obj.magic (mk_float (Float64.of_float (0x0p+0)), mk_float (Float64.of_float (0x0p+0)), mk_float (Float64.of_float (0x0p+0)), mk_float (Float64.of_float (0x0p+0)), (* 8k more similar lines occasionally starting another subarray *)
It is well-known that ocamlopt cannot compile very large OCaml functions. You might try to pass the option
-linscan (naive register allocator) and see if it works better. But even so, while this option makes the time complexity linear, it might still be using way too much stack in practice.
How do I tell COQNATIVE to pass
-linscan? I see
$(HIDE)$(call TIMER,$(1).vo.native) $(COQNATIVE) $(COQLIBS) $(1).vo
in the makefile, which doesn't seem to allow more options.
I think you have to modify coqnative / coqc
You might be able to control this with an environment variable (maybe
I've added this request to https://github.com/coq/coq/issues/17864
ulimit -s unlimited; (export OCAMLOPTFLAGS="-linscan"; make TIMED=1 -kj4 VERBOSE=1) seems to work!
OCAMLOPTFLAGS="-linscan" is not even required (though it does speed things up on the test example from 45s to 39s),
ulimit -s unlimited is enough
Last updated: Dec 05 2023 at 12:01 UTC