Stream: Nix toolbox devs & users

Topic: Breakage after Coq website migration


view this post on Zulip Karl Palmskog (Oct 06 2023 at 20:28):

I get the following error in CI:

Run nix-build https://coq.inria.fr/nix/toolbox --argstr job buchberger --arg override '{ coq = "master"; buchberger = builtins.filterSource (path: _: baseNameOf path != ".git") ./.; }'
error: unable to download 'https://coq.inria.fr/nix/toolbox': HTTP error 404

Can this be fixed by adding some forward? Or is something else needed? Example of failing job.

view this post on Zulip Théo Zimmermann (Oct 07 2023 at 14:24):

Oh indeed, this was a redirection in the Apache config. Unfortunately, with the new GitHub Pages setting we can only do HTTP redirections, and I'm not sure that this will be sufficient to fix this issue.

view this post on Zulip Théo Zimmermann (Oct 07 2023 at 14:26):

What we could do though, would be to create a nix repository in the Coq organization with a gh-pages deployment of the toolbox under /toolbox.

view this post on Zulip Karl Palmskog (Oct 07 2023 at 14:27):

how about using our regular top-level domain/repo for this? coq-community.github.io/nix becomes coq-community.org/nix

Or I guess a nix repo would automatically get that domain, maybe better

view this post on Zulip Théo Zimmermann (Oct 07 2023 at 14:29):

Or I guess a nix repo would automatically get that domain, maybe better

Indeed. And for something which is just a deployment, I prefer that this is not mixed with manually maintained code (so a similar setup to doc)


Last updated: May 25 2024 at 19:02 UTC