Skip to content

Conversation

@faukah
Copy link

@faukah faukah commented Sep 18, 2025

Hey everyone!
I saw that the rocq Nix infra seems not to be maintained very actively, so I thought I'd give it a proper cleaning and fix some outdated stuff. This is still very WIP, but I thought I'd push it as a Draft prematurely to get some feedback, as I am not that familiar with rocq.

If this is unwelcome, please do tell me so as this PR is likely to be a bigger (~500-600loc) one; It would be good to know before I spend some hours on this.

@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 18, 2025
@proux01
Copy link
Contributor

proux01 commented Sep 19, 2025

Thanks for the initial heads up. This thing is indeed outdated. Currently, the most used Nix machinery around Rocq is the toolbox: https://github.com/rocq-community/coq-nix-toolbox/ that is used both to test nixpkgs PRs and in multiple CIs.
AFAIR, it was decided (but never implemented) to port the old nix files in the current repo to the toolbox. But my memory is fuzzy, I may be wrong. @Zimmi48 do you remember better? As to porting the toolbox to flake, there is some work in progress rocq-community/coq-nix-toolbox#361 not sure what's the current status.
In any case, there is a dedicated zulip stream https://rocq-prover.zulipchat.com/#narrow/channel/290990-Nix-and-Coq-Nix-Toolbox-devs-.26-users that may be more convenient for quick discussions.

@Zimmi48
Copy link
Member

Zimmi48 commented Sep 30, 2025

There are many, currently under-maintained, pieces of Nix infra in this repo. The one that I introduced and that I continue to use for development (but recently failed to update, see #20441) is the default.nix part. This is the part that is tested in CI, even if part of it is broken:

rocq/.gitlab-ci.yml

Lines 402 to 443 in 30e9382

# broken, see eg https://gitlab.com/coq/coq/-/jobs/1754045983
# pkg:nix:deploy:
# extends: .nix-template
# environment:
# name: cachix
# url: https://coq.cachix.org
# script:
# - nix-build https://coq.inria.fr/nix/toolbox --argstr job coq --arg override "{coq = coq:$CI_COMMIT_SHA;}" -K | cachix push coq
# only:
# refs:
# - master
# - /^v.*\..*$/
# variables:
# - $CACHIX_AUTH_TOKEN
# pkg:nix:deploy:channel:
# extends: .deploy-template
# environment:
# name: cachix
# url: https://coq.cachix.org
# only:
# refs: # Repeat conditions from pkg:nix:deploy
# - master
# - /^v.*\..*$/
# variables:
# - $CACHIX_AUTH_TOKEN && $CACHIX_DEPLOYMENT_KEY
# # if the $CACHIX_AUTH_TOKEN variable isn't set, the job it depends on doesn't exist
# needs:
# - pkg:nix:deploy
# script:
# - echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null
# # Remove all pr branches because they could be missing when we run git fetch --unshallow
# - git branch --list 'pr-*' | xargs -r git branch -D
# - git fetch --unshallow
# - git branch -v
# - git push [email protected]:rocq-prover/coq-on-cachix "${CI_COMMIT_SHA}":"refs/heads/${CI_COMMIT_REF_NAME}"
pkg:nix:
extends: .nix-template
script:
- nix-build "$CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz" -K
only: *full-ci

Then, there is the infrastructure added by @vbgl under https://github.com/rocq-prover/rocq/tree/master/dev/ci/nix for reverse dependencies. I don't know if this infra is still used by anyone.

These two parts could be (rather easily) superseded by using the Coq Nix Toolbox as is, and I think it should be done. There was an initial attempt by myself to do this a long time ago in #14435, but I think it was too ambitious (we shouldn't test reverse dependencies in the Nix CI setup for now).

Then, there is the flake part that this PR attempts to update. This was introduced without consideration for existing Nix infra in #17675, to be reused in the VsCoq repo. I was always very reluctant to this duplication and the way this was done. Now, this could also be superseded by the Coq Nix Toolbox if we finished the PR that Pierre linked above. That being said, I don't see this happening in the foreseeable future. I personally don't intend to work on this for a while.

@vbgl
Copy link
Contributor

vbgl commented Sep 30, 2025

Then, there is the infrastructure added by @vbgl under https://github.com/rocq-prover/rocq/tree/master/dev/ci/nix for reverse dependencies. I don't know if this infra is still used by anyone.

I think this part can be safely removed.

@Zimmi48
Copy link
Member

Zimmi48 commented Sep 30, 2025

Also note the related #19298, which I should have re-reviewed, but didn't so far.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants