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.

Sign up for GitHub

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

Jump to bottom

Cleanup the hypothesis conversion function #10052

Merged
merged 7 commits into from May 10, 2019
Merged

Cleanup the hypothesis conversion function #10052

merged 7 commits into from May 10, 2019

Conversation

ppedrot
Copy link
Member

@ppedrot ppedrot commented May 2, 2019 •
edited

This PR is an infrastructure change before the proper fix for #9919, and can be considered a followup of #9983.

The first commit alone, by only recomputing the order of named contexts after a change when the check flag is set is responsible for an important speed-up of Flocq.

┌────────────────────────┬─────────────────────────┬─────────────────────────────────────────────┬─────────────────────────────────────────────┬───────────────────────────────┬──────────────────────────┐
│                        │      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-flocq │  545.52  589.39 -7.44 % │     1517843866484     1640938509389 -7.50 % │     2065285784165     2274595955334 -9.20 % │    1265556    1243856 +1.74 % │     274     65 +321.54 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│             coq-sf-plf │   41.88   42.16 -0.66 % │      117811394645      118374566177 -0.48 % │      150312013548      150990534441 -0.45 % │     486640     486740 -0.02 % │      24     19  +26.32 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│         coq-coquelicot │   75.06   75.40 -0.45 % │      206652248685      207378068768 -0.35 % │      248057405417      248707294500 -0.26 % │     676376     680364 -0.59 % │     207     19 +989.47 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│        coq-fiat-crypto │ 4163.86 4181.50 -0.42 % │    11571216285985    11624597464305 -0.46 % │    18345682273124    18441605281745 -0.52 % │    2576120    2489040 +3.50 % │    1110    743  +49.39 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│             coq-geocoq │ 1995.97 2003.83 -0.39 % │     5566840058915     5590407288319 -0.42 % │     8025525562031     8075801787563 -0.62 % │    1194880    1190160 +0.40 % │     250    197  +26.90 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│           coq-compcert │ 1034.56 1038.52 -0.38 % │     2883787130672     2893705565919 -0.34 % │     4389846742431     4401794319036 -0.27 % │    1041356    1041244 +0.01 % │     209    165  +26.67 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│               coq-hott │  345.50  346.76 -0.36 % │      940594833197      944043426395 -0.37 % │     1421876768857     1427770700348 -0.41 % │     479264     479456 -0.04 % │     403      5 +7960.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│         coq-verdi-raft │ 1358.42 1361.90 -0.26 % │     3790295988590     3798381106885 -0.21 % │     5123867014111     5148281404093 -0.47 % │    1820328    1820400 -0.00 % │       2      0    +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│  coq-mathcomp-solvable │  204.71  205.23 -0.25 % │      571146108040      572041367071 -0.16 % │      764482803568      765755366262 -0.17 % │     804716     805476 -0.09 % │      15      0    +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│              coq-verdi │  124.26  124.38 -0.10 % │      345084261629      345188379251 -0.03 % │      441980381612      443718677498 -0.39 % │     589740     594148 -0.74 % │       6      8  -25.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│       coq-math-classes │  218.01  218.19 -0.08 % │      610199525780      610347110155 -0.02 % │      771176635823      771526405531 -0.05 % │     513932     513728 +0.04 % │      18     21  -14.29 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│   coq-mathcomp-algebra │  176.26  176.34 -0.05 % │      491343906008      491139337916 +0.04 % │      609610596233      609623947357 -0.00 % │     635320     634660 +0.10 % │       6      1 +500.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│              coq-color │  707.80  708.09 -0.04 % │     1977651363696     1979299121103 -0.08 % │     2351148098489     2355061823386 -0.17 % │    1391084    1391212 -0.01 % │      91    134  -32.09 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│               coq-corn │ 1506.78 1507.01 -0.02 % │     4204536920152     4206430604383 -0.05 % │     6197006117891     6197973001699 -0.02 % │     836748     836780 -0.00 % │       1     49  -97.96 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│     coq-mathcomp-field │  241.21  241.03 +0.07 % │      672058700944      672563051887 -0.07 % │      960072746991      960930024114 -0.09 % │     770440     770688 -0.03 % │       1      1   +0.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│ coq-mathcomp-odd-order │ 1552.99 1551.77 +0.08 % │     4323410192350     4324033516839 -0.01 % │     7263580572580     7267730507727 -0.06 % │    1223212    1246128 -1.84 % │      11     56  -80.36 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│        coq-lambda-rust │ 2086.96 2085.29 +0.08 % │     5818205263391     5811559712708 +0.11 % │     7979694438955     7979005180843 +0.01 % │    1382816    1384804 -0.14 % │      49      0    +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│          coq-fiat-core │  110.16  110.06 +0.09 % │      313114028859      313056642892 +0.02 % │      391158147580      391491573124 -0.09 % │     503328     503184 +0.03 % │     459    198 +131.82 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│       coq-fiat-parsers │  701.65  700.69 +0.14 % │     1960269321726     1961770095258 -0.08 % │     2977121976593     2982681113787 -0.19 % │    2839864    3031108 -6.31 % │     237    678  -65.04 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│            coq-unimath │ 2722.10 2717.33 +0.18 % │     7582713682725     7573328702733 +0.12 % │    13600895981219    13605814638394 -0.04 % │     911860     911020 +0.09 % │     273    379  -27.97 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│ coq-mathcomp-character │  206.22  205.47 +0.37 % │      573771009653      572629236167 +0.20 % │      763544914598      764286366073 -0.10 % │    1066712    1066184 +0.05 % │       2      2   +0.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│            coq-bignums │   73.03   72.62 +0.56 % │      202278713148      202624717385 -0.17 % │      266808463931      267143323195 -0.13 % │     500572     498856 +0.34 % │     179    161  +11.18 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│  coq-mathcomp-fingroup │   56.02   55.64 +0.68 % │      155731449611      155249333851 +0.31 % │      203201692976      203194416465 +0.00 % │     578940     579228 -0.05 % │      82     44  +86.36 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼──────────────────────────┤
│ coq-mathcomp-ssreflect │   40.78   40.25 +1.32 % │      112178804940      111754303477 +0.38 % │      134368548545      134401749821 -0.02 % │     529756     529812 -0.01 % │      11     62  -82.26 % │
└────────────────────────┴─────────────────────────┴─────────────────────────────────────────────┴─────────────────────────────────────────────┴───────────────────────────────┴──────────────────────────┘

