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

[econstr] Cleanup in vernac/classes.ml #6392

Merged
merged 1 commit into from
Dec 15, 2017

Conversation

ejgallego
Copy link
Member

@ejgallego ejgallego commented Dec 12, 2017

We fix quite a few types, and perform some cleanup wrt to the
evar_map, in particular we prefer to thread it now as otherwise
it may become trickier to check when we are using the correct one.

Overlay: mattam82/Coq-Equations#34

@ejgallego ejgallego added the kind: cleanup Code removal, deprecation, refactorings, etc. label Dec 12, 2017
@ejgallego ejgallego added this to the 8.8 milestone Dec 12, 2017
@ejgallego ejgallego force-pushed the econstr+fix_class branch 2 times, most recently from 5bd14f5 to bcbc88a Compare December 12, 2017 03:56
Copy link
Contributor

@SkySkimmer SkySkimmer left a comment

Choose a reason for hiding this comment

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

The nf_evars_and_universes and a couple almost-aliases like nf_evar_map_universes do universe minimization, so we can't just remove them.
I agree the name should mention minimization.

let pars = fst (List.chop lenpars args) in
match cl.cl_impl with
| IndRef ind ->
let ind = ind, u in
(Some (applistc (mkConstructUi (ind, 1)) args),
applistc (mkIndU ind) pars)
Copy link
Contributor

Choose a reason for hiding this comment

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

Should we maybe have econstr applistc instead?

Copy link
Member Author

Choose a reason for hiding this comment

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

I would be more in favor of removing one of the two, having two versions seems a bit pointless, right? Are they used in some particular combinator?

val instance_constructor : typeclass Univ.puniverses -> constr list ->
constr option * types
val instance_constructor : typeclass EConstr.puniverses -> EConstr.t list ->
EConstr.t option * EConstr.t
Copy link
Contributor

Choose a reason for hiding this comment

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

The other functions in this file could also be econstr.

Copy link
Member Author

Choose a reason for hiding this comment

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

I am not sure, it looks to me like a few of these functions are expected to return ground terms, right?

Copy link
Contributor

Choose a reason for hiding this comment

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

When I looked there were a few which did unsafe to constr, I would say at least those should use econstr.

