Guillaume Melquiond

@coqbot run full ci

The thing is, the size of the bytecode is directly proportional to the size of the term, since there is no optimization such as inlining. So, to get 2 million...

Right, this had eluded me. Just to be sure, I suppose you are talking about a term of the form `fun H1 H2 ... Hn H => H1 (fun x1...

Since #18964 did not reduce the size of the generated bytecode of `coq-hott`, I went and actually read it. Closures have nothing to do with the size of bytecode. The...

Actually, my mistake, these are the numbers before the end of the section. This example gets even worse once the section is closed, since there are now 15 instances, with...

I am unable to reproduce the marshal failure on `output/Partac.v` (https://gitlab.inria.fr/coq/coq/-/jobs/4266038) with 4.14.1+flambda. Could someone with CI rights relaunch the job? Just to know if there is some actual issue...

So, cosmic ray it was.

There are still large gains all over the place: ``` coq-fiat-parsers/./src/Parsers/Refinement/SharpenedJSON.vo 20078292 6619979 -13458313 -67% coq-fiat-crypto-with-bedrock/./src/Assembly/Syntax.vo 13628376 5302455 -8325921 -61% coq-fiat-parsers/./src/Parsers/BooleanRecognizerOptimized.vo 8141817 2818502 -5323315 -65% coq-category-theory/./Instance/Coq/Par.vo 8199834 3600449 -4599385 -56%...

It seems like a non-negligible number of opaque universe constraints comes from the use of `rewrite`. Perhaps forcing the universe of `eq_ind_r` to be identical to the one of `eq`...

Just to be sure I understand. On the following code ```coq Definition comma {A B C} (f : A -> B) (g : B -> C) := fun x =>...