Is there anything that can be done about how slow coqchk is when there are lots of instantiated module functors floating around? I have an commit that added about 4s of coqc time and instantiated 3 functors, adding over 1.5h of coqchk time (https://github.com/mit-plv/fiat-crypto/runs/6742237434?check_suite_focus=true / https://github.com/mit-plv/fiat-crypto/pull/1274/files / https://github.com/mit-plv/fiat-crypto/commit/f3ef38805173110dd150c6de71f6fdaffd042c6d over https://github.com/mit-plv/fiat-crypto/runs/6742072165?check_suite_focus=true).
I suspect the issue is that the functor has a bunch of conversion problems buried in opaque proofs that become much harder when the functor arguments are instantiated. The only thing I can think of to do is replicate the functor arguments as a record and move all the proofs and definitions outside the functor (using functors because FMapInterface), but it would be nice if coqchk could handle this automatically.
The handling of functors in coqchk is very wobbly. I'm not sure if there is a universal solution to your kind of performance issues.
Correct me if I am wrong, but don't most issues arising from functors come up because their specification is just so general? Perhaps it would be possible to restrict to a sane subset of functors for which we can fix performance/soundness issues. I know there have been informal discussions about reducing the complexity of the functor mechanism, but if Jason's use case is not pathological, it should definitely be a part of the sane fragment. Of course, I could also be wrong and it could be precisely this fragment that is problematic.
coqchk trying to be safe is likely to be the issue here
i.e. it expands fully applied functors to check that the result is still well-typed
when coqchk typechecks the result of
F A instead of
A separately, does it regard members of
A as at least
otherwise, “pathological functors" will include any functor F that relies on its argument being abstract for performance
it does not
F A get the same unfolding oracle as fields of
that is fine, the question is on fields of
A itself _when typechecking the applied functor_
A is already typechecked
that is not relevant, so let me spell out what I mean
Module Type AT.
Parameter n : nat.
Definition ignore (x:nat) := 0.
Definition foo : ignore X.n = ignore 100 := eq_refl.
Definition n := 101.
Module FM := F M.
FM.foo coqchk sees
eq_refl : ignore M.n = ignore 100 with
so it will compare
101 == 100
100 == 99
99 == 98 etc until failing and falling back to unfolding
yep, so could
Opaque (even if
Defined) when typechecking
also wondering if you can even write
Opaque M.n by hand here...
even if, of course, that's useless for coqc
if you move the definition of M before F you can put Opaque M.n and I think coqchk would respect it
hm, this is also accepted, no idea with what semantics:
I think that won't work for coqchk
I think you can make definitions where treating functor arguments as Opaque in coqchk is the wrong thing but maybe it would work more often than the current system
I agree that
Opaque gives less opacity than the source program, but what are those examples, and are those rare enough to be pathological? Maybe showing such examples would help the discussion?
in any case, I wonder:
Opaque help @Jason Gross 's problem? Or would one need to add stronger sealing mechanisms?
coqchk gain better heuristics? writing
Opaque M.n is more work than
Opaque X.n, which is more work than
coqchk generating that.
Semi-OT: does coqchk also erase module sealing via opaque ascriptions (which is otherwise the strongest sealing available)?
Opaque M.n isn't strong enough here, because it's getting unfolded in a Constant vs Constructor conversion Opaque is ignored
and treating M.n as Qed is just incorrect, because you can write stuff like
Definition n_def : M.n = 100 := eq_refl in F (moving the definition of M before F)
I wonder if some intermediate
Opaquer command could help
otherwise I'm wondering if
coqchk -trust-functor-soundness that doesn't expand functors could be useful
what would Opaquer even do?
it's getting unfolded in a Constant vs Constructor conversion — Opaque is ignored
could you implement delayed unfolding even in this scenario (and have a different command just for bwd compat), or is this too hard to implement, and maybe this is too naive a Q.
Last updated: Feb 27 2024 at 23:01 UTC