coq-elpi Fix roots in solution2evd

It may happen that coq-elpi aliases something in the input evar_map and then drops the alias because it does not appear in the solution returned by coq-elpi. However, this alias might be referenced in the evar_map, so it should not be dropped. This PR fixes the issue by adding the evars from the input evar_map to the roots of the computation of reachable evars. This relies on some API from coq that does not exist yet.

Mar 19 '24 10:03 Tragicus

@Tragicus could you link to a branch of Coq which exposes the primitive you needed?

Mar 20 '24 08:03 CohenCyril

Yes, here it is (I only need the contents of engine/evd.ml): https://github.com/Tragicus/coq/tree/utils For reference, I opened a PR for this branch: https://github.com/coq/coq/pull/18820

Mar 20 '24 09:03 Tragicus

I think the old code was actually implementing Evd.undefined_evars, about the other one I don't know.

Mar 20 '24 10:03 gares

@Tragicus can you tell me if this code does what you wanted?

Then we definitely need to do some benchmarking

Jun 28 '24 09:06 gares

It was long ago so I might be mistaken, but I am pretty sure this solved our issue back then. I can do the benchmarking tomorrow.

Jun 28 '24 15:06 Tragicus

I can compile neither master nor coq-master neither on coq's master nor v8.19. Can you tell me which branches I should take?

Jun 30 '24 10:06 Tragicus

Maybe you need to rebade this pr, but currently master works with 8.19, 8.20rc1 and master, both with opam and Nix.

Jun 30 '24 14:06 gares