Stream: Coq devs & plugin devs

Topic: Dune caching & Coq non-reproducible builds


view this post on Zulip 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?).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jan 13 2023 at 12:05):

I will adapt vodump for modern Coq versions.

view this post on Zulip Paolo Giarrusso (Jan 13 2023 at 12:07):

Thanks!

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Jan 13 2023 at 12:08):

Yes, although easy might be a bit of an exaggeration.

view this post on Zulip 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

view this post on Zulip Guillaume Melquiond (Jan 13 2023 at 12:51):

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?

view this post on Zulip Paolo Giarrusso (Jan 13 2023 at 17:20):

could help beyond determinism problems in plugins — colleagues have implemented some tooling by scripting votour

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jan 15 2023 at 20:10):

unless you have two copies in the AST and only one is unreachable?

view this post on Zulip Gaëtan Gilbert (Jan 15 2023 at 20:11):

then it doesn't get removed from the hashcons table

view this post on Zulip Paolo Giarrusso (Jan 15 2023 at 20:12):

I mean _deep_ copies not shallow copies

view this post on Zulip Gaëtan Gilbert (Jan 15 2023 at 20:13):

then when we hashcons we take one as canonical and replace the other with it

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Jan 15 2023 at 20:26):

but I should probably stop here, sorry. On to uploading.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jan 15 2023 at 21:05):

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

view this post on Zulip Paolo Giarrusso (Jan 15 2023 at 21:07):

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


Last updated: Jul 23 2024 at 17:01 UTC