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

Kernel/checker reduction cleanups around projection unfolding #6686

Merged
merged 6 commits into from
Feb 7, 2018

Conversation

SkySkimmer
Copy link
Contributor

Essentially:

  • use Redflags.red_projection
  • share unfold_projection between CClosure and Reduction

- use Redflags.red_projection
- share unfold_projection between CClosure and Reduction
This just shares the unfold_projection between Closure and Reduction.
@SkySkimmer SkySkimmer added needs: review kind: cleanup Code removal, deprecation, refactorings, etc. part: kernel part: checker The coqchk binary for validating .vo files. labels Feb 2, 2018
Some (Zproj (pb.proj_npars, pb.proj_arg, Projection.constant p))
with Not_found ->
(* This is possible because sometimes for beta reduction we use a dummy env *)
None
Copy link
Contributor Author

@SkySkimmer SkySkimmer Feb 2, 2018

Choose a reason for hiding this comment

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

This is messed up. The issue can be witnessed by running some of the test suite files without this exception catching, eg 5761.v (spoilers: we get an uncaught Not_found).
The issue is at

coq/pretyping/reductionops.ml

Lines 1244 to 1246 in 76aff3c

let nf_beta = clos_norm_flags CClosure.beta (Global.env ())
let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ())
let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta (Global.env ())

These lines get run at module initialisation time so the environment is always empty.

Instead of catching the exception should we either:

  • eta-expand so that the environment is somewhat up to date
  • or change the interface so that the caller is in charge of passing the right environment?

Copy link
Member

Choose a reason for hiding this comment

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

Second solution (which implies first :) I had a patch to do that but probably before we moved to PRs :/

Copy link
Member

@mattam82 mattam82 left a comment

Choose a reason for hiding this comment

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

LGTM. Thanks !

@SkySkimmer SkySkimmer added needs: fixing The proposed code change is broken. and removed needs: review labels Feb 2, 2018
@SkySkimmer
Copy link
Contributor Author

Breaks equations.

@SkySkimmer
Copy link
Contributor Author

https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/305/console

┌──────────────────────────┬─────────────────────────┬─────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬─────────────────┐
│                          │      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-odd_order │ 1347.18 1371.33 -1.76 % │ 3750171182385 3821950618881 -1.88 % │  6682057917137  6682822410441 -0.01 % │ 1073200 1082240 -0.84 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│             coq-compcert │  799.33  808.31 -1.11 % │ 2230151226509 2252340865981 -0.99 % │  3415389152440  3413687530248 +0.05 % │ 1354172 1354388 -0.02 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│          coq-fiat-crypto │ 3492.62 3528.83 -1.03 % │ 9732285925813 9826051202677 -0.95 % │ 16524736668145 16534378179906 -0.06 % │ 3199580 3188768 +0.34 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│              coq-bignums │   74.34   75.08 -0.99 % │  206849823198  208555807688 -0.82 % │   281867319064   281896425291 -0.01 % │  521868  521908 -0.01 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                coq-flocq │   58.47   59.02 -0.93 % │  160828249919  162548537813 -1.06 % │   208565490784   209991437315 -0.68 % │  646048  650360 -0.66 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                coq-color │  558.01  562.35 -0.77 % │ 1563087821762 1572515898185 -0.60 % │  1977382809701  1976459030229 +0.05 % │ 1438948 1437944 +0.07 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│   coq-mathcomp-character │  264.48  266.38 -0.71 % │  735400242018  740594656230 -0.70 % │  1094894328337  1095345267039 -0.04 % │  982840  982832 +0.00 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│         coq-fiat-parsers │  651.68  656.31 -0.71 % │ 1825848447058 1836206395229 -0.56 % │  2971637995561  2970785606752 +0.03 % │ 3523652 3516148 +0.21 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│               coq-geocoq │ 3067.69 3088.00 -0.66 % │ 8560844592146 8606340102630 -0.53 % │ 14291890481017 14283850822054 +0.06 % │ 1212664 1211164 +0.12 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│     coq-mathcomp-algebra │  170.03  171.09 -0.62 % │  473110002856  475364640877 -0.47 % │   677518310774   677225582356 +0.04 % │  587692  587644 +0.01 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│           coq-coquelicot │   75.90   76.36 -0.60 % │  208645954671  209497283064 -0.41 % │   262417756330   262330455399 +0.03 % │  657104  657248 -0.02 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│    coq-mathcomp-solvable │  190.06  191.20 -0.60 % │  528378481451  531599005808 -0.61 % │   774299265738   774259268376 +0.01 % │  711584  711716 -0.02 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│   coq-mathcomp-ssreflect │   39.90   40.02 -0.30 % │  109573601812  110082855031 -0.46 % │   136134907340   136178290203 -0.03 % │  477968  477992 -0.01 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-real_closed │  166.83  167.28 -0.27 % │  463988380640  464685072619 -0.15 % │   717256770715   717261191941 -0.00 % │  726020  726320 -0.04 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│              coq-unimath │ 1289.44 1292.75 -0.26 % │ 3598941387112 3601904987338 -0.08 % │  6275408607810  6271988240106 +0.05 % │ 1104272 1042672 +5.91 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│            coq-fiat-core │   99.90   99.99 -0.09 % │  285183568648  285458592496 -0.10 % │   372557029698   372094285228 +0.12 % │  500624  500352 +0.05 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│       coq-mathcomp-field │  448.89  448.97 -0.02 % │ 1247880056163 1248434328021 -0.04 % │  2099273465041  2099268098411 +0.00 % │  725916  725896 +0.00 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│    coq-mathcomp-fingroup │   60.27   60.24 +0.05 % │  166581554639  166694154660 -0.07 % │   233909276448   233605946893 +0.13 % │  529116  529152 -0.01 % │   0   0  +nan % │
└──────────────────────────┴─────────────────────────┴─────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴─────────────────┘

@ppedrot ppedrot added needs: overlay This is breaking external developments we track in CI. and removed needs: fixing The proposed code change is broken. labels Feb 4, 2018
SkySkimmer added a commit to SkySkimmer/Coq-Equations that referenced this pull request Feb 5, 2018
@SkySkimmer SkySkimmer removed the needs: overlay This is breaking external developments we track in CI. label Feb 5, 2018
@Zimmi48 Zimmi48 added this to the 8.8 milestone Feb 5, 2018
@maximedenes
Copy link
Member

@SkySkimmer Would you mind opening a PR against Equations? I'll merge then notify them.

@SkySkimmer
Copy link
Contributor Author

Done (mattam82/Coq-Equations#48).

@maximedenes maximedenes merged commit 783c7d0 into coq:master Feb 7, 2018
cmangin added a commit to mattam82/Coq-Equations that referenced this pull request Feb 7, 2018
@SkySkimmer SkySkimmer deleted the ccnv-no-proj branch February 11, 2018 13:38
gares pushed a commit to gares/Coq-Equations that referenced this pull request Feb 23, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: cleanup Code removal, deprecation, refactorings, etc. part: checker The coqchk binary for validating .vo files. part: kernel
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

5 participants