Stream: Coq devs & plugin devs

Topic: `unshelve` and order of subgoals


view this post on Zulip Maxime Dénès (Jun 12 2020 at 07:39):

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?

view this post on Zulip Maxime Dénès (Jun 12 2020 at 07:41):

Maybe it's easier to maintain the order internally and provide an operation for reordering if necessary

view this post on Zulip Enrico Tassi (Jun 12 2020 at 08:26):

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).

view this post on Zulip Maxime Dénès (Jun 12 2020 at 08:30):

so what does this use case say about the order of subgoals?

view this post on Zulip Cyril Cohen (Jun 12 2020 at 11:26):

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.

view this post on Zulip Maxime Dénès (Jun 12 2020 at 11:36):

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)...

view this post on Zulip Matthieu Sozeau (Jun 12 2020 at 12:26):

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).

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:29):

I don't know, at least it breaks stdlib...

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:30):

I was also expecting scripts to not rely on it

view this post on Zulip Matthieu Sozeau (Jun 12 2020 at 12:31):

What's an example?

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:31):

you can see the pipeline at https://github.com/coq/coq/pull/12499

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:31):

it was precisely testing that

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:32):

but the compat layer does shelve all future goals by default...

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:33):

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

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:33):

the shelved status is maintained separately

view this post on Zulip Matthieu Sozeau (Jun 12 2020 at 12:34):

lra is using the shelve?

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:34):

I don't know, TBH

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:35):

I think I can keep the current behavior, while moving all this state to the evar_map

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:35):

but the behavior doesn't make much sense IMHO

view this post on Zulip Matthieu Sozeau (Jun 12 2020 at 12:37):

I'm not sure it's related to Lra, probably more trickiness with Unshelve in the proof derive_pt_recip_interv_decr in Ranalysis5

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:38):

ah, right, probably something like that

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:40):

the doc says that Unshelve puts the shelved goals at the end of the list of goals, while unshelve puts it at the beginning

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:40):

what's the reason for this design choice?

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:40):

the paragraphs are next to each other in the doc, so I imagine it is done on purpose

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:40):

https://coq.github.io/doc/master/refman/proof-engine/tactics.html#coq:cmd.unshelve

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:42):

maybe @Pierre-Marie Pédrot knows, IIRC he was the one who implemented the unshelve tactical

view this post on Zulip Matthieu Sozeau (Jun 12 2020 at 12:45):

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.

view this post on Zulip Jason Gross (Jun 13 2020 at 03:34):

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 21 2021 at 21:03 UTC