The scary stuff thread [you've been warned] [we troll] · CUDW 2020

Popping up a level: how should terms be represented in an ideal (ly performant) system? Terms + hashconsing, DAGs with pointers everywhere, functional structures with "zippers", other?

Cody Roux (Dec 01 2020 at 21:49):

Should Evars be mutable?

Enrico Tassi (Dec 01 2020 at 21:49):

was Frankestein elegant?

Pierre-Marie Pédrot (Dec 01 2020 at 21:49):

Hashconsing is another beast. Filliâtre claims that everything should hashcons implicitly, but the assumptions of this reasoning is flawed in Coq.

Enrico Tassi (Dec 01 2020 at 21:49):

Cody Roux said:

Should Evars be mutable?

it's an implementation detail. According to my experience: yes.

Pierre-Marie Pédrot (Dec 01 2020 at 21:50):

The problem with mutable evars is that I don't see how not to have a super buggy engine.

Pierre-Marie Pédrot (Dec 01 2020 at 21:50):

Barring a type system à la Rust

Enrico Tassi (Dec 01 2020 at 21:50):

you trail the updates?

Pierre-Marie Pédrot (Dec 01 2020 at 21:50):

you could do that, but it has a cost as well.

Pierre-Marie Pédrot (Dec 01 2020 at 21:51):

especially in a very backtracking setting you'll lose all the benefits.

Enrico Tassi (Dec 01 2020 at 21:51):

yes and no. a pretty standard (necessay) optimization is that if you don't have choice points, then you don't trail. if you do so, you are as efficient as ocaml (with mutable state).

Pierre-Marie Pédrot (Dec 01 2020 at 21:51):

looks reasonable.

Enrico Tassi (Dec 01 2020 at 21:51):

but you also gain ocaml's GC on this heap we call evarmap

Enrico Tassi (Dec 01 2020 at 21:51):

today we have no GC at all

Pierre-Marie Pédrot (Dec 01 2020 at 21:51):

Yeah, it's a clear bonus.

Enrico Tassi (Dec 01 2020 at 21:52):

elpi "POC" (in the git repo) was written like Coq. When we move to imperative evars + trail we got 10x speedup

Pierre-Marie Pédrot (Dec 01 2020 at 21:52):

No GC is bad for memory consumption but I don't think it affects speed that much.

Pierre-Marie Pédrot (Dec 01 2020 at 21:52):

I am not surprised.

Enrico Tassi (Dec 01 2020 at 21:53):

maybe in Coq it would not be that much, but I would be surprised if it was not visible

Cody Roux (Dec 01 2020 at 21:53):

Is there some "canonical paper" for how to implement mutable Evars in this way? Are trails just suspended substitutions?

Enrico Tassi (Dec 01 2020 at 21:53):

the trail is just to undo assignments

Enrico Tassi (Dec 01 2020 at 21:54):

you still need to apply evars to all its arguments

Cody Roux (Dec 01 2020 at 21:54):

that happens when you get a unification failure?

Enrico Tassi (Dec 01 2020 at 21:54):

which is a sort of suspended substitution

Enrico Tassi (Dec 01 2020 at 21:54):

if I get what you mean

Cody Roux (Dec 01 2020 at 21:54):

I feel like a 3rd grader in this thread

Pierre-Marie Pédrot (Dec 01 2020 at 21:54):

From my experiments, evar access has a clear cost but it's not the major source of speed issues.

Pierre-Marie Pédrot (Dec 01 2020 at 21:55):

@Cody Roux a trail is the standard trick to implement "immutability"-like behaviour with mutable state.

Pierre-Marie Pédrot (Dec 01 2020 at 21:55):

like in persistent arrays

Enrico Tassi (Dec 01 2020 at 21:55):

it's a log of things you have to undo

Cody Roux (Dec 01 2020 at 21:56):

Ok. But in what situations do you have to undo Evar instanciations? I feel like I should know this...

Pierre-Marie Pédrot (Dec 01 2020 at 21:56):

If you backtrack.

Enrico Tassi (Dec 01 2020 at 21:56):

tac1 || tac2

Cody Roux (Dec 01 2020 at 21:56):

Ok. But this doesn't happen at elaboration time.

Enrico Tassi (Dec 01 2020 at 21:57):

if tac1 assigns some evars before failing, then tac2 should start from scratch

Pierre-Marie Pédrot (Dec 01 2020 at 21:57):

Oh, it probably does.

Pierre-Marie Pédrot (Dec 01 2020 at 21:57):

Who knows what case elaboration does!

Enrico Tassi (Dec 01 2020 at 21:57):

eg, during type class instance search

Cody Roux (Dec 01 2020 at 21:57):

Right, but that's more of a bug than a feature.

Pierre-Marie Pédrot (Dec 01 2020 at 21:57):

Type class search is collapsed to its first result in elaboration currently.

Pierre-Marie Pédrot (Dec 01 2020 at 21:58):

aka "the pretyper is not in the monad"

Pierre-Marie Pédrot (Dec 01 2020 at 21:58):

So in elaboration proper we don't really have backtracking. (We do in unification, type class search, tactics in terms, etc.)

Cody Roux (Dec 01 2020 at 21:59):

Ok this is good to know.

Pierre-Marie Pédrot (Dec 01 2020 at 21:59):

We would like to have a bit more controlled backtracking in some cases.

Pierre-Marie Pédrot (Dec 01 2020 at 21:59):

Like the pretyper assigning universes too eagerly.

Enrico Tassi (Dec 01 2020 at 21:59):

TC search can backtrack internally

Pierre-Marie Pédrot (Dec 01 2020 at 21:59):

The dreaded "foo has type Type but was expected of type Set" error

Pierre-Marie Pédrot (Dec 01 2020 at 21:59):

where you never wrote Type in the first place

Pierre-Marie Pédrot (Dec 01 2020 at 22:00):

anyway, backtracking on the beginning of the conversation

Pierre-Marie Pédrot (Dec 01 2020 at 22:00):

proof engine needs fast evars

Cody Roux (Dec 01 2020 at 22:01):

I wish I understood universe polymorphism better tbh. When I was young and stupid I thought it was easy to have explicit universe quantifiers in the kernel, but now I'm not so sure.

Pierre-Marie Pédrot (Dec 01 2020 at 22:01):

It is easy.

Pierre-Marie Pédrot (Dec 01 2020 at 22:01):

It is just a catastrophe performance-wise.

Cody Roux (Dec 01 2020 at 22:01):

Ok, maybe I was confused by the number of critical bugs involving them.

Pierre-Marie Pédrot (Dec 01 2020 at 22:01):

Ah, this is just a historical accident due to 8.5

Pierre-Marie Pédrot (Dec 01 2020 at 22:02):

"The StillBorn 9.0 from Hell"

Cody Roux (Dec 01 2020 at 22:02):

I love how we present Coq to other people vs how we speak about it internally

Pierre-Marie Pédrot (Dec 01 2020 at 22:02):

were three (four?) major branches were merged at the same time, resulting in a code mess we're currently finishing up to clean

Enrico Tassi (Dec 01 2020 at 22:02):

Note that I got user reports that CoqIDE 8.5 was better than CoqIDE 8.6 :-P

Pierre-Marie Pédrot (Dec 01 2020 at 22:03):

Enrico was the leader of the ParalITP faction

Enrico Tassi (Dec 01 2020 at 22:03):

STM + univpoly + primproj + logic-monad

Pierre-Marie Pédrot (Dec 01 2020 at 22:03):

"Forever thou shalt be punished for the introduction of the STM"

Enrico Tassi (Dec 01 2020 at 22:03):

what else?

Pierre-Marie Pédrot (Dec 01 2020 at 22:03):

univpoly / primproj are in the same package

Cody Roux (Dec 01 2020 at 22:04):

Software Transactional Memory?

Enrico Tassi (Dec 01 2020 at 22:04):

I'm about to replace it with a new thing that does the same but is called differently

Enrico Tassi (Dec 01 2020 at 22:04):

State Transaction Machine

Pierre-Marie Pédrot (Dec 01 2020 at 22:04):

the name has been long forgotten since

Enrico Tassi (Dec 01 2020 at 22:04):

it's a mix (hence the mess) of a document manager and a document-checking manager

Cody Roux (Dec 01 2020 at 22:04):

first hit on google! Nice.

Pierre-Marie Pédrot (Dec 01 2020 at 22:05):

it is but a cursed syntagm that often bars your path in the way to enlightment

Cody Roux (Dec 01 2020 at 22:05):

I remember confusing conversations with Markarius actually.

Pierre-Marie Pédrot (Dec 01 2020 at 22:05):

so yes, merging three major branches in one release is not good for the soundness of your kernel

Enrico Tassi (Dec 01 2020 at 22:06):

Pierre-Marie Pédrot said:

univpoly / primproj are in the same package

that was part of the mess, IMO ;-)

Cody Roux (Dec 01 2020 at 22:06):

ouch

Pierre-Marie Pédrot (Dec 01 2020 at 22:06):

true also

Enrico Tassi (Dec 01 2020 at 22:06):

the compat layer

Pierre-Marie Pédrot (Dec 01 2020 at 22:06):

oh noes

Enrico Tassi (Dec 01 2020 at 22:06):

I'm going to bed now

Pierre-Marie Pédrot (Dec 01 2020 at 22:06):

you'll have nightmares

Pierre-Marie Pédrot (Dec 01 2020 at 22:06):

too late

Cody Roux (Dec 01 2020 at 22:06):

Thanks to both, this was very informative!

Pierre-Marie Pédrot (Dec 01 2020 at 22:07):

the eldritch horrors of side-effects are going to haunt you beyond non-euclidean monadic code

Enrico Tassi (Dec 01 2020 at 22:07):

If you say so ;-)

Enrico Tassi (Dec 01 2020 at 22:07):

let (*) x y = x + y (today, PMP)

Enrico Tassi (Dec 01 2020 at 22:07):

good night

Pierre-Marie Pédrot (Dec 01 2020 at 22:07):

wut. this is perfectly legal.

Pierre-Marie Pédrot (Dec 01 2020 at 22:07):

g'night

Cody Roux (Dec 01 2020 at 22:07):

No really. The only thing it takes is an amateurish experience of trying to implement your own DTT/ITP

Pierre-Marie Pédrot (Dec 01 2020 at 22:09):

proof assistants are very complex objects.

Paolo Giarrusso (Dec 01 2020 at 22:35):

No GC is bad for memory consumption but I don't think it affects speed that much.

Memory consumption should affect speed... Except if you've already given up hope for cache locality.

Paolo Giarrusso (Dec 01 2020 at 22:38):

which seems plausible anyway, ASTs are a nightmare for locality. IIRC this seemed a major pain point for Scala compilers, even with Java’s great GC — probably the lack of value types in JVMs makes locality there even worse than needed.

Cody Roux (Dec 01 2020 at 22:51):

I wonder if Lean's ref counting + reallocate if refcount = 1 and you're creating a cell of the same type helps with this

Paolo Giarrusso (Dec 01 2020 at 23:00):

ah, I was assuming imperative ASTs; purely functional ones are even worse, but destructive updates are slightly less bad

Paolo Giarrusso (Dec 01 2020 at 23:03):

I haven’t done measurements recently, but basically the cache footprint is O(size of written memory) (rounded up, since each write pulls in a whole cacheline — ~16 bytes), so n purely functional updates are likely to have n times the cache footprint of the imperative version, until you trigger a minor GC and start reusing memory.

Paolo Giarrusso (Dec 01 2020 at 23:07):

OTOH, naive refcounting can be a pretty expensive form of GC, especially when done pervasively in a language implementations — it’s even worse as soon as you need atomic refcount operations because you’re running more than one thread. There’s a reason no good virtual machines use refcounting.

Paolo Giarrusso (Dec 01 2020 at 23:08):

but that doesn’t necessarily apply when you’re doing mostly manual memory management with just a bit of refcounting as needed.

Emilio Jesús Gallego Arias (Dec 01 2020 at 23:35):

I'm 100% with Enrico on this discussion, I think Coq's proof engine has several catastrophic performance decisions, the more I have profiled it the more scary it looks, linear memory consumption for each goal! It is hard to do worse! In that sense researchers have an easy job as almost any other approach they use will be faster.

Pierre-Marie, logic programming is a fast implementation of a slow idea. And no doubt techniques they use are _at least_ an order of magnitude faster than what we have.

[I see that simpl appeared in the scary thread, I can sleep now]

Paolo Giarrusso (Dec 02 2020 at 00:51):

Evar implementations is also something that has been studied in isolation...

Paolo Giarrusso (Dec 02 2020 at 00:52):

... and some mature LPs add tabling :-P, even if it's much scarier

Cody Roux (Dec 02 2020 at 02:52):

I'd love to see a bulleted list of the worst offenders in terms of day to day Coq usage. Obviously that might depend on the development, but what makes each goal linear for example?

Pierre-Marie Pédrot (Dec 02 2020 at 08:43):

As I mentioned above, the naive evar implementation has a definite cost but it's not a leading one in day-to-day use. I believe that using an efficient representation for evars wouldn't bring more than a ~15% speedup (educated guess). So it's not neglectible, but it's not a tenfold improvement.

Pierre-Marie Pédrot (Dec 02 2020 at 08:44):

The linearity of goal size is due to the representation of evar instances, which are just the list of its arguments.

Pierre-Marie Pédrot (Dec 02 2020 at 08:44):

This is a stupid representation since for most of those arguments, they will just be the corresponding variable of the context.

Pierre-Marie Pédrot (Dec 02 2020 at 08:44):

Unfortunately one cannot use a compact representation without seriously changing the kernel.

Pierre-Marie Pédrot (Dec 02 2020 at 08:45):

Typical suspects for day-to-day slowness are: 1. universes, 2. hashconsing, 3. a hell of a lot of naive term traversals in unification.

Pierre-Marie Pédrot (Dec 02 2020 at 08:46):

I am working on 1. because it's really a pain and it can probably be alleviated with a bit of engineering (e.g. persistent arrays)

Pierre-Marie Pédrot (Dec 02 2020 at 08:49):

is a real conundrum. We want hashconsing otherwise we get OOM errors, but the typical hashconsing mechanism which is supposed to be amortized O(1) doesn't apply in Coq, because we unmarshall stuff. So, in particular, we do not hashcons on the fly but instead at definite points in the proof (typically at Qed). This is slightly superlinear in the size of the proof, and proofs are big. There was quite a bit of work in that area a few years ago but from all experiments the current tradeoff was the most efficient one in practice.

Pierre-Marie Pédrot (Dec 02 2020 at 08:52):

is linked to an engineering issue / OCaml language limitation. Essentially, we have this one-size-fits-all term AST, but in many cases we would like to have more refined versions of it. A typical usecase would be to store compositional information inside each term node, e.g. whether the considered subterm contains evars. Unfortunately there is no easy way to do that in OCaml (interestingly it's an area where OOP shines), because every type of refined term is different from the standard one so you need either a very heavy machinery or a lot of code duplication. The net result is that we have a lot of quadratic algorithms where we keep recomputing stuff we already have computed for the subterms.

Gaëtan Gilbert (Dec 02 2020 at 09:26):

Pierre-Marie Pédrot said:

I am working on 1. because it's really a pain and it can probably be alleviated with a bit of engineering (e.g. persistent arrays)

how do persistent arrays help universes?

Pierre-Marie Pédrot (Dec 02 2020 at 09:52):

The fact that we have a log n access cost is observable.

Pierre-Marie Pédrot (Dec 02 2020 at 09:52):

amortized O(1) would be better

Pierre-Marie Pédrot (Dec 02 2020 at 09:52):

unfortunately the AcyclicGraph API is a bit ugly, so we have to first simplify it

Janno (Dec 02 2020 at 10:06):

universes

This thread suddenly became very interesting to me! Are there any plans to address the slowness of CClosure with polymorphic constants? I have flamegraphs if people want to see scary stuff. (yay, back on topic!)

Pierre-Marie Pédrot (Dec 02 2020 at 10:10):

Oh, that one is a completely different issue.

Pierre-Marie Pédrot (Dec 02 2020 at 10:11):

Polymorphic universes have so many performance issues that I don't think the secondary ones should be prioritized.

Pierre-Marie Pédrot (Dec 02 2020 at 10:12):

I mean, I won't oppose your PRs, but when universes computation represent ~ 20% runtime of some heavy monomorphic developments, I am afraid I will not spend a lot of time trying to fill a Danaides barrel

Pierre-Marie Pédrot (Dec 02 2020 at 10:12):

My personal take on that is that polymorphic universes have fundamental design issues w.r.t. performance.

Janno (Dec 02 2020 at 10:13):

Ooh, sorry, I assumed you were talking about polymorphic universes.

Janno (Dec 02 2020 at 10:13):

In any case, polymorphic universes easily represent 50% of my runtime :)

Pierre-Marie Pédrot (Dec 02 2020 at 10:13):

Well, polymorphic universes are also affected by slow constraint folding.

Pierre-Marie Pédrot (Dec 02 2020 at 10:13):

Oh, I know. My PhD studend was brave enough to start writing shallow models of CIC in CwF style.

Pierre-Marie Pédrot (Dec 02 2020 at 10:14):

It's a small dev, a few hundred lines.

Pierre-Marie Pédrot (Dec 02 2020 at 10:14):

Very quickly all definitions have hundreds of free universe variables.

Pierre-Marie Pédrot (Dec 02 2020 at 10:14):

And then suddently, a wild Qed appears, which takes 40mn, most of which is due to universe trickery.

Pierre-Marie Pédrot (Dec 02 2020 at 10:15):

It's impressive how easy it it to completely blow up the complexity with univpoly.

Janno (Dec 02 2020 at 10:16):

The trick to get fast Qed is to use the buggy Time Qed which ignores the time taken by universe minimization!

Pierre-Marie Pédrot (Dec 02 2020 at 10:16):

I think that in this case minimization is not culprit, the kernel is really suffering and panting heavily.

Janno (Dec 02 2020 at 10:17):

Ah, then I have no solution to offer :D

Janno (Dec 02 2020 at 10:17):

But I do want to mention that I observe obscene CClosure slowdown even when polymorphic constants have very few universes.

Pierre-Marie Pédrot (Dec 02 2020 at 10:18):

Yeah, it' proportional to the term size, not the number of universes

Pierre-Marie Pédrot (Dec 02 2020 at 10:18):

(as long as nuniv > 0)

Janno (Dec 02 2020 at 10:18):

Right.

Pierre-Marie Pédrot (Dec 02 2020 at 10:19):

I think that one of Beta's PRs could have been tweaked to be more efficient and partially solve your problem.

Pierre-Marie Pédrot (Dec 02 2020 at 10:19):

IIRC Beta closed it because it had a nontrivial cost over monomorphic devs.

Janno (Dec 02 2020 at 10:19):

I think that was https://github.com/coq/coq/pull/8747/, right?

Pierre-Marie Pédrot (Dec 02 2020 at 10:19):

Ah yeah. My bad, it was your PR.

Janno (Dec 02 2020 at 10:19):

I recently asked Josh to help me revive it but I didn't have time to get that started.

Pierre-Marie Pédrot (Dec 02 2020 at 10:20):

Shouldn't be very hard.

Janno (Dec 02 2020 at 10:21):

I have to admit I have no idea what exactly is going on there. The initial implementation was easy enough to understand but then Josh took over and it quickly went over my head.

Pierre-Marie Pédrot (Dec 02 2020 at 10:22):

I happen to be working on substitutions today.

Pierre-Marie Pédrot (Dec 02 2020 at 10:22):

maybe I should try to do the same patch in my variant of substs.

Pierre-Marie Pédrot (Dec 02 2020 at 10:23):

(https://github.com/coq/coq/pull/13537, the revival of a PR I've closed, but I am decided to fix the small slowdowns it incurs)

Janno (Dec 02 2020 at 10:24):

I am rereading the changes in 8747 now and it doesn't seem that scary, actually.

Pierre-Marie Pédrot (Dec 02 2020 at 10:24):

Yeah, I agree.

Matthieu Sozeau (Dec 02 2020 at 10:31):

Regarding 1. universes I think the problem comes from the fact we use a too simplistic universe algebra too. We cannot keep l+1 in universe instances so we always introduce a fresh l' (usually with l+1 <= l') when needed. Each subsequent use of a definition where we used that will generate a fresh universe and constraint, and this will just pile up to give humongous universe instances. If we allow algebraics everywhere we shall need much less fresh universes, actually 0.

Pierre-Marie Pédrot (Dec 02 2020 at 10:33):

I partly subscribe to this thesis.

Pierre-Marie Pédrot (Dec 02 2020 at 10:34):

That is, it is fairly obvious we do generate too many universes.

Pierre-Marie Pédrot (Dec 02 2020 at 10:35):

But I don't believe that introducing algebraics everywhere will be a silver bullet.

Matthieu Sozeau (Dec 02 2020 at 10:35):

Regarding your proposal Janno, I guess it would be relatively easy to make CClosure not substitute universes eagerly by just maintaining a current universe substitution. You never tried that Pierre-Marie?

Pierre-Marie Pédrot (Dec 02 2020 at 10:35):

Isn't that essentially what that PR did?

Matthieu Sozeau (Dec 02 2020 at 10:36):

I don't think it will solve all issues, and inference will be more complicated probably, but it will help

Pierre-Marie Pédrot (Dec 02 2020 at 10:36):

BTW, a common offender for universe generation is setoid_rewrite.

Pierre-Marie Pédrot (Dec 02 2020 at 10:37):

It refreshes the pattern a gazillion times.

Pierre-Marie Pédrot (Dec 02 2020 at 10:37):

I suspect there is actually a bug, since we should be able to share the fresh pattern when it doesn't unify.

Matthieu Sozeau (Dec 02 2020 at 10:37):

Pierre-Marie Pédrot said:

Isn't that essentially what that PR did?

Yep, it seems very similar

Matthieu Sozeau (Dec 02 2020 at 10:39):

Re setoid_rewrite. I though we had an optimization that avoided refreshing unless necessary (e.g when going under binders, and even that could be optimized by "weakening" the evars in the pattern)

Enrico Tassi (Dec 02 2020 at 10:39):

Pierre-Marie Pédrot said:

As I mentioned above, the naive evar implementation has a definite cost but it's not a leading one in day-to-day use. I believe that using an efficient representation for evars wouldn't bring more than a ~15% speedup (educated guess). So it's not neglectible, but it's not a tenfold improvement.

To me a "decent" representation of evars includes the fact that the "heap" would be garbage collected.
As we know, today the evarmap is not garbage collected, and at the end of the proof is contains the entire history of the proof building process.
Of course, not having a GC is not a problem if you have enough memory and if you never traverse it. Both assumption are false, since we have users hitting the 64G limit (of normal machines) and the ocaml GC is going to traverse (for nothing) this huge heap from time to time.

As I said elpi was coded like that a long time ago. Doing list reversal was, IIRC, 22000x slower than ocaml. By "manually" adding instruction to remove from the heap useless cells, it went to 1000x slower IIRC. Of course in elpi everything is an evar, in Coq you do other stuff as well. But using less memory is also making your (ocaml) code much faster.

I would try to use weak pointers in the evar map. I don't know if ocaml can handle so many of them, but at least we would get a figure. with "imperative" evars, one would not need weak pointers, but this change is much harder to do and get figures about.

Pierre-Marie Pédrot (Dec 02 2020 at 10:41):

@Enrico Tassi evar maps do not only contain evars, universes are I believe more often than not a huge memory leak.

Pierre-Marie Pédrot (Dec 02 2020 at 10:41):

I was profiling memory consumption of Require recently and realized that a good chunk of the allocated memory in perennial came from universe naming.

Pierre-Marie Pédrot (Dec 02 2020 at 10:42):

Like, we want to give fancy names for universes, and actually 99% of our users don't give a shit, but for them it will still be a few hundreds of MB

Enrico Tassi (Dec 02 2020 at 10:43):

For universes, I have a different dream. A -type-upto 3 flag which keeps at most 3 non-floating universes in the graph and collapses all floating one the these 3 after each type inference.

Pierre-Marie Pédrot (Dec 02 2020 at 10:43):

640k should be enough for anybody?

Enrico Tassi (Dec 02 2020 at 10:43):

I boldly claim 90% of computer scientists and 80% of mathematicians would be happy with that.

Pierre-Marie Pédrot (Dec 02 2020 at 10:44):

The problem with that is that you will probably make eager choices wrongly, even for 99% of users.

Enrico Tassi (Dec 02 2020 at 10:44):

Also 3 is a nice number ;-)

Enrico Tassi (Dec 02 2020 at 10:44):

I'm not so sure. 99% of the times you mean Type0

Pierre-Marie Pédrot (Dec 02 2020 at 10:45):

I'd be interested in such an experiment.

Pierre-Marie Pédrot (Dec 02 2020 at 10:45):

But we would probably realize some horrible problem midway.

Matthieu Sozeau (Dec 02 2020 at 10:46):

Practice should tell, but if we have algebraics everywhere, maybe a lot of people would be content to use Set, Set+1 and Set+2 directly

Enrico Tassi (Dec 02 2020 at 10:46):

At some point @Assia Mahboubi did it with math comp (a long time ago) by replacing all Type with MyType from Definition MyType := Type. IIRC she needed 3 MyType.

Théo Zimmermann (Dec 02 2020 at 10:46):

Matthieu Sozeau said:

Practice should tell, but if we have algebraics everywhere, maybe a lot of people would be content to use Set, Set+1 and Set+2 directly

It would certainly be useful in the doc.

Théo Zimmermann (Dec 02 2020 at 10:47):

Also, if Set is really Type_0, it would be nice to have a way to check for this explicitly in Coq.

Pierre-Marie Pédrot (Dec 02 2020 at 10:47):

@Matthieu Sozeau what are you waiting for? That's more useful that induction-recursion, which will be used by Agda fanboys to prove the termination of simply-typed λ-calculus for the 4591460th time.

Matthieu Sozeau (Dec 02 2020 at 10:48):

Well, I need help with the Bender & al algorithm :)

Enrico Tassi (Dec 02 2020 at 10:49):

For the -type-upto 3 thing, I think any algorithm would be efficient enough ;-)

Gaëtan Gilbert (Dec 02 2020 at 10:49):

Théo Zimmermann said:

Also, if Set is really Type_0, it would be nice to have a way to check for this explicitly in Coq.

What do you mean?

Matthieu Sozeau (Dec 02 2020 at 10:49):

Note that in the case of Set, Set+1 and Set+2, we don't even need to check the graph most of the time

Enrico Tassi (Dec 02 2020 at 10:49):

For the algebraic case... well, not so easy I'm afraid. (I mean with succ and max freely mixed)

Pierre-Marie Pédrot (Dec 02 2020 at 10:50):

@Enrico Tassi but probably better in the long run

Matthieu Sozeau (Dec 02 2020 at 10:51):

@Enrico Tassi I'm wondering how you could decide if you have x < y what you should assign to x and y.

Pierre-Marie Pédrot (Dec 02 2020 at 10:51):

X := Type0, Y := Type1

Enrico Tassi (Dec 02 2020 at 10:52):

yeah!

Matthieu Sozeau (Dec 02 2020 at 10:52):

So kind of "minimal" solutions?

Pierre-Marie Pédrot (Dec 02 2020 at 10:52):

Actually, I believe that we should have a more principled approach for UGraph where this would be easy to perform.

Pierre-Marie Pédrot (Dec 02 2020 at 10:53):

Currently we have this hacky type-in-type stuff.

Pierre-Marie Pédrot (Dec 02 2020 at 10:53):

If we could use various implementation of the graph, it could be easy to switch from them.

Pierre-Marie Pédrot (Dec 02 2020 at 10:53):

There is no conceptual difference between a graph algorithm that collapses everybody on one point, and one that collapses only le nodes.

Matthieu Sozeau (Dec 02 2020 at 10:55):

For me with type-in-type we should not consult the graph at all. But yes we can also interpret < and <= as = to model the same thing

Enrico Tassi (Dec 02 2020 at 10:55):

I have the impression that in such a mode one could live with Set=type0, Type=type1, U=type2 (I mean, even be explicit in the concrete syntax).
For _ one can still delay the choice, but it seems hard to believe that one gets many i < j for i and j not related to one of the 3 named universes.

Gaëtan Gilbert (Dec 02 2020 at 10:55):

if we have algebraics in instances we can also implement non cumulative mode

Matthieu Sozeau (Dec 02 2020 at 10:56):

@Gaëtan Gilbert yes, indeed that's one nice benefit.

Pierre-Marie Pédrot (Dec 02 2020 at 10:56):

Down with Cumulativity! Let's turn Coq into Agda!

Enrico Tassi (Dec 02 2020 at 10:56):

Haskell!

Matthieu Sozeau (Dec 02 2020 at 10:57):

@Enrico Tassi indeed in many cases they will be related

Enrico Tassi (Dec 02 2020 at 10:58):

That is my intuition, but I understand that "it works for 3" is not very satisfactory, intellectually speaking...

Assia Mahboubi (Dec 02 2020 at 11:00):

Enrico Tassi said:

At some point Assia Mahboubi did it with math comp (a long time ago) by replacing all Type with MyType from Definition MyType := Type. IIRC she needed 3 MyType.

Indeed. Disclaimer: it was a long time ago and mathcomp was way skinnier at the time.

Matthieu Sozeau (Dec 02 2020 at 11:01):

That's still some good evidence!

Assia Mahboubi (Dec 02 2020 at 11:02):

Enrico Tassi said:

That is my intuition, but I understand that "it works for 3" is not very satisfactory, intellectually speaking...

It is a common situation in computer algebra systems to implement a portfolio of algorithms for a same task (e.g. for multiplying matrices or polynomials), each of which being better for a different class of inputs, due to the size of the constants hidden in big O....

Gaëtan Gilbert (Dec 02 2020 at 11:04):

we have Print Sorted Universes to tell use how many are needed btw, no need for hand replacing Type with MyType

Assia Mahboubi (Dec 02 2020 at 11:06):

This idea was to measure the gain in performance. It was much faster with explicit definitions.

Gaëtan Gilbert (Dec 02 2020 at 11:06):

Enrico Tassi (Dec 02 2020 at 11:10):

Are you saying that we test that the stdlib works with 3 universes?

Pierre-Marie Pédrot (Dec 02 2020 at 11:12):

@Enrico Tassi yes.

Pierre-Marie Pédrot (Dec 02 2020 at 11:12):

I think it's 5 currently, but that's the idea.

Pierre-Marie Pédrot (Dec 02 2020 at 11:12):

Actually 4.

Pierre-Marie Pédrot (Dec 02 2020 at 11:13):

see test-suite/misc/universes.sh

Pierre-Marie Pédrot (Dec 02 2020 at 11:13):

@Gaëtan Gilbert speaking of which, I am currently extruding universe sorting / printing from AcyclicGraph / UGraph, are you fine with that?

Gaëtan Gilbert (Dec 02 2020 at 11:14):

depends how the code looks
but why?

Pierre-Marie Pédrot (Dec 02 2020 at 11:14):

This stuff has nothing to do in the kernel (and it's the sole user of safe_repr :/)

Pierre-Marie Pédrot (Dec 02 2020 at 11:14):

I want to replace the implementation of Point, and it's a mess.

Pierre-Marie Pédrot (Dec 02 2020 at 11:14):

sort is a big hack, to start with.

Pierre-Marie Pédrot (Dec 02 2020 at 11:14):

Instead, I will just dump the graph and print that in vernac.

Enrico Tassi (Dec 02 2020 at 11:15):

if Hurkens needs 4 to prove false, then limiting to 3 universes is also about soundness ;-)

Pierre-Marie Pédrot (Dec 02 2020 at 11:15):

@Enrico Tassi You, sir, are a genius.

Emilio Jesús Gallego Arias (Dec 02 2020 at 16:46):

I'm afraid @Pierre-Marie Pédrot I cannot share your analysis and much less the 15% number you come with, I think Enrico gave numbers more close to the actual evidence people have. Current engine just is not in the same class of perf than other proof search systems.

By linear, I didn't mean that memory consumption per-goal is linear, which is, but it is also linear on the number of evars ever created. That's just scary. We have discussed many times about the proof engine, and I'm still to be convinced about the defenses of many things, including the high-level design where refine is not a part of the primitives.

Enrico Tassi (Dec 02 2020 at 16:51):

@Pierre-Marie Pédrot can we try to replace the IntMap in the evd with https://caml.inria.fr/pub/docs/manual-ocaml/libref/Ephemeron.GenHashTable.html (plus a call to nf_evar on the initial evar, say, every 1K evar allocations, or every end of run of the tactic monad)?

Pierre-Marie Pédrot (Dec 02 2020 at 16:52):

You'll probably get evars reclaimed to eagerly, but, yes, please try.

Pierre-Marie Pédrot (Dec 02 2020 at 16:53):

Also, weak cells / ephemerons are far from being free.

Enrico Tassi (Dec 02 2020 at 16:54):

I'm too busy with the release, but maybe someone at the CUWD would like to play with this

Emilio Jesús Gallego Arias (Dec 02 2020 at 16:58):

I try something like that but I never managed it to work, even after adding a copy [keep in mind that evar_maps are purely functional whereas hash may not]

But indeed we have some other problems like the imperative evar_counter, that's a mess once we try ocaml-multicore

Emilio Jesús Gallego Arias (Dec 02 2020 at 16:58):

Not even equality of evars in two evar maps is properly defined if we want to assume some separation rules.

Emilio Jesús Gallego Arias (Dec 02 2020 at 16:59):

Imagine how fast will be Coq + multicore be when each evar creation does introduce a global lock :S

Pierre-Marie Pédrot (Dec 02 2020 at 16:59):

But let me repeat something: universes are a worse hotspot than that.

Emilio Jesús Gallego Arias (Dec 02 2020 at 16:59):

Not so sure in view of @Jason Gross results

Emilio Jesús Gallego Arias (Dec 02 2020 at 16:59):

how can you measure that

Pierre-Marie Pédrot (Dec 02 2020 at 16:59):

This has nothing to do with the imperative representation of evars.

Emilio Jesús Gallego Arias (Dec 02 2020 at 16:59):

the kind of slowdown we are talking about is hard to measure, because it is intrinsic

Pierre-Marie Pédrot (Dec 02 2020 at 17:00):

It's linked to the representation of instance, which is not related.

Emilio Jesús Gallego Arias (Dec 02 2020 at 17:00):

we are not just disucssing "imperative representation of evars"

Emilio Jesús Gallego Arias (Dec 02 2020 at 17:00):

that alone does little

Pierre-Marie Pédrot (Dec 02 2020 at 17:00):

I have no idea what you want to implement then, because I don't see how you're gonna gain anything with it.

Emilio Jesús Gallego Arias (Dec 02 2020 at 17:01):

we are talking about the whole design of the proof search engine, you can have an imperative representation and perform worse than the current evar_map , some advanced tricks are needed to make it fast

Pierre-Marie Pédrot (Dec 02 2020 at 17:01):

Evar creation is already linear in the size of the instance.

Pierre-Marie Pédrot (Dec 02 2020 at 17:01):

Anyways, I prefer rebasing my branch than vacuously trolling, so have fun.

Emilio Jesús Gallego Arias (Dec 02 2020 at 17:01):

for example, I'm convinced that evar == goal is not the right notion; I'm just repeating the discussion

Pierre-Marie Pédrot (Dec 02 2020 at 17:01):

But don't expect even a 2x speedup, however fast your evar will be.

Emilio Jesús Gallego Arias (Dec 02 2020 at 17:02):

we had some time ago

Emilio Jesús Gallego Arias (Dec 02 2020 at 17:02):

instantiating a unification variable is a totally different concept than solving a goal

Emilio Jesús Gallego Arias (Dec 02 2020 at 17:02):

and indeed the engine does not provide operations for neither

Emilio Jesús Gallego Arias (Dec 02 2020 at 17:02):

engine I mean the proofview

Emilio Jesús Gallego Arias (Dec 02 2020 at 17:03):

I'm not trolling by the way as I'm dead serious

Pierre-Marie Pédrot (Dec 02 2020 at 17:03):

I am waiting for your PR.

Emilio Jesús Gallego Arias (Dec 02 2020 at 17:03):

I wish I had the time to back my claims with code

Emilio Jesús Gallego Arias (Dec 02 2020 at 17:03):

I don't say this is a small project

Emilio Jesús Gallego Arias (Dec 02 2020 at 17:04):

I am already busy trying to have coqc not to recheck the same stuff over and over again when a user changes a line :)

Emilio Jesús Gallego Arias (Dec 02 2020 at 17:04):

which is like 2 order of magnitude less ambitious but very tricky still

Pierre-Marie Pédrot (Dec 02 2020 at 17:05):

I would kindly recommend getting rid of the STM if you want to stop having a gaping memory leak in coqc, btw.

Matthieu Sozeau (Dec 02 2020 at 17:21):

Re. the representation of evars: even if we made evar "closed" i.e. of closed type (forall ctx, ty), I don't see how that would help in any way with the issue of evar instance representation, rather the other way around: it would make it harder to have compact representations for instances unless we go to fully represent explicit substitutions in terms. However that experiment (using explicit substitutions pervasively) was tried and failed in both Coq and Matita IIRC.

Jason Gross (Dec 02 2020 at 18:14):

I was under the impression that the bulk of the performance issue in the rewrite variants was allocating evars every time there's a head constant match or something like that, and so there's this pervasive issue where rewriting gets slower the more lemmas being used to rewrite. Is this not the case? (Btw, if it's helpful, I can open an issue with the "runs out of RAM and is way too slow" example from my defense)

Clément Pit-Claudel (Dec 04 2020 at 16:22):

In past projects I used something like this:

type 'a ast =
  | X of 'a node
  | …
and 'a node := { annot: 'a; data: 'a ast }

Then most of the code operates on 'a ASTs and there's a function reset_annots: 'a AST -> 'b -> 'b AST that you use before doing a transformation. This works well for turning quadratic operations on the AST into linear, but you don't get incremental updates of the metadata when you make changes to the AST (you have to reset all metadata before each pass). @Pierre-Marie Pédrot have you considered something along these lines?

Emilio Jesús Gallego Arias (Dec 04 2020 at 16:25):

Note that this is already implemented in Coq, see lib/cAst.mli

Clément Pit-Claudel (Dec 04 2020 at 23:20):

Ah, super. Then I didn't understand PMP's point about quadratic blow-up

Pierre-Marie Pédrot (Dec 05 2020 at 11:51):

@Clément Pit-Claudel that's not what the kernel uses. And even if we wanted to use this structure, it'd be an engineering nightmare. It'd require a serious rewriting of Coq, we'd pay non-trivial overheads all over the place, and it's quite dubious from a trust point of view that you can maintain meaningful invariants there.

Pierre-Marie Pédrot (Dec 05 2020 at 11:51):

CAst is only used for syntactic data the user inputs, FTR.

Emilio Jesús Gallego Arias (Dec 06 2020 at 12:12):

Oh indeed I was talking about the AST part, kernel terms are a different story.

Emilio Jesús Gallego Arias (Dec 06 2020 at 12:12):

But I think in most cases you are dealing with ASTs

Last updated: Apr 19 2024 at 17:02 UTC