Dear Nixers,
I'm currently trying to add a project (ssprove) to the Nix CI that is not yet in nixpkgs
.
So I did all the necessary steps:
Now I would like to test the bundles that I defined for the CI to make sure they are working correctly without initiating the whole coq-nix-ci.
So I added the workflow_dispatch:
options to the generated Github actions, such that I can start them manually in the ssprove repository.
Yet the setup of the build environment does not work. The build cannot find the dependencies such as mathcomp
.
Why is that the case?
My assumption is that the jobs load a certain version of the ssprove repository. And hence whether ssprove
is already available in nixpkgs
or not does not really matter.
However, if that is the case then how does the CI job know the (propagated)buildInputs
?
I cannot yet see where it drags that information from the existing nixpkgs
such that I can force it to look at my fork of nixpkgs
.
Also, in the config.nix
script, there is a buildInputs
attribute. But I'm not sure how to use it, when and why? It might have to do with my problem but if I would write my dependencies there then how would that look like?
Simply writing buildInputs = [ mathcomp ]
just does not work.
Any help on this would be very much appreciated.
@Cyril Cohen and @Théo Zimmermann , if one of you finds the time to have a quick look at this question, I would really appreciate that.
Thanks,
Sebastian.
Dear @Sebastian Ertel. Sorry for taking such a long time to answer. I just had a look and I could not find a local overlay to describe ssprove
derivation nor could I find a pointer to a nixpkgs branch which contains it.
nix-shell --arg do-nothing true --run "createOverlay ssprove"
to create a fresh overlay file for you to use. (Ultimately this is the kind of command that could be handled by a flakes "app", note there is also a variant to fetch an existing derivation from nixpkgs and create a overlay starting from it)..nix/coq-overlays/ssprove
derivation to include the dependencies you need.Cf https://github.com/sertel/ssprove/pull/1 for the result
cannot yet see where it drags that information from the existing nixpkgs such that I can force it to look at my fork of nixpkgs.
Above, I showed how to implement the overlay method, but I understand that what you wished was to point towards your own nixpkgs branch. To do that you need to use another command:
nix-shell --arg do-nothing true --run "updateNixpkgs sertel ssprove"
to pin a particular version of nixpkgs (this is what must ultimately be replaced by a flakes lock)Cf https://github.com/sertel/ssprove/pull/2 for the result
Also, in the
config.nix
script, there is abuildInputs
attribute. But I'm not sure how to use it, when and why? It might have to do with my problem but if I would write my dependencies there then how would that look like?
Simply writingbuildInputs = [ mathcomp ]
just does not work.
This is a fallback for the lazy who just want a working setup for a very small cost (not overlay, no fork of nixpkgs, etc), and it un-intuitively expect strings that reflect the names of the coqPackages attribute. I believe this is very bad practice and should be removed asap in favor of a better tool to generate the overlay.
Hi @Cyril Cohen ,
thanks a lot for your answer and the PRs.
I still have the problem that I cannot run the the bundles locally in the same way that the NIX-CI does it. At least that is what it seems in your second PR.
The 8.17-job is failing because even though it gets the derivation now from the proper nixpkgs
repo, it does not checkout the according version (v0.1.0 in this case). It tries to build the current version of sertel/ssprove
against Coq 8.17 which of course fails.
The problem is now that only the current version actually has the explicit nixpkgs
configuration from your PR. Even if it would checkout the proper earlier version, it would still ask the wrong nixpkgs
repo.
Of course, once I pushed this into nixpkgs
things should work and I do not need that workaround anymore. But at this point I cannot actually be sure whether the bundles I configured are actually working properly. I also do not know whether my switch statement in the derivation is actually working properly.
Is there a way to work around this issue other than starting the PR on the nixpkgs
repo?
This CI is meant to use the checked out version of the project. If you really wish to test version 0.1.0 instead you can override it in a nix config file, but that wouldn't be consistent against the dev version. If you want to test released versions ssrprove, we recommend you push a draft pr to the coq-nix-toolbox instead. It should pin your own forked branch of nixpkgs. Thanks to caching it won't actually recompile anything else than ssprove, and when successful one can 1. Merge your nixpkgs pr 2. Update the draft toolbox pr to use the nixpkgs master again, undraft and merge.
Of course you can always test locally to your computer builds of released packages through the nix-build -A
command in your nixpkgs workdir
Finally you can use the coq nix-toolbox to setup a full CI testing whichever versions of whatever... But I'd advise you do it in a separate repo... But that requires maintenance for now... I wish one day we have GitHub hooks to try to auto upgrade versions of this and that and ping us if it works.
Ok, I will do that then, thanks!
Indeed I just wanted to understand whether one can just reuse the CI jobs for a repo-local CI instead of writing yet another CI job that does not run in the Coq-Nix-CI.
But I bet I can setup something generic such that repo owners can always run their latest configuration as the repo-local CI.
Oh I see now.
All the CI jobs are actually repo-local to coq-nix-toolbox
. I had completely spaced on that. Sorry.
I'm again stuck.
I opened a PR.
But when trying to create the Github actions with nix-shell --arg do-nothing true --run "updateNixpkgs sertel ssprove"
I get the following error:
warning: found empty hash, assuming 'sha256-AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA='
error:
… while evaluating a branch condition
at /Users/sebastianertel/sandbox/coq-nix-toolbox/default.nix:133:1:
132| in
133| if !isDerivation nix-auto then nix-auto
| ^
134| else nix-auto.overrideAttrs (o: {
… in the argument of the not operator
at «none»:0: (source not available)
(stack trace truncated; use '--show-trace' to show the full trace)
error: unable to download 'https://github.com/sertel/nixpkgs/archive/.tar.gz': HTTP error 404
response body:
Not Found
What am I doing wrong again?
I sse no sprove
branch on your fork of coq-nix-toolbox: https://github.com/sertel/coq-nix-toolbox
(if that's the issue, admitedly, the error message could be improved)
But I thought refers to the nixpkgs
pull request.
I needs that to run the CI against.
It looks for a nixpkgs
repository under the owner sertel
(on Github). For some reason...
And totally makes sense. This my fork where the PR is. The PR branch is ssprove
.
Are you missing a "ref" Attribute to fetchFromGitHub
?
I’m following the steps here:
I have the feeling that the toolbox does not like that I’m running this in the coq-nix-toolbox
directory (of my fork) with local branch called ssprove
.
Looks sound at first glance.
You could specify the commit hash instead of the branch.
I also tried it with the PR number.
Did not work.
It is indeed the case that one needs to run these commands in branch master
. Now it works.
I'm stuck again.
When generating the updates to the CI, the genNixActions
command misses to generate a CI job for Coq 8.17.
How does genNixActions
derive the bundles?
From the switch statement in the according nixpkgs
entry?
Problem found. See other thread.
Last updated: Oct 13 2024 at 01:02 UTC