search

coq-community / templates

Templates for configuration files and scripts useful for maintaining Coq projects [maintainers=@palmskog,@Zimmi48]
The Unlicense
13 stars 8 forks source link

New nix infrastructure #87

Closed CohenCyril closed 3 years ago

CohenCyril commented 3 years ago

CC @Zimmi48

CohenCyril commented 3 years ago

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

Zimmi48 commented 3 years ago

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

CohenCyril commented 3 years ago

woops ;)

CohenCyril commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

This PR cannot be merged until https://github.com/coq-community/coq-nix-toolbox/issues/49 is fixed.

Zimmi48 commented 3 years ago

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 commented 3 years ago

@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 commented 3 years ago

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