Fixing part of #5669: unification heuristics sensitive to alphabet #924
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
This reminds me a lot of universe minimization being sensitive to the file name, for similar reasons. So indeed, there may be other instances of the same problem. |
herbelin
force-pushed
the
master+fix-5669-alphabet-unif-heuristic-sensitivity
branch
from
0771d63
to
29c0896
Compare
|
You're right. We indeed had similar bugs already. |
|
Wow, that one's deserve a praise indeed! The fix looks good to me. |
|
May the fix for some of the cases be performance-sensitive? |
It adds a search through the evar context for each possible solutions when more than one is available, and, in common problems, this number rarely exceeds two (one for the dependent case, one for the non dependent case). Even on the worst artificial examples, it would add at most a O(n^2) cost on the number of variables in the context when several solutions exist, which is a cost common in unification. In theory, we could absorb this cost, by remembering the original position of each variable in the context, but by doing so we would allocate more, always. I'm not the complexity expert around, but I believe that working on compacting the identity part of instances would for instance be worther. Also, worther, even if liable to randomly affect the complexity, shall be various expected improvements of the unification such as not dropping too early exploration paths as we do now. |
…ce of names). This surprising bug was caused by an Id.Set which was ordering solutions to variable-projection problems in ascii order. We fix it by re-considering the variables involved in the solutions using the declaration order. Note that in practice, this implies preferring a dependent solution over a non-dependent one.
herbelin
force-pushed
the
master+fix-5669-alphabet-unif-heuristic-sensitivity
branch
from
29c0896
to
c24bcae
Compare
|
Just realized that I did not correctly push an optimization (my previous answer was relative to this further simplification). |
|
I guess a pendulum run should tell us if there's any impact. |
Zimmi48
added
kind: fix
|
Hum, I feel that this will be without noticeable impact but a test is started here. Edit: result gives minor variations with extrema +1.2 and -0.86. |
|
I took the initiative to remove the |
|
Indeed, the complete results are as follow: and the |
coqbot
pushed a commit
that referenced
this pull request
Nov 3, 2017
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Apr 15, 2018
This refines even further c24bcae (PR coq#924) and 6304c84: - c24bcae fixed the order in the heuristic - 6304c84 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases.
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Apr 15, 2018
This refines even further c24bcae (PR coq#924) and 6304c84: - c24bcae fixed the order in the heuristic - 6304c84 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases.
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Apr 15, 2018
This refines even further c24bcae (PR coq#924) and 6304c84: - c24bcae fixed the order in the heuristic - 6304c84 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases.
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Apr 16, 2018
This refines even further c24bcae (PR coq#924) and 6304c84: - c24bcae fixed the order in the heuristic - 6304c84 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases. Note that this has consequences on the test-suite (in output/Notations.v) as some problems now infer a dependent return clause.
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Apr 17, 2018
This refines even further c24bcae (PR coq#924) and 6304c84: - c24bcae fixed the order in the heuristic - 6304c84 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases. Note that this has consequences on the test-suite (in output/Notations.v) as some problems now infer a dependent return clause.
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Apr 18, 2018
This refines even further c24bcae (PR coq#924) and 6304c84: - c24bcae fixed the order in the heuristic - 6304c84 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases. Note that this has consequences on the test-suite (in output/Notations.v) as some problems now infer a dependent return clause.
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Apr 18, 2018
This refines even further c24bcae (PR coq#924) and 6304c84: - c24bcae fixed the order in the heuristic - 6304c84 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases. Note that this has consequences on the test-suite (in output/Notations.v) as some problems now infer a dependent return clause.
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Jul 28, 2018
This refines even further c24bcae (PR coq#924) and 6304c84: - c24bcae fixed the order in the heuristic - 6304c84 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases. Note that this has consequences on the test-suite (in output/Notations.v) as some problems now infer a dependent return clause.
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Jul 28, 2018
This refines even further c24bcae (PR coq#924) and 6304c84: - c24bcae fixed the order in the heuristic - 6304c84 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases. Note that this has consequences on the test-suite (in output/Notations.v) as some problems now infer a dependent return clause.
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Sep 11, 2018
This refines even further c24bcae (PR coq#924) and 6304c84: - c24bcae fixed the order in the heuristic - 6304c84 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases. Note that this has consequences on the test-suite (in output/Notations.v) as some problems now infer a dependent return clause.
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Sep 12, 2018
This refines even further c24bcae (PR coq#924) and 6304c84: - c24bcae fixed the order in the heuristic - 6304c84 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases. Note that this has consequences on the test-suite (in output/Notations.v) as some problems now infer a dependent return clause.
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Sep 14, 2018
This refines even further c24bcae (PR coq#924) and 6304c84: - c24bcae fixed the order in the heuristic - 6304c84 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases. Note that this has consequences on the test-suite (in output/Notations.v) as some problems now infer a dependent return clause.
silene
pushed a commit
that referenced
this pull request
Oct 16, 2018
This refines even further c24bcae (PR #924) and 6304c84: - c24bcae fixed the order in the heuristic - 6304c84 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases. Note that this has consequences on the test-suite (in output/Notations.v) as some problems now infer a dependent return clause. (cherry picked from commit 99ffdbb)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
A sensitivity to the order in which objects are stored in an OCaml
Setstructure.See bug report #5669 and commit message for details.
May other similar bugs hang around?