Emilio Jesús Gallego Arias (Nov 30 2020 at 16:55): Emilio Jesús Gallego Arias (Nov 30 2020 at 16:55):Indeed, as observed with OCaml profiling tools, Coq's engine, in particular the allocation of evars seems to be far from state of the art, looking at the memory numbers I wonder how much of the problems are just due to this.
Emilio Jesús Gallego Arias (Nov 30 2020 at 16:57):So indeed comparing the proof engine to a reflective procedure is just comparing apples to oranges, in the sense that one engine has not even a GC, whereas the other will use OCaml's GC which is indeed pretty nice.
Pierre-Marie Pédrot (Nov 30 2020 at 16:57):There are other sources of quadratic behaviour.
Pierre-Marie Pédrot (Nov 30 2020 at 16:57):As mentioned, VM compilation of closure is quadratic in the number of binders as well.
Emilio Jesús Gallego Arias (Nov 30 2020 at 16:57):Sure, but just that mem analysis / sharing is scary
Emilio Jesús Gallego Arias (Nov 30 2020 at 16:58):the numbers I saw seem pretty worrying, that's a hard problem to solve, sure
Pierre-Marie Pédrot (Nov 30 2020 at 16:58):Also, a lot of the code is very naive, e.g. unification where we repeatedly compute compositional data over subcomponents.
Emilio Jesús Gallego Arias (Nov 30 2020 at 16:58):but indeed, I mean, not surprising. The current architecture cannot just do the kind of proofs Jason is doing efficiently
Pierre-Marie Pédrot (Nov 30 2020 at 16:58):On that we agree.
Emilio Jesús Gallego Arias (Nov 30 2020 at 16:59):It would be super-interesting to compare the number would engine had a GC and better evar management
Pierre-Marie Pédrot (Nov 30 2020 at 16:59):GC wouldn't help much, rather, we should change the evar representation.
Pierre-Marie Pédrot (Nov 30 2020 at 16:59):But I don't know how to do that.
Emilio Jesús Gallego Arias (Nov 30 2020 at 16:59):Actually the quesiton just asked now is mine
Matthieu Sozeau (Nov 30 2020 at 17:02):I was wondering if not storing contexts (having closed evars c : forall ctx, ty) would change anything but I guess not.
Pierre-Marie Pédrot (Nov 30 2020 at 17:02):Nah, the problem lies in the instances.
Pierre-Marie Pédrot (Nov 30 2020 at 17:03):It's an engineering problem. We want compact instance representation, but then we need to duplicate the kernel to handle evar-bearing terms.
Pierre-Marie Pédrot (Nov 30 2020 at 17:03):'cause everytime you see an Evar node, you need an evarmap to retrieve the uncompressed evar instance.
Pierre-Marie Pédrot (Nov 30 2020 at 17:04):I believe that implicit modules will help on that level.
Matthieu Sozeau (Nov 30 2020 at 17:04):You mean an algebraic representation would help ? Or would it just move the problem around.
Pierre-Marie Pédrot (Nov 30 2020 at 17:05):What I mean is that when you get an EConstr in the kernel, you don't have enough data to perform anything if you don't have either the sigma or the full instance around
Pierre-Marie Pédrot (Nov 30 2020 at 17:05):e.g. how do you substitute named variables without the instance?
Matthieu Sozeau (Nov 30 2020 at 17:05):Sure.
Enrico Tassi (Nov 30 2020 at 17:05):wonderful locally nameless?
Pierre-Marie Pédrot (Nov 30 2020 at 17:06):@Enrico Tassi this is moving the price somewhere else.
Pierre-Marie Pédrot (Nov 30 2020 at 17:06):I'd be very pleased to see a variant of the proof engine with locally nameless
Enrico Tassi (Nov 30 2020 at 17:06):?
Pierre-Marie Pédrot (Nov 30 2020 at 17:06):but apart from backwards compat which would be hellish
Enrico Tassi (Nov 30 2020 at 17:06):the proof engine is in locally nameless
Pierre-Marie Pédrot (Nov 30 2020 at 17:06):It's named though?
Enrico Tassi (Nov 30 2020 at 17:07):locally names in contrast to nameless
Pierre-Marie Pédrot (Nov 30 2020 at 17:07):ah yeah
Pierre-Marie Pédrot (Nov 30 2020 at 17:07):so indeed, I'd be curious to see a nameless variant à la Matita
Enrico Tassi (Nov 30 2020 at 17:07):so yes, it is named (w.r.t. the kernel)
Enrico Tassi (Nov 30 2020 at 17:07):gotta go
Pierre-Marie Pédrot (Nov 30 2020 at 17:07):But I suspect that it'd be actually worse than the named approach
Pierre-Marie Pédrot (Nov 30 2020 at 17:08):Because you need to substitute eagerly in huge proof terms
Pierre-Marie Pédrot (Nov 30 2020 at 17:08):in that sense you're moving complexity around.
Pierre-Marie Pédrot (Nov 30 2020 at 17:08):(see ya)
Matthieu Sozeau (Nov 30 2020 at 17:08):@Enrico Do you mean changing evars to use de Bruijn instead of names?
Pierre-Marie Pédrot (Nov 30 2020 at 17:09):But viz the evar representation there is hope if we make the kernel parametric in the kind of terms it manipulates.
Pierre-Marie Pédrot (Nov 30 2020 at 17:09):Would be the best of both worlds.
Gaëtan Gilbert (Nov 30 2020 at 17:10):Lean uses local names iirc
Matthieu Sozeau (Nov 30 2020 at 17:10):Does that mean much more than passing functions like "safe_evar_value" ?
Pierre-Marie Pédrot (Nov 30 2020 at 17:12):That means passing the evar map essentially.
Pierre-Marie Pédrot (Nov 30 2020 at 17:12):You want the evar_info
Pierre-Marie Pédrot (Nov 30 2020 at 17:12):I don't think that Lean has reached the "wall of complexity" yet.
Pierre-Marie Pédrot (Nov 30 2020 at 17:13):@Matthieu Sozeau ideally you'd have a type 'a constr, and a type 'a env.
Matthieu Sozeau (Nov 30 2020 at 17:14):Where the env would be instantiated by a global_env + evar_map I guess?
Guillaume Melquiond (Nov 30 2020 at 17:41):In Why3, we are using a mixed representation. Bound variables are locally named, but substitutions stop at binders. In other words, we have implicit substitutions for unbound terms, and explicit ones for bound terms. Thus, performances would be disastrous if we were opening the same quantifiers again and again. But in practice, a quantified term is visited at most once, so the whole mechanism is kind of constant time. (But, since Why3 is first order while Coq is higher order, I am not sure we can have the same expectation for Coq.)
Enrico Tassi (Nov 30 2020 at 20:39):Gaëtan Gilbert said:
Lean uses local names iirc
Lean uses imperative updates + copy, yet another beast, AFAIK
Last updated: May 31 2023 at 17:01 UTC