Stream: Coq devs & plugin devs

Topic: Jason's PhD discussion


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 16:57):

There are other sources of quadratic behaviour.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 30 2020 at 16:57):

Sure, but just that mem analysis / sharing is scary

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 16:58):

On that we agree.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 16:59):

GC wouldn't help much, rather, we should change the evar representation.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 16:59):

But I don't know how to do that.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 30 2020 at 16:59):

Actually the quesiton just asked now is mine

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 17:02):

Nah, the problem lies in the instances.

view this post on Zulip 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.

view this post on Zulip 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.

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

I believe that implicit modules will help on that level.

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 17:04):

You mean an algebraic representation would help ? Or would it just move the problem around.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 17:05):

e.g. how do you substitute named variables without the instance?

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 17:05):

Sure.

view this post on Zulip Enrico Tassi (Nov 30 2020 at 17:05):

wonderful locally nameless?

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 17:06):

@Enrico Tassi this is moving the price somewhere else.

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 30 2020 at 17:06):

?

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 17:06):

but apart from backwards compat which would be hellish

view this post on Zulip Enrico Tassi (Nov 30 2020 at 17:06):

the proof engine is in locally nameless

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 17:06):

It's named though?

view this post on Zulip Enrico Tassi (Nov 30 2020 at 17:07):

locally names in contrast to nameless

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 17:07):

ah yeah

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 17:07):

so indeed, I'd be curious to see a nameless variant à la Matita

view this post on Zulip Enrico Tassi (Nov 30 2020 at 17:07):

so yes, it is named (w.r.t. the kernel)

view this post on Zulip Enrico Tassi (Nov 30 2020 at 17:07):

gotta go

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 17:07):

But I suspect that it'd be actually worse than the named approach

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 17:08):

Because you need to substitute eagerly in huge proof terms

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 17:08):

in that sense you're moving complexity around.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 17:08):

(see ya)

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 17:08):

@Enrico Do you mean changing evars to use de Bruijn instead of names?

view this post on Zulip 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.

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

Would be the best of both worlds.

view this post on Zulip Gaëtan Gilbert (Nov 30 2020 at 17:10):

Lean uses local names iirc

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 17:10):

Does that mean much more than passing functions like "safe_evar_value" ?

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

That means passing the evar map essentially.

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

You want the evar_info

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

I don't think that Lean has reached the "wall of complexity" yet.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 17:14):

Where the env would be instantiated by a global_env + evar_map I guess?

view this post on Zulip 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.)

view this post on Zulip 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: Oct 21 2021 at 21:03 UTC