New nix infrastructure

[CohenCyril]

CC @Zimmi48

• Update ref.yml

[Zimmi48]

Did you forget to git add config.nix and shellHook.sh?

[CohenCyril]

@Zimmi48 I reached something satisfactory, want to talk about it?

[Zimmi48]

Sure! I'm available anytime tomorrow, Tuesday or next Thursday/Friday.

[Zimmi48]

Some typos in the documentation of config.nix.

[CohenCyril]

woops ;)

[CohenCyril]

It seems to me that the instructions on how to define / extend tasks should still be present even if the initial list of tasks was generated from meta.yml given that as soon as you copy the file into config.nix, you are on your own and you cannot rely on this generation process to edit them anymore.

I think there should be two distinct docs anyway: one on coq-community/template functionalities and one on the coq-community/coq-nix-toolbox functionalities. When one copies fallback-config.nix to config.nix they should be warned that by doing so 1. the handling of task should be removed from meta.yml and 2. they must now refer to coq-nix-toolbox documentation.

Anyway meta.yml is now able to generate everything that most user may want from config.nix. The missing feature is code factoring as in
https://github.com/math-comp/analysis/pull/345/files#diff-a4e04df48252cabe60d40e7d9b7417d7c5f9259e81e4be5e86f18430a22d011aR1-R8
or using overrideAttrs instead of override (which I never had to use because I prefer overlays).

[CohenCyril]

BTW, now that tasks generation is also handled by the templates, what is the remaining justification for leaving the possibility to the user to copy and manually edit the fallback-config.nix file?

I'm not sure anymore (I did not expect to reach that level of automated generation when I started...)

[Zimmi48]

I'm not sure anymore (I did not expect to reach that level of automated generation when I started...)

Yeah, me neither! Anyway, my opinion is that having to copy the template fallback config to a new file was fine when you couldn't do most things except by hand but now it doesn't really make sense anymore. So what I suggest is to have config.yml auto-generated and some option in meta.yml to disable its generation when people want to switch to manually editing this file. We should anyway have a general mechanism to disable a list of files from the auto-generation process (beyond listing explicitly all the files that you want to get, which doesn't scale).

[Zimmi48]

Let's check that this is still compatible with the latest version of the toolbox.

[Zimmi48]

Some changes are needed to default.nix.mustache to use the latest version of the toolbox.

[Zimmi48]

Note that we could set a default value for this token if community is true.

[Zimmi48]

FWIW, I tried with this patch but it didn't work:

diff --git a/nix-action.yml.mustache b/nix-action.yml.mustache
index 3f67a5c..60a4e9f 100644
--- a/nix-action.yml.mustache
+++ b/nix-action.yml.mustache
@@ -39,6 +39,21 @@ jobs:
 <%# token%>
         authToken: '${{ secrets.<%token%> }}'
 <%/ token%>
+<%/ cachix%>
+<%^ cachix%>
+<%# community%>
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: coq
+    - name: Cachix setup coq-community
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: coq-community
+        authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+<%/ community%>
 <%/ cachix%>
     - name: Git checkout
       uses: actions/checkout@v2
@@ -87,6 +102,21 @@ jobs:
 <%# token%>
         authToken: '${{ secrets.<%token%> }}'
 <%/ token%>
+<%/ cachix%>
+<%^ cachix%>
+<%# community%>
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: coq
+    - name: Cachix setup coq-community
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: coq-community
+        authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+<%/ community%>
 <%/ cachix%>
     - name: Git checkout
       uses: actions/checkout@v2

My Mustache is too rusty for me to understand what the problem is.

[Zimmi48]

I did manage to do something similar with default Cachix instances and default Cachix pushing for coq-community projects in #99.

[Zimmi48]

This used to be provided as the nix field of the dependencies list. Would it be possible to reuse this (less conversion of projects using the former infrastructure)? If not, we should remove this unused field from the documentation.

[Zimmi48]

This PR cannot be merged until coq-community/coq-nix-toolbox#49 is fixed.

[Zimmi48]

At this stage, my opinion is that it's better if we don't have to maintain three different complex CI generation procedures, so it would make sense to only focus on the generation mechanism of the standalone installation procedure, and to only provide a lightweight CI template here like in #99. So I propose to close this.

[Zimmi48]

@CohenCyril: do you agree with my suggestion of closing this and recommending either a full Coq Nix Toolbox setup with a standalone installation or a lightweight CI generation mechanism with the current version of the templates (following #99)?

[CohenCyril]

Ok! I'd rather keep the branch though...