Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix #5752: `Hint Mode` ignored for type classes that appear as assumptions #9996

Merged
merged 6 commits into from May 4, 2019

Conversation

@maximedenes
Copy link
Member

commented Apr 25, 2019

The creation of the local hint db now inherits the union of the modes
from the dbs passed to typeclasses eauto.

We could probably go further and define in a more systematic way the
metadata that should be inherited. A lot of this code could also be
cleaned up by defining the merge of databases, so that the search code
is parametrized by just one db (the merge of the input ones).

Fixes #5752.

  • Added / updated test-suite
  • Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
  • Entry added in CHANGES.md.

@maximedenes maximedenes added this to the 8.11+beta1 milestone Apr 25, 2019

@maximedenes maximedenes requested review from mattam82, ppedrot, SkySkimmer and coq/doc-maintainers as code owners Apr 25, 2019

@RalfJung RalfJung changed the title Fix #5752: `Hint Mode` ignored for type classes that appear as assump… … …tions Fix #5752: `Hint Mode` ignored for type classes that appear as assumptions Apr 25, 2019

Show resolved Hide resolved kernel/univ.ml Outdated
@maximedenes

This comment has been minimized.

Copy link
Member Author

commented Apr 25, 2019

@RalfJung can you let me know if the iris failure is expected?

Show resolved Hide resolved CHANGES.md
Show resolved Hide resolved tactics/class_tactics.ml Outdated
?st:TransparentState.t
(** The transparent_state used when working with local hypotheses *)
Hints.hint_mode array list GlobRef.Map.t * TransparentState.t
(** The transparent_state and modes used when working with local hypotheses *)

This comment has been minimized.

Copy link
@Zimmi48

Zimmi48 Apr 25, 2019

Member

I have wondered before if this function should be removed from the API since it's not used elsewhere. I'm still wondering.

This comment has been minimized.

Copy link
@maximedenes

maximedenes Apr 26, 2019

Author Member

I've been wondering too, but I'd rather remove it as part of a specific PR.

Show resolved Hide resolved test-suite/bugs/closed/bug_5752.v Outdated
@RalfJung

This comment has been minimized.

Copy link
Contributor

commented Apr 25, 2019

@robbertkrebbers is looking into this.

@robbertkrebbers

This comment has been minimized.

Copy link
Contributor

commented Apr 25, 2019

@RalfJung can you let me know if the iris failure is expected?

Failure in Iris was expected and fixed now :) This PR allowed me to fix many ambiguous occurrences where type annotations were needed. So 👍

@maximedenes maximedenes modified the milestones: 8.11+beta1, 8.10+beta1 Apr 25, 2019

@maximedenes maximedenes force-pushed the maximedenes:fix-assumptions-mode branch from 5c51399 to 24a33b5 Apr 26, 2019

@maximedenes

This comment has been minimized.

Copy link
Member Author

commented Apr 26, 2019

All comments addressed, this should be ready modulo CI. I'd need an assignee. Since @mattam82 is in the jungle, maybe @ppedrot ?

@maximedenes

This comment has been minimized.

Copy link
Member Author

commented Apr 26, 2019

modulo CI

And a benchmark, btw.

@maximedenes maximedenes force-pushed the maximedenes:fix-assumptions-mode branch from 24a33b5 to bc1da54 Apr 26, 2019

@vbgl

This comment has been minimized.

Copy link
Contributor

commented Apr 29, 2019

Are there some benchmark results available?

@maximedenes

This comment has been minimized.

Copy link
Member Author

commented Apr 29, 2019

Unfortunately, this patch seems to have some negative impact:

┌────────────────────────┬─────────────────────────┬─────────────────────────────────────────────┬─────────────────────────────────────────────┬───────────────────────────────┬──────────────────────────┐
│                        │      user time [s]      │                 CPU cycles                  │              CPU instructions               │     max resident mem [KB]     │        mem faults        │
│                        │                         │                                             │                                             │                               │                          │
│           package_name │     NEW     OLD PDIFF   │               NEW               OLD PDIFF   │               NEW               OLD PDIFF   │        NEW        OLD PDIFF   │     NEW    OLD   PDIFF   │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│ coq-mathcomp-ssreflect │   40.11   40.56 -1.11 % │      111155294021      111283593867 -0.12 % │      133663184194      133589430010 +0.06 % │     530340     530424 -0.02 % │      15    100  -85.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│          coq-fiat-core │  109.17  110.29 -1.02 % │      312595285016      314521089026 -0.61 % │      392777705885      392526316684 +0.06 % │     505996     505656 +0.07 % │     258    117 +120.51 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│               coq-corn │ 1491.21 1504.88 -0.91 % │     4161172624442     4199157838763 -0.90 % │     6204019031212     6196257825023 +0.13 % │     836744     836832 -0.01 % │       1      7  -85.71 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│  coq-mathcomp-fingroup │   55.49   55.90 -0.73 % │      154936951898      155685829663 -0.48 % │      203293888343      203182486809 +0.05 % │     579668     579236 +0.07 % │       4     53  -92.45 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│         coq-coquelicot │   75.17   75.71 -0.71 % │      206719934650      208173268440 -0.70 % │      249234296026      249811938236 -0.23 % │     707732     707840 -0.02 % │     206     17 +1111.76 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│            coq-unimath │ 2704.56 2722.53 -0.66 % │     7527154648083     7576973383352 -0.66 % │    13598338369772    13604366349229 -0.04 % │     912784     911120 +0.18 % │     283    379  -25.33 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│   coq-mathcomp-algebra │  174.80  175.95 -0.65 % │      487521021872      489512250730 -0.41 % │      611006095532      610519394339 +0.08 % │     637420     636064 +0.21 % │      86      1 +8500.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│           coq-compcert │ 1043.86 1050.14 -0.60 % │     2908558610364     2925585864793 -0.58 % │     4456906475896     4454957895868 +0.04 % │    1294888    1297064 -0.17 % │     199    181   +9.94 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│       coq-fiat-parsers │  705.08  709.27 -0.59 % │     1974936363515     1984797412138 -0.50 % │     3004877158410     3002398813722 +0.08 % │    3026476    3034644 -0.27 % │     211    676  -68.79 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│             coq-sf-plf │   41.92   42.16 -0.57 % │      117462831404      118582878163 -0.94 % │      150606013406      151203132628 -0.39 % │     498896     499052 -0.03 % │      24     19  +26.32 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│ coq-mathcomp-odd-order │ 1424.40 1432.50 -0.57 % │     3970177203649     3992928072873 -0.57 % │     6620975004331     6609788218350 +0.17 % │    1272704    1272492 +0.02 % │      14      7 +100.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│ coq-mathcomp-character │  205.09  206.16 -0.52 % │      571347868757      574496139822 -0.55 % │      765557280833      765678444188 -0.02 % │    1064040    1064044 -0.00 % │       1      2  -50.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│              coq-verdi │  124.83  125.38 -0.44 % │      346416033235      348342277739 -0.55 % │      447365353171      447676102748 -0.07 % │     610328     593116 +2.90 % │       6      9  -33.33 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│               coq-hott │  349.26  350.68 -0.40 % │      949418469703      954632706973 -0.55 % │     1442858561892     1441886891309 +0.07 % │     479648     479584 +0.01 % │     428      5 +8460.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│     coq-mathcomp-field │  237.76  238.72 -0.40 % │      662692193462      665804506267 -0.47 % │      954512074939      954485115014 +0.00 % │     756880     757284 -0.05 % │       0      2 -100.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│             coq-geocoq │ 2022.88 2030.70 -0.39 % │     5641676805001     5666417050147 -0.44 % │     8232219160816     8187032570006 +0.55 % │    1203184    1195740 +0.62 % │     170     38 +347.37 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│            coq-bignums │   72.33   72.57 -0.33 % │      201234542648      202099874227 -0.43 % │      267328334234      267104344123 +0.08 % │     502316     503416 -0.22 % │     174    116  +50.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│  coq-mathcomp-solvable │  201.39  201.93 -0.27 % │      561647970083      562520965005 -0.16 % │      753488857517      751694090182 +0.24 % │     806084     806032 +0.01 % │      15      0    +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│              coq-color │  709.18  710.46 -0.18 % │     1982794391065     1986597541703 -0.19 % │     2381329857766     2363462092520 +0.76 % │    1391172    1342740 +3.61 % │      20     58  -65.52 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│         coq-verdi-raft │ 1396.11 1397.95 -0.13 % │     3892014805109     3897114304878 -0.13 % │     5325527271828     5294217921447 +0.59 % │    1828176    1816220 +0.66 % │       2     16  -87.50 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│       coq-math-classes │  218.64  218.43 +0.10 % │      610851609320      610613348266 +0.04 % │      778278959500      771872080318 +0.83 % │     519676     514300 +1.05 % │      19     13  +46.15 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│        coq-fiat-crypto │ 4234.82 4225.99 +0.21 % │    11765308103313    11742165172948 +0.20 % │    18664558093402    18609560777325 +0.30 % │    2489128    2633988 -5.50 % │    1144    745  +53.56 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│        coq-lambda-rust │ 2108.00 2087.07 +1.00 % │     5874825808885     5811205311106 +1.09 % │     8091450937905     7980413404060 +1.39 % │    1414452    1393440 +1.51 % │      53      5 +960.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│              coq-flocq │  691.32  680.53 +1.59 % │     1920380446741     1894558961812 +1.36 % │     2744978917039     2691863008617 +1.97 % │    1727660    1727620 +0.00 % │     281    214  +31.31 % │
└────────────────────────┴─────────────────────────┴─────────────────────────────────────────────┴─────────────────────────────────────────────┴───────────────────────────────┴──────────────────────────┘

I'll need to investigate what's going on.

@Zimmi48

This comment has been minimized.

Copy link
Member

commented Apr 29, 2019

Before worrying and trying to investigate, I would re-run the bench several times on the most impacted packages. We might still be under the noise limit.

@maximedenes

This comment has been minimized.

Copy link
Member Author

commented Apr 29, 2019

Before worrying and trying to investigate, I would re-run the bench several times on the most impacted packages. We might still be under the noise limit.

I doubt so, the instruction count is fairly reliable usually. But I'll rerun to check.

@maximedenes

This comment has been minimized.

Copy link
Member Author

commented Apr 29, 2019

I doubt so

Although it is indeed suspicious that CompCert did not get the same impact as Flocq.

@maximedenes

This comment has been minimized.

Copy link
Member Author

commented Apr 29, 2019

@Zimmi48

This comment has been minimized.

Copy link
Member

commented Apr 29, 2019

I doubt so, the instruction count is fairly reliable usually. But I'll rerun to check.

I hadn't thought about this and had only looked at the timing reports.

@Zimmi48 Zimmi48 referenced this pull request Apr 29, 2019

Merged

Credits for 8.10 #9939

@maximedenes maximedenes force-pushed the maximedenes:fix-assumptions-mode branch from bc1da54 to f59bc9e Apr 29, 2019

@maximedenes

This comment has been minimized.

Copy link
Member Author

commented Apr 29, 2019

@ppedrot Somehow it seems I've made it much worse.

@maximedenes maximedenes modified the milestones: 8.10+beta1, 8.10.0 Apr 29, 2019

maximedenes added some commits Apr 24, 2019

Fix #5752: `Hint Mode` ignored for type classes that appear as assump…
…tions

The creation of the local hint db now inherits the union of the modes
from the dbs passed to `typeclasses eauto`.

We could probably go further and define in a more systematic way the
metadata that should be inherited. A lot of this code could also be
cleaned-up by defining the merge of databases, so that the search code
is parametrized by just one db (the merge of the input ones).

@ppedrot ppedrot force-pushed the maximedenes:fix-assumptions-mode branch from f59bc9e to 48b8657 May 2, 2019

@ppedrot

This comment has been minimized.

Copy link
Member

commented May 3, 2019

