There's a discrepancy between the "new" proof engine and the legacy compat layer: in the first, shelved and regular goals are ordered separately, while in the second there's a global order. This explains for example the difference between simple refine
and unshelve refine
. Is it an intended design choice? What do users want w.r.t. unshelving in general? Should shelving followed by unshelving preserve the original order of goals, or reorder the goals like the current documentation of unshelve
says? Maybe @Jason Gross , @Pierre-Marie Pédrot or @Matthieu Sozeau have an idea?
Maybe it's easier to maintain the order internally and provide an operation for reordering if necessary
It would certainly help to have concrete use cases for the shelve. IMO the original one was to avoid having dangling goals and be able to implement Grab Existential Variables and proof progress printing without scanning the whole evar map (that amounts to the invariant: each evar is either a goal or a shelved).
so what does this use case say about the order of subgoals?
In my only explicit use case of the shelves (i.e. not resolved when a goal is closed) in mathcomp-analysis, I always maintain a reference to the shelved items in my active goals, and when they become unused, they are filled with a default value (which is a process I would like to automate btw), so I do not care about their order. I suspect any code that relies on their order might be not very robust.
I see, thanks, sounds like a sensible approach. Unfortunately, there seems to be code out there relying on the order of both models (the legacy one and the new one)...
I think for the compat layer you should be able to break any invariant on order, as there were no "shelved" goals in the old (8.2) model, right? Is it Grab Existentials that causes trouble in that case? I suppose it used to use the order on existential keys (order of creation of the evars).
I don't know, at least it breaks stdlib...
I was also expecting scripts to not rely on it
What's an example?
you can see the pipeline at https://github.com/coq/coq/pull/12499
it was precisely testing that
but the compat layer does shelve all future goals by default...
and if you do shelve / unshelve on future goals, you know that the data structure maintained in the evar_map is not the same as in the proofview
the shelved status is maintained separately
lra is using the shelve?
I don't know, TBH
I think I can keep the current behavior, while moving all this state to the evar_map
but the behavior doesn't make much sense IMHO
I'm not sure it's related to Lra, probably more trickiness with Unshelve in the proof derive_pt_recip_interv_decr in Ranalysis5
ah, right, probably something like that
the doc says that Unshelve
puts the shelved goals at the end of the list of goals, while unshelve
puts it at the beginning
what's the reason for this design choice?
the paragraphs are next to each other in the doc, so I imagine it is done on purpose
https://coq.github.io/doc/master/refman/proof-engine/tactics.html#coq:cmd.unshelve
maybe @Pierre-Marie Pédrot knows, IIRC he was the one who implemented the unshelve
tactical
Unshelve is generally called when no subgoals remain, but personally I would prefer if it put them at the beginning as well. It's useful when you want to track down where shelved goals are produced in a proof.
I believe simple refine
was added precisely because unshelve refine
reordered goals. I do occasionally use unshelve/shelve to move goals to the end (is there any other way to move a particular goal to the end of the list?). I think in my ideal world, there's a tactic for moving goals to the end of the goals list, and unshelve preserves the global ordering. Of course, I want to be able to write code that works with multiple versions of Coq, so I want some sort of good backwards compatibility story. (It also sounds like this might be a pain for f-c-l? Which I would like to keep working at least until the PR about evars that it found some bugs in gets merged.)
Last updated: Oct 13 2024 at 01:02 UTC