Stream: Coq devs & plugin devs

Topic: moving more files to EConstr


view this post on Zulip Hugo Herbelin (Nov 12 2020 at 07:58):

@Pierre-Marie Pédrot , @Emilio Jesús Gallego Arias : any objections if I move indrec.ml, inductiveops.ml, logic.ml and similar files to EConstr? At first view, it is only threading the sigma (how costly could it be?) and possibly avoiding a few costly to_constr. In particular, should I be afraid of a slowdown risk?

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 09:49):

Beware with Logic, the other should be fine.

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 09:50):

I remember that I had trouble with efficiency when trying to port Logic because there are a few critical calls to unsafe back and forth conversions in there

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 09:50):

(Or maybe it was breaking? I don't remember, this was already quite a long time ago.)

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 09:51):

But I distinctly remember porting Logic to EConstr already and not pushing it further

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 10:04):

(Also I'd advise against wasting time on Logic. It's legacy code that is bound to disappear.)

view this post on Zulip Hugo Herbelin (Nov 12 2020 at 10:25):

My initial motivation was to use the API of inductiveops.ml on EConstr. I don't really care about logic.ml, it arrives as a dependency of a change in inductiveops.mli. So, maybe, I'll keep logic.ml as it is then.

view this post on Zulip Hugo Herbelin (Nov 12 2020 at 10:31):

And is it essential that vnorm.ml is in constr?

view this post on Zulip Hugo Herbelin (Nov 12 2020 at 13:19):

Actually, I don't know how is perceived the Inductiveops API. It avoids some inductive data routine massaging, but controlling the exact amount of job which is done is difficult.

view this post on Zulip Hugo Herbelin (Nov 12 2020 at 13:26):

Currently, Termops.lift_rel_context and friends are on constr. If I need a variant of them on EConstr, do I add them to EConstr.Vars, to EConstr? Do I made a Constr or EConstr submodule to Termops? Any idea? (By default, I may lean to add it eConstr.ml.)

view this post on Zulip Hugo Herbelin (Nov 12 2020 at 13:32):

Or we split Termops into Constrops and EConstrops?


Last updated: Oct 16 2021 at 03:02 UTC