Jan-Oliver Kaiser
Jan-Oliver Kaiser
## Desired Behavior It seems dune currently schedules the easiest-to-get-to files first. I would like to have a depth first mode that assumes the longest chain is also the costliest...
Classes with unique instances are forbidden from changing their chosen answer when other goals make progress. Classes with strict resolution cannot contribute to other classes progress since they are forbidden...
### Description of the problem This is an unforeseen consequence of #18373, I think. If I am right, it highlights a flaw in the attempt to decouple the concept and...
### Description of the problem The example below fails at Qed time instead of during unification. Using `apply eq_refl` does not help. It's not clear to me at all that...
Currently, make is called with `-j`, which will spawn as many jobs as there are parallel targets at any given time. On systems with (only) 4 CPUs, this leads to...
### Description of the problem The code below (minimized from a real example) sets up a fully opaque database and registers hints on terms involving reverse coercions. In 8.16 and...
See https://github.com/ocaml/opam/issues/3435 for more details about this 6 year old bug.
This introduces `kred` (short for "kernel reduction", not to be confused with kernel reduction [no quotes]). The name needs some workshopping. But it is descriptive in the sense that `kred`...
### Description of the problem _No response_ ### Small Coq file to reproduce the bug ```coq #[projections(primitive=yes)] Class Lens (a b c d : Type) : Type := { view...
The example below does not seem to terminate. Removing either of the three quantified assertions makes z3 terminate, though it still takes several seconds (with some variation depending on which...