Stream: Coq devs & plugin devs

Topic: coqchk OOM

Jason Gross (Mar 31 2022 at 15:21):

Fiat Crypto builds fine, but coqchk OOMs https://github.com/mit-plv/fiat-crypto/issues/1181 (validate-vo (real: 3861.28, user: 3163.89, sys: 54.80, mem: 6725700 ko)). Is there a good way to debug this? Can I figure out which constant it was checking when it OOMed?

Gaëtan Gilbert (Mar 31 2022 at 15:31):

the one it says "checking cst:..." (the message is printed before the checking, not after)

Jason Gross (Mar 31 2022 at 17:43):

Hmm, the proof is fully automated (Proof using Type. Time constructor; make_computed_op. Defined.), and coqc peaks at 2,038,196 ko mem, while coqchk is killed at 6,725,700 ko mem...

Gaëtan Gilbert (Mar 31 2022 at 17:45):

what coq version? if <8.15 it doesn't use vm_compute in coqchk

Jason Gross (Mar 31 2022 at 17:46):

Current master (035dcfc0b7)

Jason Gross (Mar 31 2022 at 17:51):

The tactic is

Ltac make_computed_op :=
  eapply Build_computed_op;
  lazymatch goal with
  | |- _ = ErrorT.Success _ => vm_compute; reflexivity
  | _ => idtac
  end;
  vm_compute; reflexivity.

Gaëtan Gilbert (Mar 31 2022 at 17:56):

no wait 8.15 doesn't respect vm_compute, it respects Kernel Term Sharing

Gaëtan Gilbert (Mar 31 2022 at 17:58):

so it's probably just the disabled vm_compute

Jason Gross (Mar 31 2022 at 18:37):

I see messages like

checking cst:Crypto.Spec.Curve25519.prime_p
Warning: Native compiler is disabled, falling back to VM conversion test.
         [native-compiler-disabled,native-compiler]

Is this misleading? Is there a way to enable vm_compute in coqchk, or otherwise work around this issue?

Gaëtan Gilbert (Mar 31 2022 at 18:49):

there's no way to enable it currently

Ali Caglayan (Mar 31 2022 at 19:01):

Can we enable it ml side? Or is even that impossible?

Gaëtan Gilbert (Mar 31 2022 at 19:02):

should be pretty easy, just add it to checkFlags.ml
maybe conditionally on a command line flag like -allow-vm so that people who want to check without it can

Ali Caglayan (Mar 31 2022 at 19:07):

Ok I'll submit a patch

Ali Caglayan (Mar 31 2022 at 19:08):

Actually do we want to enable it by default?

Jason Gross (Mar 31 2022 at 19:23):

I think we don't want to enable it by default, the default run of coqchk should be minimal, I think

Ali Caglayan (Mar 31 2022 at 20:29):

Done: https://github.com/coq/coq/pull/15886

Ali Caglayan (Mar 31 2022 at 20:29):

It is disabled by default for now

Ali Caglayan (Mar 31 2022 at 20:29):

I can't remember does the validate job for coq_makefile pass all the flags to coqchk?

Ali Caglayan (Mar 31 2022 at 20:30):

I used -bytecode-compiler in order to be inline with whatever coqc/coqtop was using

Gaëtan Gilbert (Mar 31 2022 at 20:32):

Ali Caglayan said:

I can't remember does the validate job for coq_makefile pass all the flags to coqchk?

most coqc flags aren't accepted by coqchk so no

Ali Caglayan (Mar 31 2022 at 20:36):

OK but it is still probably good to use the same option names right?

Ali Caglayan (Mar 31 2022 at 20:37):

Would it be possible to modify coq_makefile so that typing flags like -indices-matter etc. are inherited from _CoqProject?

Ali Caglayan (Mar 31 2022 at 20:45):

I see that coq_makefile has COQCHKEXTRAFLAGS for setting extra flags for coqchk

Last updated: Sep 15 2024 at 13:02 UTC