fix sigma pruning when calling ltac, reachability is not correct #581
Conversation
|
@Tragicus this new test seems more correct. Can you try it in your example? (After all I can't completely remove the pruning as we were doing this afternoon). |
| debug Pp.(fun () -> str "Goals: " ++ prlist_with_sep spc Evar.print declared_goals); | ||
| debug Pp.(fun () -> str "Shelved Goals: " ++ prlist_with_sep spc Evar.print shelved_goals); | ||
| Evd.fold_undefined (fun k _ sigma -> | ||
| if Evar.Set.mem k all_goals || Evd.mem sigma0 k then sigma | ||
| if Evar.Set.mem k reachable_undefined_evars then sigma | ||
| else Evd.remove sigma k |
There was a problem hiding this comment.
Sorry for hijacking this PR, but you definitely shouldn't reimplement your own pruning in a plugin. As a matter of fact, I wonder why Evd.remove is not marked as deprecated in the Coq API as you can easily wreak havoc (and definitely will if people use additional Store primitives in an evarmap).
We should instead provide a pruning function directly with Evd and ask in the API when creating user-defined evar data to provide functions explaining how the new data creates pointers to other blocks. It is more than time to realize that an evarmap is a proper heap...
There was a problem hiding this comment.
I'm all for a heap that comes with a garbage collector, but currently it does not.
Worse, there is code that insists all your allocations are pointed to by the root, that is, that you don't leave garbage.
I'm happy to use any API you provide.
After this is merged, we can see if it also fixes the other bug affecting the TC solver.
It works. |
to be checked: examples/example_abs_evars.v