Jason Gross

Still failing at https://github.com/JasonGross/test/actions/runs/13686640123/job/38271477628

Trying that out at https://github.com/JasonGross/test/actions/runs/13693808963/job/38291718192

> Can you execute it by doing the following? > > ``` > opam exec -- bash ./test.sh > ``` Yes, this variant works fine

Indeed, this is a defect that results from wanting to avoid recompiling the entire project on every change to every file. However, we should probably add a flag `--keep-transitive-dependencies` (or...

Yes, this should work. For 1, there is already code in the bug minimizer that adds all transitive `Require`s to the top of the file. Probably we want a slightly...

Some incomplete notes if you (or anyone else) wants to implement this: I believe the first steps are: 1. Add a `--add-transitive-requires-before-minimizing` flag to gate this behavior 2. Add a...

This was caused by having autocompletions enabled in settings, disabling them fixes the issue

I've fixed compatibility with Coq 8.9, let me look at quickcheck

The issue with QuickChick seems to be a bug in Coq's legacy (`apply`) unification, I'm currently minimizing it.

The issue with QuickCheck is https://github.com/coq/coq/issues/17566. I'm not sure what we should do here, options I see are: 1. Remove `Opaque ret` 2. Fully instantiate the lemma being `apply`d 3....