Stream: Hydras & Co. universe

Topic: Good riddance to binders in index


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jan 03 2023 at 13:51):

What Coq version should I switch to? 8.16? 8.17? master?

view this post on Zulip 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: May 24 2024 at 23:01 UTC