(N.B.: the coq-mathcomp-ssreflect apparent slowdown is noise, as hinted by the mostly unchanged cycle count. I had run another bench before rebasing where this did not happen.)

Overlays:

@ppedrot ppedrot added the kind: cleanup Code removal, deprecation, refactorings, etc. label May 2, 2019
@ppedrot ppedrot requested review from amahboubi, forestjulien and a team as code owners May 2, 2019 23:22
@gares
Copy link
Member

gares commented May 3, 2019

There are a couple of check: false you add to set. Is it intentional?

@ppedrot
Copy link
Member Author

ppedrot commented May 3, 2019

Outside of tactics.ml, the check flags should be unchanged, they've just been made explicit. Did I misunderstand your question, or is there an instance that I messed up?

@gares
Copy link
Member

gares commented May 3, 2019

I meant SSR, not set sorry I wrote with my phone. I will point them out

@gares
Copy link
Member

gares commented May 3, 2019

It is when you call reduct_in_concl that I see false. Did you change its behaviour?

@jashug
Copy link
Contributor

jashug commented May 3, 2019

As far as I can tell, Tactics.reduct_in_concl had a default argument ?(check=false) that's being made explicit here.

@gares
Copy link
Member

gares commented May 4, 2019

Thanks, then this pr is good to me.

@ppedrot
Copy link
Member Author

ppedrot commented May 4, 2019

@herbelin you've been touching this code recently, do you want to be the assignee of this PR?

@herbelin herbelin self-requested a review May 4, 2019 17:58
herbelin
herbelin approved these changes May 4, 2019
View reviewed changes
Copy link
Member

@herbelin herbelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

do you want to be the assignee of this PR?

I can formally do the merge, but if someone had a closer look to the algorithmic part of the code than I had (@jashug or @gares), maybe can he also do the merge.

A side remark: What are the plans for logic.ml, wasn't it the plan that it eventually disappears? If so, maybe can Logic.convert_hyp goes to tactics.ml directly?

@ppedrot
Copy link
Member Author

ppedrot commented May 4, 2019

A side remark: What are the plans for logic.ml, wasn't it the plan that it eventually disappears? If so, maybe can Logic.convert_hyp goes to tactics.ml directly?

I thought about that, but tactics.ml is already quite big, and I don't like the idea to see it growing even more. It should probably be moved to some other low-level module for very basic tactic API.

@ppedrot
Copy link
Member Author

ppedrot commented May 4, 2019

@herbelin Also, there is not much algorithmic change for now, this PR is mostly a matter of moving code around and writing stupid fast paths.

@herbelin
Copy link
Member

herbelin commented May 4, 2019

there is not much algorithmic change for now

I was thinking to the check_decl_position and apply_to_hyp part which I skipped.

@ppedrot ppedrot force-pushed the cleanup-logic-convert-hyp branch 2 times, most recently from 285c802 to 479a547 Compare May 5, 2019 16:42
@herbelin herbelin self-assigned this May 5, 2019
@herbelin
Copy link
Member

herbelin commented May 5, 2019