For some reason, a rerun on Flocq gives me only 1% slowdown. Furthermore, there are not many observable differences. Here are the the top lines in absolute timing increase.

src/Core/Float_prop.v.html:228 0.06 0.00 0.06 (inf%)
src/Pff/Pff.v.html:19811 0.06 0.03 0.09 (233%)
src/Pff/Pff.v.html:24188 0.06 2.96 3.02 (2%)
src/Pff/Pff.v.html:14688 0.07 1.05 1.12 (6%)
src/Pff/Pff.v.html:7542 0.07 1.31 1.38 (5%)
src/Pff/Pff.v.html:7557 0.07 1.30 1.37 (5%)
src/Pff/Pff.v.html:18774 0.08 3.31 3.38 (2%)
src/Pff/Pff.v.html:18768 0.08 3.29 3.37 (2%)
src/Pff/Pff.v.html:15168 0.08 2.38 2.47 (4%)
src/Pff/Pff.v.html:18771 0.09 3.30 3.39 (3%)
src/Prop/Double_rounding.v.html:4526 0.11 2.26 2.37 (5%)
src/Pff/Pff.v.html:24444 0.13 7.11 7.25 (2%)
src/Core/Zaux.v.html:19 0.13 0.22 0.36 (60%)
src/Pff/Pff.v.html:18326 0.14 0.13 0.26 (107%)
src/Pff/Pff.v.html:27793 0.23 0.13 0.36 (178%)

Not very significant...

@maximedenes

This comment has been minimized.

Copy link
Member Author

commented May 3, 2019

Hmmm, so it would be our bench infrastructure?

@ppedrot

This comment has been minimized.

Copy link
Member

commented May 3, 2019

My theory is that this PR adds a very spread out slowdown on the order of maginute of 1-1.5% of total time of Flocq. Very hard to pinpoint, because Flocq seems to be completely crazy regarding named contexts and this PR lightly touches it.

@maximedenes

This comment has been minimized.

Copy link
Member Author

commented May 3, 2019

@ppedrot so what should we do? merge this PR? The bug it fixes is rather severe IMHO.

@ppedrot

This comment has been minimized.

Copy link
Member

commented May 3, 2019

Judging from the fact that Flocq is getting a ~20% speedup by mere fiddling with conversion tactics, not even being smart, I wouldn't bother for 1%.

@maximedenes

This comment has been minimized.

Copy link
Member Author

commented May 3, 2019

Judging from the fact that Flocq is getting a ~20% speedup by mere fiddling with conversion tactics, not even being smart, I wouldn't bother for 1%.

Makes sense, so let's merge and ship it in the beta.

@ppedrot

ppedrot approved these changes May 4, 2019

@ppedrot

This comment has been minimized.

Copy link
Member

commented May 4, 2019

Let's merge then.

@coqbot coqbot added this to Request 8.10 inclusion in Coq 8.10 May 4, 2019

@ppedrot ppedrot merged commit 48b8657 into coq:master May 4, 2019

7 checks passed

GitLab CI pipeline Pipeline completed on GitLab CI
Details
coq.coq Build #20190502.21 succeeded
Details
coq.coq (Windows) Windows succeeded
Details
coq.coq (macOS) macOS succeeded
Details
doc:ml-api:odoc: ml-api artifact Link to ml-api build artifact.
Details
doc:refman: refman artifact Link to refman build artifact.
Details
doc:refman: stdlib artifact Link to stdlib build artifact.
Details

ppedrot added a commit that referenced this pull request May 4, 2019

Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that …
…appear as assumptions

Ack-by: RalfJung
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: maximedenes
Reviewed-by: ppedrot
Ack-by: robbertkrebbers

vbgl added a commit to vbgl/coq that referenced this pull request May 6, 2019

@coqbot coqbot moved this from Request 8.10 inclusion to Shipped in 8.10+beta1 in Coq 8.10 May 6, 2019

@maximedenes maximedenes deleted the maximedenes:fix-assumptions-mode branch May 15, 2019

amintimany pushed a commit to amintimany/iris that referenced this pull request Jun 13, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.