Lucie Lahaye

I'm unsure as to what's the cause of this, sorry. For instance, consider the following: ```coq Definition identity (b: bool) : bool := b. Inductive Test1 : bool -> Prop...

Redefining `forAllShrinkNonDet` as follows solves the issue (but the performance is awful - it's not a satisfying fix): ```coq Definition forAllShrinkNonDet {A prop : Type} {_ : Checkable prop} `{Show...

Another possible solution would be to write an action that a) generates a Actions workflow file with the arbitrary job tree we want, b) commits it _somewhere_ to trigger it...

I was able to get something working using a Personal Access Token: https://github.com/lweqx/ci-dynamic-job-tree In this example I generate a random tree of job dependencies. Example run: https://github.com/lweqx/ci-dynamic-job-tree/actions/runs/17863682429. It adds a...

> Another option to test reverse dependencies is to use the Coq Nix Toolbox, in which case, the list of packages to test is still auto-generated, but it can be...