I assigned, but overlays are needed for the now mandatory check:bool (wasn't it all green before the last force-push actually)?

@ppedrot
Copy link
Member Author

ppedrot commented May 6, 2019

@herbelin Yes, that was green, strangely enough. I'll write overlays anyways.

@ppedrot ppedrot added the needs: overlay This is breaking external developments we track in CI. label May 6, 2019
ppedrot added a commit to ppedrot/relation-algebra that referenced this pull request May 6, 2019
@ppedrot
Adapt to coq/coq#10052.
f1158a1
ppedrot added a commit to ppedrot/aac-tactics that referenced this pull request May 6, 2019
@ppedrot
Adapt to coq/coq#10052.
2331ca1
ppedrot added a commit to ppedrot/Coq-Equations that referenced this pull request May 6, 2019
@ppedrot
Adapt to coq/coq#10052.
63f4428
@ppedrot ppedrot force-pushed the cleanup-logic-convert-hyp branch from 479a547 to 685313f Compare May 6, 2019 20:27
ppedrot added a commit to ppedrot/coq that referenced this pull request May 6, 2019
@ppedrot
Add overlays for coq#10052.
685313f
ppedrot added a commit to mattam82/Coq-Equations that referenced this pull request May 6, 2019
@ppedrot
Merge pull request #204 from ppedrot/cleanup-logic-convert-hyp
f094965 
Adapt to coq/coq#10052.
palmskog added a commit to coq-community/aac-tactics that referenced this pull request May 7, 2019
@palmskog
Merge pull request #42 from ppedrot/cleanup-logic-convert-hyp
3b156bf 
Adapt to coq/coq#10052.
@ppedrot ppedrot removed the needs: overlay This is breaking external developments we track in CI. label May 8, 2019
@ppedrot ppedrot force-pushed the cleanup-logic-convert-hyp branch from 685313f to ed99695 Compare May 8, 2019 14:11
ppedrot added a commit to ppedrot/coq that referenced this pull request May 8, 2019
@ppedrot
Add overlays for coq#10052.
ed99695
@ppedrot
Copy link
Member Author

ppedrot commented May 8, 2019

@herbelin should be ready modulo CI.

@herbelin
Copy link
Member

herbelin commented May 9, 2019

should be ready modulo CI.

OK, shall merge tomorrow if no objections by then.

(The Ltac2 test should now be deactivated as far as I understood?)

@ppedrot ppedrot mentioned this pull request May 9, 2019
Merged
@ppedrot
Copy link
Member Author

ppedrot commented May 9, 2019

FTR, Ltac2 has been removed from the CI, so no problem anymore.

@ppedrot
Cleanup of Logic.convert_hyp.
4785156
@ppedrot
Logic.convert_hyp now takes an environment as an argument.
a5a89e8 
This prevents having to call global functions, for no good reason.
We also seize the opportunity to name the check argument.
@ppedrot
Make the check flag of conversion functions mandatory.
f7c5501 
The current situation is a mess, some functions set it by default, but other
no. Making it mandatory ensures that the expected value is the correct one.
@ppedrot
Split the hypothesis conversion check in a conversion + ordering check.
d313bc5
@ppedrot
Take advantage of the ordering / conversion check split.
4f3c70a
@ppedrot
Fast-path for reordering of a single closed variable.
1c4a11e 
Doesn't seem to matter in practice, but it doesn't hurt either.
@ppedrot
Add overlays for coq#10052.
1b4c0a1
@ppedrot ppedrot force-pushed the cleanup-logic-convert-hyp branch from ed99695 to 1b4c0a1 Compare May 10, 2019 10:55
@herbelin herbelin added this to the 8.11+beta1 milestone May 10, 2019
@herbelin herbelin merged commit 1b4c0a1 into coq:master May 10, 2019
herbelin added a commit that referenced this pull request May 10, 2019
@herbelin
Merge PR #10052: Cleanup the hypothesis conversion function
1fb2819 
Reviewed-by: herbelin
@ppedrot ppedrot deleted the cleanup-logic-convert-hyp branch May 11, 2019 10:24
chdoc pushed a commit to damien-pous/relation-algebra that referenced this pull request May 11, 2019
Merge pull request #8 from ppedrot/cleanup-logic-convert-hyp
aaab209 
Adapt to coq/coq#10052.
damien-pous pushed a commit to damien-pous/relation-algebra that referenced this pull request Feb 26, 2020
@ppedrot @damien-pous
Adapt to coq/coq#10052.
2aae5f0
damien-pous pushed a commit to damien-pous/relation-algebra that referenced this pull request Feb 27, 2020
@ppedrot @damien-pous
Adapt to coq/coq#10052.
23151df
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@herbelin herbelin herbelin approved these changes

@amahboubi amahboubi Awaiting requested review from amahboubi

@forestjulien forestjulien Awaiting requested review from forestjulien

Assignees

@herbelin herbelin

Labels
kind: cleanup Code removal, deprecation, refactorings, etc.
Projects
None yet
Milestone
8.11+beta1
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@ppedrot @gares @jashug @herbelin