Stream: Coq devs & plugin devs

Topic: what is ocamlopt status 2?

Jason Gross (Jul 17 2023 at 00:09):

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?)

Other than 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?)

Pierre Roux (Jul 17 2023 at 06:41):

Have you tried increasing stack size as suggested / reducing size of the array?

Gaëtan Gilbert (Jul 17 2023 at 08:42):

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 *)

Gaëtan Gilbert (Jul 17 2023 at 08:44):

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 *)

Guillaume Melquiond (Jul 17 2023 at 09:11):

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.

Jason Gross (Jul 17 2023 at 16:06):

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.

Gaëtan Gilbert (Jul 17 2023 at 16:28):

I think you have to modify coqnative / coqc

Rodolphe Lepigre (Jul 17 2023 at 16:50):

You might be able to control this with an environment variable (maybe OCAMLOPTFLAGS?).

Jason Gross (Jul 17 2023 at 16:51):

I've added this request to https://github.com/coq/coq/issues/17864

Jason Gross (Jul 17 2023 at 17:00):

ulimit -s unlimited; (export OCAMLOPTFLAGS="-linscan"; make TIMED=1 -kj4 VERBOSE=1) seems to work!

Jason Gross (Jul 17 2023 at 18:29):

In fact, 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