Paolo Giarrusso (Jan 13 2023 at 11:38): Paolo Giarrusso (Jan 13 2023 at 11:38):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 https://github.com/coq/coq/issues/11229, but it doesn't work as-is (fails on the magic number, might be easy to update?).
Paolo Giarrusso (Jan 13 2023 at 11:39):Most of the credits go to dune's DUNE_CACHE_CHECK_PROBABILITY, and to the recent fixes that made it usable.
Paolo Giarrusso (Jan 13 2023 at 11:59):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.
Pierre-Marie Pédrot (Jan 13 2023 at 12:05):I will adapt vodump for modern Coq versions.
Paolo Giarrusso (Jan 13 2023 at 12:07):Thanks!
Paolo Giarrusso (Jan 13 2023 at 12:07):Just to confirms: it dumps the vo into text form so it's easy to diff and tell what changed, right?
Pierre-Marie Pédrot (Jan 13 2023 at 12:08):Yes, although easy might be a bit of an exaggeration.
Paolo Giarrusso (Jan 13 2023 at 12:11):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
Pierre-Marie Pédrot said:
I will adapt vodump for modern Coq versions.
We already have votour in the main repository. It seems to me that vodump would be just as useful. Was it considered?
Paolo Giarrusso (Jan 13 2023 at 17:20):could help beyond determinism problems in plugins — colleagues have implemented some tooling by scripting votour
Pierre-Marie Pédrot (Jan 14 2023 at 23:18):Regardless of the decision to ship vodump with Coq, I've pushed a patch that should make it compatible with recent Coq versions.
Paolo Giarrusso (Jan 15 2023 at 20:03):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.
Paolo Giarrusso (Jan 15 2023 at 20:04):... while other times into_sep_at stores thread_info only once, as expected, which fits https://github.com/coq/coq/issues/11229#issuecomment-563252139.
Gaëtan Gilbert (Jan 15 2023 at 20:09):I never understood that theory
if something is removed from the hashcons table then it's unreachable, so removing it shouldn't break sharing with anything
Paolo Giarrusso (Jan 15 2023 at 20:10):unless you have two copies in the AST and only one is unreachable?
Gaëtan Gilbert (Jan 15 2023 at 20:11):then it doesn't get removed from the hashcons table
Paolo Giarrusso (Jan 15 2023 at 20:12):I mean _deep_ copies not shallow copies
Gaëtan Gilbert (Jan 15 2023 at 20:13):then when we hashcons we take one as canonical and replace the other with it
Paolo Giarrusso (Jan 15 2023 at 20:23):sure, but it depends on the lifetime of the copies — can you hash-cons, output and GC one copy _before_ you hash-cons the other?
Paolo Giarrusso (Jan 15 2023 at 20:26):but I should probably stop here, sorry. On to uploading.
Paolo Giarrusso (Jan 15 2023 at 20:58):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.
Last updated: Oct 13 2024 at 01:02 UTC