Karl Palmskog (Jan 02 2023 at 14:08): Karl Palmskog (Jan 02 2023 at 14:08):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.
Pierre Castéran (Jan 02 2023 at 16:52):After the last push (10 minutes ago), there are still 20463 entries of type "binder". Perhaps I didn't understand what to do.
Karl Palmskog (Jan 02 2023 at 16:57):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
Karl Palmskog (Jan 02 2023 at 16:58):at worst, the binder index should go away in the next few days if the caching is to blame
Karl Palmskog (Jan 02 2023 at 17:01):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...
Karl Palmskog (Jan 02 2023 at 17:01):it may be a remnant from when SerAPI was not compatible with master (it's in Coq's CI now)
Théo Zimmermann (Jan 03 2023 at 13:50):Indeed, the Nix CI jobs are still on Coq 8.14. The reason for this was that it included goedel I think.
Théo Zimmermann (Jan 03 2023 at 13:51):What Coq version should I switch to? 8.16? 8.17? master?
Karl Palmskog (Jan 03 2023 at 14:08):@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