Fix restrict_universe_context#7495
Conversation
SkySkimmer
added
needs: fixing
|
@gares could you check that it works for your bug? Since it's hard to trigger we will have to wait for unit tests to put a regression test in. |
|
Once merged I can enable restriction in elpi, and this triggers the bug... I'll prepare an overlay for you with minimisation on |
|
Feel free to push to my branch.
Gaëtan Gilbert
…On 13/05/2018 01:11, Enrico wrote:
Once merged I can enable restriction in elpi, and this triggers the
bug... I'll prepare an overlay for you with minimisation on
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
<#7495 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/ACWQ7Mo4t7mcNhLdq2tdgbRztPsy1hhrks5tx2wagaJpZM4T8jCm>.
|
|
Incidentally fixes the example in #5200. |
…pposed to fix
|
elpi passes! I see 3 tests failing:
|
|
I think @mattam82 is the most reasonable assignee here, given that @SkySkimmer authors the PR. Maybe also @ppedrot understand this code and can be shepherd. In case he can just override my assignment of this PR to Matthieu. |
…pposed to fix
|
the rebase dropped my commit, I hope it was not intended since I put it back |
|
There was no rebase, I did |
|
Well same result. For the formal-topology overlay, I'm not sure I did the right thing. |
well, given you did not pull this branch, you dropped my commit. No problem, but next time beware -f |
|
They will also need to make a branch for 8.8 testing unless this gets
backported.
Gaëtan Gilbert
…On 14/05/2018 15:15, Enrico wrote:
Well same result.
For the formal-topology overlay, I'm not sure I did the right thing.
I made a PR with the right set of changes, see bmsherman/topology#17
<bmsherman/topology#17> but
I made the PR on master, while the current branch being tested by ci
includes extra commits from other overlays I guess
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#7495 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/ACWQ7H0p3buCcX7fbPlr0aBJDSoU0yy4ks5tyYNvgaJpZM4T8jCm>.
|
|
I can't fix the test suite alone. The first error is about a missing instance, I passed |
mattam82
left a comment
mattam82
left a comment
There was a problem hiding this comment.
I'm trying to understand the difference it introduces. It can certainly select a different subset of the constraints. There are cases where it now selects a different subset of the kept universes, eliminating more spurious ones as well? I think overall the code is better that way, reusing the existing uGraph implementation.
| LSet.fold (fun v (csts,g as cstsg) -> | ||
| (** Fold through all pairs of kept universes. We avoid | ||
| recomputing for swapped order pairs. *) | ||
| if Level.compare u v >= 0 then cstsg |
There was a problem hiding this comment.
Why > here?
What do you mean?
There was a problem hiding this comment.
Why not Level.compare u v == 0
There was a problem hiding this comment.
Right, I don't understand the comment either... That's meant to avoid treating u = l, v = l twice?
| allkept cstsg) | ||
| allkept (Constraint.empty,g) | ||
| in | ||
| (LSet.inter univs keep, csts) |
There was a problem hiding this comment.
The universes we keep are exactly the same, as indicated by this line not changing. The constraints are not the same.
|
See the comment immediately above
Gaëtan Gilbert
…On 14/05/2018 19:55, Matthieu Sozeau wrote:
***@***.**** commented on this pull request.
------------------------------------------------------------------------
In engine/univops.ml
<#7495 (comment)>:
> + let test = [(u,Eq,v);(u,Lt,v);(v,Lt,u);(u,Le,v);(v,Le,u)] in
+ try Some (List.find (UGraph.check_constraint g) test)
+ with _ -> None
+
+let restrict_universe_context (univs, csts) keep =
+ let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
+ let g = UGraph.empty_universes in
+ let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
+ let g' = UGraph.merge_constraints csts g in
+ let removed = LSet.diff univs keep in
+ let allkept = LSet.diff allunivs removed in
+ let csts, _g = LSet.fold (fun u cstsg ->
+ LSet.fold (fun v (csts,g as cstsg) ->
+ (** Fold through all pairs of kept universes. We avoid
+ recomputing for swapped order pairs. *)
+ if Level.compare u v >= 0 then cstsg
Why not |Level.compare u v == 0|
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#7495 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/ACWQ7J0mMu0OdHyiw9FlQE2im0HY7nFmks5tycUDgaJpZM4T8jCm>.
|
|
If the universes are u and v we will see (u,u) (v,v) (u,v) and (v,u). We
skip (u,u) (v,v) because in a valid graph there are no interesting
constraints between them. We skip (u,v) or (v,u) because we don't care
about the order.
Gaëtan Gilbert
…On 14/05/2018 20:07, Matthieu Sozeau wrote:
***@***.**** commented on this pull request.
------------------------------------------------------------------------
In engine/univops.ml
<#7495 (comment)>:
> + let test = [(u,Eq,v);(u,Lt,v);(v,Lt,u);(u,Le,v);(v,Le,u)] in
+ try Some (List.find (UGraph.check_constraint g) test)
+ with _ -> None
+
+let restrict_universe_context (univs, csts) keep =
+ let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
+ let g = UGraph.empty_universes in
+ let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
+ let g' = UGraph.merge_constraints csts g in
+ let removed = LSet.diff univs keep in
+ let allkept = LSet.diff allunivs removed in
+ let csts, _g = LSet.fold (fun u cstsg ->
+ LSet.fold (fun v (csts,g as cstsg) ->
+ (** Fold through all pairs of kept universes. We avoid
+ recomputing for swapped order pairs. *)
+ if Level.compare u v >= 0 then cstsg
Right, I don't understand the comment either... That's meant to avoid
treating u = l, v = l twice?
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#7495 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/ACWQ7CCyahIWTloknRokhUMDmrCO3OmBks5tycfsgaJpZM4T8jCm>.
|
|
Good, I see now. |
|
I think this bug/PR should have high priority for two reasons:
|
gares
added
the
priority: high
|
New commit is a better version I'll leave it with separate commits for a bit so people can have a look. |
|
For the new version (vs master): |
| let rmap, csts = LSet.fold (fun u (rmap,csts) -> | ||
| let arcu = repr g u in | ||
| if LSet.mem arcu.univ kept then | ||
| LMap.add arcu.univ arcu.univ rmap, enforce_eq_level u arcu.univ csts |
There was a problem hiding this comment.
Ok, we add u = u so that the LMap.find on kept canonical universes works.
| else | ||
| match LMap.find arcu.univ rmap with | ||
| | v -> rmap, enforce_eq_level u v csts | ||
| | exception Not_found -> LMap.add arcu.univ u rmap, csts) |
There was a problem hiding this comment.
Here I'm a bit worried: rmap is in the process of being built, so we depend on the fold order somehow?
Otherwise, it looks to me that indeed, constraints_for will for sure not return constraints mentioning anything else than the kept universes.
There was a problem hiding this comment.
Here I'm a bit worried: rmap is in the process of being built, so we depend on the fold order somehow?
The fold order impacts which kept universe is canonical when the ugraph considers a removed universe to be canonical.
There was a problem hiding this comment.
What is the worry exactly? ie what can go wrong?
There was a problem hiding this comment.
Good, thanks for the explanation.
…pposed to fix
SkySkimmer
removed
the
needs: squashing
|
Squashed. |
|
Maybe this is not the right place but I'd like to know the answer to the point raised by @JasonGross, that is also where I wanted to go with my example: understand if this minimization can be specified at the semantic level of the graph, and not at its syntactic level. That is "having 1 syntactic predecessor" makes no sense, since the two graphs in my example are semantically equivalent but only in one case the node
Does this make sense? |
|
I don’t see how to do this properly without basically doing a transitive
closure computation. Ie when there is more than one predecessor, check if
one of them is above all the others in the transitive closure.
Le mer. 23 mai 2018 à 14:29, Enrico <notifications@github.com> a écrit :
… Maybe this is not the right place but I'd like to know the answer to the
point raised by @JasonGross <https://github.com/JasonGross>, that is also
where I wanted to go with my example: understand if this minimization can
be specified at the semantic level of the graph, and not at its syntactic
level.
That is "having 1 syntactic predecessor" makes no sense, since the two
graphs in my example are semantically equivalent but only in one case the
node v is purged.
Intuitively v has to be purged (made = to x) if:
- v has no successors (strict or weak, eg v is a node on the border of
the graph)
- x is the max of all the predecessors of v.
If there is a node x with such property then v=x (v is collapsed to x).
Does this make sense?
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#7495 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/AAGARVPU-nkuAuavRyhb78UCPa9wE7nlks5t1VYFgaJpZM4T8jCm>
.
|
|
I have a somewhat related minimization question. Minimization is currently done by joining universes different from I tried to hack When a variable occurs in Conversely, if I'd like in the cases above that some given universe variable is allowed to be minimized to Typical examples where this would be useful are the following: Check fun b : bool => if b then bool else True. (* works *)
Check fun b : bool => if b then True else bool. (* fails *)or Check bool = True. (* works *)
Check True = bool. (* fails *)Both failing examples would work and return the same sort as in the succeeding examples if we were able in #7369 to minimize the graph |
AFAICT (from the comments) this PR does the TC of the graph. Am I wrong? (otherwise my example is bogus). |
It stops at the first kept universe in any transitive chain. |
|
OK. Anyway, is it true that if we perform/reason-on the TC closure of the graph then restriction/minimization is a semantic property and not a syntactic one? I agree it is still an heuristic in the sense that one could be smarter and collapse more/less, but if we fix the criteria as in #7495 (comment) then: is the algorithm working at the semantic level? |
|
Yes, it can be made a semantic property of the TC of the graph. Actually, it might be feasible, I did not experiment. |
|
@gares what do you think, shall we merge this cleanup? @SkySkimmer it seems the HoTT failure happens no more, as there's no overlay and it works on gitlab, right? |
Yes. |
|
The cleanup should be merged IMO. |
|
Thanks for the answers everyone, I'll merge. |
|
@gares I'm not sure what you need to do about the overlay, just reminding you there was one for elpi |
|
It's fine, I'll eventually uncomment restriction in elpi, I should be able to update the branch we track in CI next week. |
5 participants
This should fix #7472 although I didn't test it.
Instead of messing with a buggy custom graph algorithm we go through the ugraph algorithm in a slightly brute-force manner.
It seems this impacts some tricky heuristic causing HoTT and formal-topology (and a HoTT-based test suite file) to fail. Still investigating.
Bench: https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/426/console
Despite the unsophisticated algorithm there is little impact, I think we rarely have many new universes / constraints per object.