Jason Gross

We still need `-emacs`. But once https://github.com/JasonGross/coq-tools/pull/126 and https://github.com/coq-community/run-coq-bug-minimizer/pull/18 are merged, the minimizer will try splitting statements with both versions of coqtop, so we won't need the simple compiler to...

It looks like coqbot encountered a separate anomaly in the middle of minimizing (perhaps the log is enough to recreate it? if not, once the minimizer is finished, you can...

Resumption failed because ``` git checkout 4a9b926e4283e50bf6e5d95b6d747854986833a5 fatal: reference is not a tree: 4a9b926e4283e50bf6e5d95b6d747854986833a5 ``` And unfortunately the example is just a bit too long to resume minimization by comment

Let's just ask again @coqbot ci minimize ci-metacoq

MetaCoq inlining failure due to https://github.com/JasonGross/coq-tools/issues/129. I can work around it for MetaCoq, but in general this is hitting the problem that there's no way to create a module named...

Should the example from metacoq be added to the test-suite (is there a way to make an example that does not depend on Equations?) (Also, btw, minimization of metacoq should...

I can think of two ways to resolve this issue. 1. Replace the primitive Boolean equality operator at https://github.com/coq/coq/blob/147f4da1beee028be550f098401398f5822af78e/theories/Numbers/Cyclic/Int63/PrimInt63.v#L79 with something of type `forall x y, option (x = y)`....

> having an additional opcode of type `forall x y:int, option (x = y)` makes sense to me, assuming it is sufficient. This should be sufficient for defining the wrappers,...

> > > having an additional opcode of type `forall x y:int, option (x = y)` makes sense to me, assuming it is sufficient. > > > > > >...

This is still an issue, and still quite annoying.