Jason Gross

The logs seem to indicate that coqc fails to flush the glob file before quitting, and that this, combined with not uploading _build_ci *and* the fact that HoTT does not...

Oh, I see, this is because we pull globs from passing Coq rather than failing Coq.

Let's try again now that https://github.com/JasonGross/coq-tools/pull/298 has been merged. @coqbot ci minimize ci-hott ci-color

The CI job that is timing out is the one that builds only .v files. There is [a separate one for making sure the extracted OCaml code compiles](https://github.com/coq/coq/blob/82e064be93905101eb56a8de85072884b37f0368/dev/ci/ci-fiat_crypto_ocaml.sh#L16) which builds...

> * can ExtractionOCaml not be a part of this target? I would like to keep this, because not many developments test Extraction. (And plausibly we should ask the Coq...

> This pull request introduces a new kind of accumulator that discards its arguments. This is great! I've wanted something like this (although more general than the VM, I've wanted...

> You always call `vm_compute` on a goal, which is a type, almost always axiomatic or inductive, hence open. Ah, right. I think the actual confusion on my end, though,...

> And you cannot even replace the calls to `vm_compute` by something else, because the constants involved are "basically transparent but considered opaque for reduction", as Coq says Can we...

> @Janno pointed out we have code normalizing AVL trees, and those embed Qed-opaque proofs. What then? If there is some small fixed set of Qed-opaque proofs, we can just...

> Since it chokes, I suppose a `Qed`ed constant plays the role of the fresh name, but it is not obvious from the code. Is `abstract` used under the hood?