if abstract then
begin
let subst = List.fold_left2
(fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
[] subst (snd k.cl_context)
in
let (_, ty_constr) = instance_constructor (k,u) subst in
let nf, subst = Evarutil.e_nf_evars_and_universes evars in
Copy link
Contributor

@SkySkimmer SkySkimmer Dec 12, 2017

Choose a reason for hiding this comment

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

This is required too, you just didn't hit a case where it was used.
Note to self: fixed but github doesn't see it on the next line.

Copy link
Member Author

Choose a reason for hiding this comment

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

Indeed Travis does show problems.

@@ -372,10 +369,7 @@ let context poly l =
let env = Global.env() in
let evars = ref (Evd.from_env env) in
let _, ((env', fullctx), impls) = interp_context_evars env evars l in
let fullctx = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) fullctx in
let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
Copy link
Contributor

Choose a reason for hiding this comment

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

This is also required.

@ejgallego
Copy link
Member Author

Interesting, thanks for having a look @SkySkimmer . I have a few questions thou:

  • Does this mean that every client of the API then has to take care itself of universe minimization?
  • Where is the documentation for these functions, what are exactly the invariants? AFAICS they are called inconsistently throu the code.
  • Does point 1 imply then that we have to add a test case for minimization to every operation saving a constant?
  • Also, does this imply that inferring universes when a term is saved should be better than inferring along its constructions?

I guess again this boils down to what the meaning of Constr.t is ( #6258 )

@SkySkimmer
Copy link
Contributor

Does this mean that every client of the API then has to take care itself of universe minimization?

Yes.

Where is the documentation for these functions, what are exactly the invariants? AFAICS they are called inconsistently throu the code.

Nonexistant.

Does point 1 imply then that we have to add a test case for minimization to every operation saving a constant?

Should maybe.

Also, does this imply that inferring universes when a term is saved should be better than inferring along its constructions?

I'm not sure what you mean by that.

It's tricky because if you're doing multiple constants at once which refer to each other (Axioms (foo : Foo) (bar : foo = foo).) you need to make sure to put in the right universes in the cross references, which means you minimize as a whole rather than once per constant. There are probably tricky issues with obligations and side effects and so on as well.

I think one thing we could do is provide a function

val definition_entry_easy : (* name TBD *)
  opaque:bool -> inline:bool -> ?types:EConstr.types ->
  proof_state:Evd.evar_map -> polymorphic:bool -> udecl:UState.universe_decl ->
  -> body:EConstr.t -> Safe_typing.private_constants definition_entry

which handles universe minimization, declaring universe binders, extracting private constant stuff from the evd and maybe some other misc stuff (up to changing the arguments a bit). (the definition_entry gets fed to declare_constant)

This should get actual design involving looking at what we do in core and what plugins do in the wild.

@ejgallego
Copy link
Member Author

Indeed you did read my mind. The current API is indeed problematic as the steps every client must do are very complex, and worse, dependent on low-level implementation details.

I'm not sure what you mean by that.

I meant that the client could just not care of universes and have some inference stuff done at QED time, but that may not work but polymorphism. I was just thinking out loud.

But going back to the actual code, indeed, it looks like most API users would like to build a constant in the way you propose. I think for example a good test plugin could be coq-paramcoq [crazy stuff there now, it would be good to see if your proposed API would work for them].

I would go even further, protecting [making private] all the universe minimization functions etc... So all the layers above engine can only use the easy function [unless they open Internal], then, I would be curious who needs Internal and why.

Clearly we have to do something that guarantees that minimization proceeds properly, adding 100 test cases seems not viable for me [mainly because we won't maintain them].

@ejgallego
Copy link
Member Author

Ok, some cleanup and fixes as suggested by @SkySkimmer done, I went a bit further and also cleaned up evar_map passing. Some comments are still valid thou.

@@ -112,22 +110,22 @@ let instance_hook k info global imps ?hook cst =
Typeclasses.declare_instance (Some info) (not global) cst;
(match hook with Some h -> h cst | None -> ())

let declare_instance_constant k info global imps ?hook id decl poly evm term termtype =
let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
Copy link
Contributor

Choose a reason for hiding this comment

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

Here you rename evm -> sigma but the one above you rename evars -> evd

Copy link
Member Author

Choose a reason for hiding this comment

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

More consistency needed indeed. The thing is that I am not so fond of sigma, but I recall that this is the proper convention, right @ppedrot ?

let _evd = ref sigma in
let impls, ((env', ctx), imps) = interp_context_evars env _evd ctx in
let c', imps' = interp_type_evars_impls ~impls env' _evd tclass in
let sigma = !_evd in
Copy link
Contributor

Choose a reason for hiding this comment

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

I don't like underscore variables.
How about

let sigma = ref sigma in
let impls, ... = ... in
let c', ... = ... in
let sigma = !sigma in 

Copy link
Member Author

Choose a reason for hiding this comment

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

That is temporal anyways, I have a patch migrating that not to use a ref. I like the underscore as it bugs people to fix it.

Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
let univs = Evd.check_univ_decl ~poly !evars decl in
let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
(* Note, this imperative updates the evar_map! [Then used in to_constr] *)
Copy link
Contributor

Choose a reason for hiding this comment

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

??

Copy link
Member Author

Choose a reason for hiding this comment

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

Leftover comment, good catch.

Some (Inr (c, subst))
let _evd = ref sigma in
let c = interp_casted_constr_evars env' _evd term cty in
Some (Inr (c, subst)), !_evd
Copy link
Contributor

Choose a reason for hiding this comment

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

Just use let sigma.

k.cl_props props subst))
in
let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
let _evd = ref sigma in
Copy link
Contributor

Choose a reason for hiding this comment

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

sigma

let fullctx = Context.Rel.map subst fullctx in
let ce t = Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr t) in
let sigma = Evd.from_env env in
let _evd = ref sigma in
Copy link
Contributor

Choose a reason for hiding this comment

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

sigma

@ejgallego
Copy link
Member Author

I've pushed a couple of minor nits, [keeping the _evd and IMHO it means "fix the API"] however I am not sure that patch is sound, it seems that to_constr is not strong enough so that raises interesting questions on the design of EConstr and how much can really gain [due to universes]

More interestingly, at least in my Travis we got a case where FLambda fails but not the regular build, interesting! It could well be a flambda bug, but the blame is likely on my side.

@ejgallego
Copy link
Member Author

Note that I have a very large patch doing a pass on Lemmas and Command. However I get very weird universe undefined errors, even when doing kind of trivial changes, so yeah, this is gonna go slow I'm afraid.

let _, ((env', fullctx), impls) = interp_context_evars env _evd l in
let sigma = !_evd in
(* Note, we must use the normalized evar from now on! *)
let evm,_ = Evarutil.nf_evars_and_universes sigma in
Copy link
Contributor

Choose a reason for hiding this comment

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

Why not use shadow sigma here?

@SkySkimmer
Copy link
Contributor

it seems that to_constr is not strong enough

How so?

@ejgallego
Copy link
Member Author

How so?

Let's wait for Travis, but basically I am replacing:

 let sigma, nf = Evarutil.nf_evar_map_universes sigma in
 let c         = EConstr.Unsafe.to_constr c           in
 let c         = nf c                                 in

by

 let sigma, _ = Evarutil.nf_evars_and_universes sigma in
 let c        = to_constr sigma c                     in

@ejgallego
Copy link
Member Author

By the way I'm sure this interests at least @gasche , in this travis we are getting different results for Coq compiled with -flambda and without: https://travis-ci.org/ejgallego/coq/builds/315578994

It could well be a Coq bug so not reporting upstream for now.

@gasche
Copy link
Contributor

gasche commented Dec 12, 2017

Interesting indeed! Let me know if you manage to reproduce this locally, and if you have simplified reproduction instructions.

There can be bugs in flambda, but it can also be the case that more aggressive optimizations change the evaluation order (in ways that are valid -- the evaluation order of OCaml programs is not uniquely specified -- but still result in observable differences in user code). We are trying to avoid these situations (they can be reported as issues that flambda people will try to fix), but they can still happen.

@ejgallego
Copy link
Member Author

Interesting indeed! Let me know if you manage to reproduce this locally, and if you have reproduction instructions.

Reproduction should be easy, just try to compile the Coq commit 7e787c4 with 4.06.0 and 4.06.0+flambda.

There were a couple of bugs in the patch [trying a fresh build], but given the nature of the code I found it interesting that only flambda showed a problem. Indeed, likely due to some dead code removal.

let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
let _evd = ref sigma in
Some (Inl (type_ctx_instance (push_rel_context ctx' env') _evd
kcl_props props subst)), !_evd
Copy link
Contributor

Choose a reason for hiding this comment

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

This line is broken in flambda, it returns non-modified sigma when we want the one modified by runnning type_ctx_instance (at least in ocamldebug).

Copy link
Contributor

Choose a reason for hiding this comment

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

Confirmed that let-lifting the function application fixes the missing constraint in crelationclasses.

Copy link
Contributor

Choose a reason for hiding this comment

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

This is typically a case where both evaluation orders are valid, so you should left-lift the type_ctx application indeed if it needs to be performed before !_evd is computed.

Copy link
Member Author

Choose a reason for hiding this comment

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

Oh indeed that was my fault; I was not so careful as I was planning to remove that code anyways.

Copy link
Member Author

Choose a reason for hiding this comment

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

In fact the ref and the _evd are already gone in the next PR.

ejgallego added a commit to ejgallego/Coq-Equations that referenced this pull request Dec 12, 2017
This just removes a few type castings. Indeed, it seems that the
upstream change was positive then.
We fix quite a few types, and perform some cleanup wrt to the
evar_map, in particular we prefer to thread it now as otherwise
it may become trickier to check when we are using the correct one.

Thanks to @SkySkimmer for lots of comments and bug-finding.
@ejgallego ejgallego added the needs: overlay This is breaking external developments we track in CI. label Dec 12, 2017
@ejgallego
Copy link
Member Author

So thanks to @SkySkimmer this is starting to look ready for merging. With regards the _evd, I would request a waiver. They will be gone in a next PR and IMHO they should be left as this as to remind they are FIXMEs.

@ejgallego ejgallego changed the title [econstr] Some cleanup in the upper layers. [econstr] Cleanup in `vernac/classes.ml Dec 12, 2017
@ejgallego ejgallego changed the title [econstr] Cleanup in `vernac/classes.ml [econstr] Cleanup in vernac/classes.ml Dec 12, 2017
@ejgallego ejgallego added the needs: benchmarking Performance testing is required. label Dec 13, 2017
@ppedrot
Copy link
Member

ppedrot commented Dec 13, 2017

@ejgallego AFAIU, nf_evar_map_universes is not the identity w.r.t. universe expansion, it also generates proxy universes in the returned term. No wonder why you cannot drop it.

Copy link
Contributor

@SkySkimmer SkySkimmer left a comment

Choose a reason for hiding this comment

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

Looks ready to me as well.

@ejgallego
Copy link
Member Author

@ejgallego AFAIU, nf_evar_map_universes is not the identity w.r.t. universe expansion, it also generates proxy universes in the returned term. No wonder why you cannot drop it.

Thanks for the explanation, it is a bit hard to figure out what is the proper normalization to apply.

@ejgallego
Copy link
Member Author

ejgallego commented Dec 15, 2017

@ejgallego ejgallego removed the needs: benchmarking Performance testing is required. label Dec 15, 2017
@ejgallego
Copy link
Member Author

Finally ready.

@ejgallego
Copy link
Member Author

┌──────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬─────────────────┐
│                          │      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-sf-lf │   15.48   15.86 -2.40 % │    43231801650    43250681253 -0.04 % │    60510923302    60390306981 +0.20 % │  418124  418096 +0.01 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│       coq-mathcomp-field │  449.20  452.42 -0.71 % │  1251235345335  1259759462038 -0.68 % │  2100893489664  2101111341698 -0.01 % │  725192  723040 +0.30 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│             coq-compcert │  810.45  815.14 -0.58 % │  2258612385178  2270928416186 -0.54 % │  3427325716695  3425114962396 +0.06 % │ 1339892 1347604 -0.57 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│         coq-fiat-parsers │  672.63  675.22 -0.38 % │  1860951864514  1865245842295 -0.23 % │  3030770815766  3025470001775 +0.18 % │ 3507024 3510164 -0.09 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│              coq-unimath │ 1293.02 1297.99 -0.38 % │  3601375655576  3620506717846 -0.53 % │  6247973517945  6243762641329 +0.07 % │ 1135212 1077060 +5.40 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│            coq-fiat-core │  119.27  119.70 -0.36 % │   314256880423   313115466799 +0.36 % │   421188171685   418873376311 +0.55 % │  500564  498880 +0.34 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│   coq-mathcomp-character │  266.94  267.74 -0.30 % │   742501955494   744554803726 -0.28 % │  1099168495208  1099227962069 -0.01 % │  982544  982732 -0.02 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│    coq-mathcomp-solvable │  192.32  192.87 -0.29 % │   534346950694   535553199499 -0.23 % │   778620656028   778132672744 +0.06 % │  712784  710764 +0.28 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│          coq-fiat-crypto │ 3715.35 3723.65 -0.22 % │ 10336862272381 10357857235060 -0.20 % │ 17673397253133 17640097930769 +0.19 % │ 3273484 3273664 -0.01 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│               coq-geocoq │ 3086.20 3092.72 -0.21 % │  8598164690168  8627779994706 -0.34 % │ 14347612591612 14328118670173 +0.14 % │ 1252132 1215264 +3.03 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│              coq-bignums │   75.49   75.59 -0.13 % │   210066705345   210132240560 -0.03 % │   287388940083   287363066783 +0.01 % │  524928  524692 +0.04 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-real_closed │  168.25  168.26 -0.01 % │   467400791365   467593147268 -0.04 % │   717203332214   717464321280 -0.04 % │  726576  725884 +0.10 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│     coq-mathcomp-algebra │  171.12  171.02 +0.06 % │   475131386157   475043164796 +0.02 % │   675771319049   675578150801 +0.03 % │  586576  586352 +0.04 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                coq-flocq │   58.44   58.38 +0.10 % │   160667109915   160601445736 +0.04 % │   207105505168   208145586499 -0.50 % │  645128  645148 -0.00 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│    coq-mathcomp-fingroup │   60.03   59.93 +0.17 % │   166164724285   166585242613 -0.25 % │   233105042490   233255870310 -0.06 % │  532368  531684 +0.13 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│   coq-mathcomp-odd_order │ 1390.35 1387.40 +0.21 % │  3873151318245  3866881268405 +0.16 % │  6726925071837  6728518726075 -0.02 % │ 1113424 1088996 +2.24 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│           coq-coquelicot │   75.24   74.95 +0.39 % │   207626472973   206723108684 +0.44 % │   260916285238   260449749993 +0.18 % │  657920  657452 +0.07 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│               coq-sf-plf │   42.14   41.96 +0.43 % │   117381836147   117294997787 +0.07 % │   154812706352   154695853271 +0.08 % │  517248  517712 -0.09 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│   coq-mathcomp-ssreflect │   39.61   39.44 +0.43 % │   108778967108   108463874256 +0.29 % │   135076123138   135003996004 +0.05 % │  477208  476884 +0.07 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                coq-color │  569.80  564.47 +0.94 % │  1593253421353  1579045365891 +0.90 % │  2012908251494  2007056679857 +0.29 % │ 1436740 1438532 -0.12 % │   0   0  +nan % │
└──────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴─────────────────┘

@maximedenes maximedenes merged commit 7799626 into coq:master Dec 15, 2017
mattam82 added a commit to mattam82/Coq-Equations that referenced this pull request Dec 15, 2017
@ejgallego ejgallego deleted the econstr+fix_class branch December 15, 2017 17:01
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. needs: overlay This is breaking external developments we track in CI.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants