Non deterministic coqc output

[SkySkimmer]

Based on https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Dune.20caching.20.26.20Coq.20non-reproducible.20builds.

---

Unless I made some very weird mistake, a (very mildly patched) Coqc 8.16.0 is (again?) non-reproducible, which affects our dune-based CI.

Here are two ARM vo files from the same source file — everything is public
https://gist.github.com/Blaisorblade/cd953398a241c17002b1d903806c2bea

I tried https://github.com/ppedrot/vodump from #11229, but it doesn't work as-is (fails on the magic number, might be easy to update?).

Most of the credits go to dune's DUNE_CACHE_CHECK_PROBABILITY, and to the recent fixes that made it usable.

We also have evidence that this happens on our x86 CI — possibly with lower frequency. I should note this file uses

Module IM := FMapAVL.Make OT_bs.

but other files don't use modules so blatantly.

---

I wiped my dune cache and I'm collecting more data via repeated rebuilds — I've already hit the same vos, and more.

If anybody wants to try, at recent dune versions make it easy (I'm using 3.6.1):

(for i in `seq 1 10`; do rm -rf _build/; time DUNE_CACHE_CHECK_PROBABILITY=1 dune b; done) 2>&1| tee -a output

---

Combining vodump, votour and Coq sources let me confirm that this is about string hash-consing again, like last time; I'll be uploading analysis results.

The example in the gist involves modules, but I'll upload a new one without where it seems that opaque constant into_sep_at = λ (thread_info : biIndex) ... : ∀ (thread_info : biIndex) with section-bound thread_info, stores thread_info twice, one for the type and one in the cooking_info for the opaque body.

... while other times into_sep_at stores thread_info only once, as expected, which fits #11229 (comment).

---

Here it is: https://gist.github.com/Blaisorblade/a7274f0eb15a13afbaa083b5b3673697 for the example that does not involve modules. It should be easy to confirm the same string appears once vs twice, and the node paths hint to the involved types and code:

Depth 17 Pos 0.1.2.0.0.1.0.2.0.1.0.1.0.0.1.1.0 Context library/compiled/module_body/module_sign/list/label*sfb/struct_field_body/constant_body/constant_def/opaque/list/cooking_info/abstr_info/list/named_declaration/constr/array
Depth 10 Pos 0.1.2.0.0.1.0.3.0.0 Context library/compiled/module_body/module_sign/list/label*sfb/struct_field_body/constant_body/constr/binder_annot

but the original example (avl.vo) involves different paths wrapping the different strings:

Depth 30 Pos 0.1.2.0.0.1.0.2.0.1.0.1.0.2.0.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.0.1.0.2.0.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.0.1.0.0.0.8.1.0.1.1.1.1.1.0.0.0 
Context 
library/compiled/module_body/module_sign/list/label*sfb/struct_field_body/module_body/module_sign/
list/label*sfb/struct_field_body/module_body/module_sign/list/label*sfb/struct_field_body/module_body/
module_sign/list/label*sfb/struct_field_body/mutual_inductive_body/array/one_inductive_body/array/*/
list/rel_declaration/binder_annot 

I haven't cleaned up the analysis of avl.vo, but I can do it if it helps.

into_sep_at with Set Printing All: https://gist.githubusercontent.com/Blaisorblade/a7274f0eb15a13afbaa083b5b3673697/raw/f607062b1dab313da5118645f366bf0263409606/into_sep_at_term.v

Originally posted by @Blaisorblade in #11229 (comment)

Consortium support on behalf of Bedrock Systems

[SkySkimmer]

@Blaisorblade what's the distribution of results? I mean is one hash common and the other rare, or is it more 50/50?

[silene]

I have no idea whether Coq does the following (hopefully not), but just in case, keep in mind that marshaling is a bit strange when it comes to lazy values (even forced ones!). The behavior depends on whether the garbage collector got the chance to clean the proxies or not.

let () =
  let l1 = lazy ("foo" ^ "bar") in
  let l2 = lazy (Printf.printf ""; l1) in
  ignore (Lazy.force l1);
  ignore (Lazy.force l2);
  let v1 = Marshal.to_string l2 [] in
  Gc.major ();
  let v2 = Marshal.to_string l2 [] in
  let v3 = Marshal.to_string l2 [] in
  Printf.printf "%b %b\n%!" (v1 = v2) (v2 = v3)
(* output: false true *)

[SkySkimmer]

I don't think we marshal any lazies, and even if we do I don't think the difference would look like what we see in the analysis.
IIUC with the lazy thing we would sometimes a difference in indirections ie some values would be inconsistently wrapped, but here we see a string getting inconsistently duplicated or inconsistently hashconsed.

[SkySkimmer]

@Blaisorblade I don't know how to make progress on this

[ejgallego]

Can you folks reproduce when compiling with the simple compiler (#16190) ?

[Blaisorblade]

@SkySkimmer First of all, did you manage to reproduce this, or run into trouble?