Jason Gross
Jason Gross
[The documentation](https://agda.readthedocs.io/en/v2.6.2.2/language/mixfix-operators.html) does not specify the precedence of function application. It seems based on my experiments below that application binds more tightly than any possible infix, and that applications involving...
Can anyone reproduce the (seemingly consistent?) issue that `make -j2` fails on Mac OS the first time it's run after a clean checkout? c.f. https://github.com/mit-plv/fiat-crypto/pull/1458 _Originally posted by @JasonGross in...
It would be nice to get all files to under 2 GB so that Coq's CI could build with -j2. As of 637c7cec3a2ab18edb6e52b0c15a3797d195c7ee the most memory-hungry files are: ``` Time...
> It's worth noting that native_compute performs significantly worse than OCaml HOAS, though the two should be similar; probably native_compute does not use flambda optimization options at all. Indeed, the...
Kernel conversion uses something akin to `lazy`. The fastest normalization is probably `vm_compute`, unless you are starting from very small terms and ending up with very small terms, but have...
According to https://github.com/coq/coq/issues/11277, the right way to tweak Coq's GC is to use the environment variable `OCAMLRUNPARAM` (see https://caml.inria.fr/pub/docs/manual-ocaml/runtime.html). You can also tweak Coq's stack limits via `ulimit -S -s`,...
> We use this because I was not able to find a good direct way in Coq to force normalization of large Church trees, because `Eval compute` will attempt to...