Since https://github.com/coq/coq/pull/17045 was just merged, our HTML deployment will finally be lean again. It looks like 20463*2 entries will disappear from the index after the next hydra-battles master commit.
After the last push (10 minutes ago), there are still 20463 entries of type "binder". Perhaps I didn't understand what to do.
hmm, maybe the runner that builds the coqdoc is using an old Nix-cached Coq. I can't see in the CI job which revision of Coq it's using: https://github.com/coq-community/hydra-battles/actions/runs/3823847507/jobs/6505507769
at worst, the binder index should go away in the next few days if the caching is to blame
on the other hand, maybe the
build-doc job actually uses an ancient version of Coq (I see references to Coq 8.14 in output). Then we'll have to ask @Théo Zimmermann to switch to use Coq master...
it may be a remnant from when SerAPI was not compatible with master (it's in Coq's CI now)
Indeed, the Nix CI jobs are still on Coq 8.14. The reason for this was that it included goedel I think.
What Coq version should I switch to? 8.16? 8.17? master?
@Théo Zimmermann I think we should use
master to immediately get coqdoc and other improvements. I also hope Alectryon is adopted in Coq itself at some point.
Last updated: Jun 11 2023 at 00:30 UTC