Jan-Oliver Kaiser

Results 22 issues of 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...

kind: enhancement
needs: changelog entry
needs: test-suite update
needs: full CI

### 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...

kind: regression
part: primitive records
kind: bug

### 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...

part: universes
part: unification
kind: bug

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...

part: coercions
kind: bug

See https://github.com/ocaml/opam/issues/3435 for more details about this 6 year old bug.

needs: full CI

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...

kind: bug
needs: triage

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...

enhancement
core