Lazy.t and Memprof_limits

[gares]

In VSRocq PR 1046 we follow rocq-lsp and use Memprof_limits to provide a button to stop a looping Rocq. It seems to work reliably, in the sense that Rocq stops as expected.

We got carried away and we tried to use the same machinery to preempt running tasks whenever a high priority query arrives, like hovering, a bit like coq-lsp is doing to the best of my understanding. Of course we discovered various bugs about global state being corrupted, fixed in Rocq 9.2 thanks to PR 19177. We also found out that Lazy.t is problematic as well, Elpi had a global value of that type and if its Lazy.force was interrupted (the first time), the Memprof_limits interruption gets trapped in the lazy value. Fixed in PR 1021 and documented in Issue 9.

The next step was to grep Rocq sources for Lazy.t and I found some occurrences. I think that a lazy value that is created on the fly by a function and never stored globally is possibly fine, while global values are surely not.
Eg

plugins/funind/indfun_common.mli:val eq : EConstr.constr Lazy.t (* probably a problem *)
lib/dAst.mli:| Thunk : 'a Lazy.t -> ('a, [ `thunk ]) thunk (* OK I guess *)

There are some hints in kernel/ and one in evd/ that worry me. I think that "state sharing" is possibly a problem, i.e. if in a state I have an evar_map with a value lazy not forced, then I run a tactic to obtain a new state and while the tactic forces the lazy I interrupt it, then the broken lazy value is also present in the previous state.

In the end, @gadmm I think having Memprof_limits provide a safe replacement for Lazy is the best option, but that requires some time.

In the meanwhile I summon @ppedrot and @SkySkimmer to know what they think about these issues, how many of the Lazy are really problematic, how important it is to keep them Lazy, and so on... I can of course completely disable preemption in vsrocq (currently off by default, recommended only if Rocq >= 9.2), and use Memprof_limits when the use manually, out of despair, stops a looping Rocq. But preemption seemed to work reasonably ok in practice in rocq-lsp, maybe it is worth doing the last mile.

CC @rtetley

[SkySkimmer]

Global lazys like let eq = lazy (EConstr.of_constr (rocq_constant "core.eq.type")) (from funind, but funind isn't the only one using this pattern) are bugs even without preemption (if the lazy is forced then the user registers something else (possibly with state backtrack), the new register is ignored). They should be changed to regular thunks.
Doing that would take some work and it's not a commonly observed bug so nobody is working on it.

For other global lazys it would be case by case I guess.

BTW we could have a Lazy.force wrapper which locally disables memprof interruptions. Something like

let safe_force x =
  Memprof_coq.Masking.with_resource ~acquire:Lazy.force x ~scope:Fun.id ~release:ignore

If we keep some lazy whose lifetime spans across an interruption recovery (~a command) it should be forced that way (but IDK if we want to keep any such long lived lazys).

[SkySkimmer]

cc @gadmm

[gares]

Just got hit by:

$ git grep 'lazy' gramlib/
gramlib/grammar.ml:    let p = lazy (continue_parser_of_levels entry 0 elev) in
gramlib/grammar.ml:    let p = lazy (start_parser_of_levels entry 0 elev) in

[gares]

I think we should shadow Lazy.force over the entire code base, I did not think about disabling interruptions locally. I don't think we have lazy computations that take long anyway, or that can loop.

[gadmm]

We just discussed this with @SkySkimmer, it sounds to me that the strategy outlined so far makes sense:

• replace Lazy.force with some (interrupt_)safe_force that masks the interrupts during the computation
• try to remove long-running lazys

[gadmm]

Note that the "safe_force" should probably first check whether the value is already computed, and only mask if one needs to compute the value.

[SkySkimmer]

I did a grep for ^let.*lazy.*" to find global lazys and opened PRs to remove them.
This probably misses some global lazys which don't match the regex (eg going to newline between let and lazy, or having a function wrapping lazy)