Sebastian Ertel (Apr 12 2024 at 13:47): Sebastian Ertel (Apr 12 2024 at 13:47):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.
Sebastian Ertel (Apr 17 2024 at 07:18):@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.
Cyril Cohen (Apr 23 2024 at 08:35):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/ssprovederivation to include the dependencies you need. Cyril Cohen (Apr 23 2024 at 08:38):Cf https://github.com/sertel/ssprove/pull/1 for the result
Cyril Cohen (Apr 23 2024 at 08:44):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) Cyril Cohen (Apr 23 2024 at 08:45):Cf https://github.com/sertel/ssprove/pull/2 for the result
Cyril Cohen (Apr 23 2024 at 08:48):Also, in the
config.nixscript, there is abuildInputsattribute. 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.
Sebastian Ertel (Apr 25 2024 at 20:21):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?
Cyril Cohen (Apr 26 2024 at 05:54):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.
Cyril Cohen (Apr 26 2024 at 05:55):Of course you can always test locally to your computer builds of released packages through the nix-build -A command in your nixpkgs workdir
Cyril Cohen (Apr 26 2024 at 05:57):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.
Sebastian Ertel (Apr 26 2024 at 06:52):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.
Sebastian Ertel (Apr 26 2024 at 07:18):Oh I see now.
All the CI jobs are actually repo-local to coq-nix-toolbox. I had completely spaced on that. Sorry.
Sebastian Ertel (Apr 26 2024 at 14:01):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?
Pierre Roux (Apr 26 2024 at 14:21):I sse no sprove branch on your fork of coq-nix-toolbox: https://github.com/sertel/coq-nix-toolbox
Pierre Roux (Apr 26 2024 at 14:22):(if that's the issue, admitedly, the error message could be improved)
Sebastian Ertel (Apr 26 2024 at 14:38):But I thought refers to the nixpkgs pull request.
I needs that to run the CI against.
spacefrogg (Apr 26 2024 at 14:44):It looks for a nixpkgs repository under the owner sertel (on Github). For some reason...
Sebastian Ertel (Apr 26 2024 at 15:25):And totally makes sense. This my fork where the PR is. The PR branch is ssprove.
spacefrogg (Apr 26 2024 at 15:40):Are you missing a "ref" Attribute to fetchFromGitHub?
Sebastian Ertel (Apr 26 2024 at 15:51):I’m following the steps here:
Sebastian Ertel (Apr 26 2024 at 15:53):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.
spacefrogg (Apr 26 2024 at 15:54):Looks sound at first glance.
spacefrogg (Apr 26 2024 at 15:57):You could specify the commit hash instead of the branch.
Sebastian Ertel (Apr 26 2024 at 16:02):I also tried it with the PR number.
Sebastian Ertel (Apr 26 2024 at 16:02):Did not work.
Sebastian Ertel (Apr 29 2024 at 08:45):It is indeed the case that one needs to run these commands in branch master. Now it works.
Sebastian Ertel (Apr 29 2024 at 12:33):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?
Sebastian Ertel (Apr 30 2024 at 08:39):Problem found. See other thread.
Last updated: Oct 13 2024 at 01:02 UTC