Karl Palmskog (Oct 06 2023 at 20:28): 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.
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.
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.
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
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: Oct 13 2024 at 01:02 UTC