search

coq-community / coq-nix-toolbox

Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
MIT License
32 stars 9 forks source link

Testing vscoq2 #163

Closed CohenCyril closed 7 months ago

CohenCyril commented 12 months ago

Testing nix PR https://github.com/NixOS/nixpkgs/issues/256515

@Zimmi48 this PR includes an extension of the toolbox to add the vscoq2 language server to any shell.

Zimmi48 commented 12 months ago

Would it make sense to make this optional with an argument similar to the current withEmacs?

[We could go further, BTW, and provide a reproducible VSCoq environment where VS Code is provided with the VsCoq extension pre-installed via Nix too. But that's more work.]

CohenCyril commented 12 months ago

Would it make sense to make this optional with an argument similar to the current withEmacs?

I don't think so. withEmacs will basically override your own emacs and your init file, so it's mandatory for it to be optional. Since the vscoq2 language server is tied to the version of coq, which is always in the build inputs of your derivation, I'd say it is mandatory to use this specific version at all times. However could have a withoutVSCoqServer option, but I'm not sure what use it would have.

[We could go further, BTW, and provide a reproducible VSCoq environment where VS Code is provided with the VsCoq extension pre-installed via Nix too. But that's more work.]

Sure, and then it would indeed make sense to have a withVSCode option indeed. And I believe it is not a lot of work.

Zimmi48 commented 12 months ago

Sure, and then it would indeed make sense to have a withVSCode option indeed. And I believe it is not a lot of work.

Should be withVsCoq preferably since VsCoq is not the only option for Coq support in VS Code.

I don't think so. withEmacs will basically override your own emacs and your init file, so it's mandatory for it to be optional. Since the vscoq2 language server is tied to the version of coq, which is always in the build inputs of your derivation, I'd say it is mandatory to use this specific version at all times. However could have a withoutVSCoqServer option, but I'm not sure what use it would have.

I guess it's not going to hurt anyone to have it in their dev environment even if they don't use it, but it will not be useful to everyone of course (one can develop Coq projects using ProofGeneral, or Coqtail, or coq-lsp, or VsCoq1, and none of these options require the vscoq2 language server).

CohenCyril commented 12 months ago

Sure, and then it would indeed make sense to have a withVSCode option indeed. And I believe it is not a lot of work.

Should be withVsCoq preferably since VsCoq is not the only option for Coq support in VS Code.

Ok, it's a bit of a lie both way (withVsCoq seems to imply we install only vscoq and not vscode). But I won't debate the name anymore. Any of the two make sense.

I don't think so. withEmacs will basically override your own emacs and your init file, so it's mandatory for it to be optional. Since the vscoq2 language server is tied to the version of coq, which is always in the build inputs of your derivation, I'd say it is mandatory to use this specific version at all times. However could have a withoutVSCoqServer option, but I'm not sure what use it would have.

I guess it's not going to hurt anyone to have it in their dev environment even if they don't use it, but it will not be useful to everyone of course (one can develop Coq projects using ProofGeneral, or Coqtail, or coq-lsp, or VsCoq1, and none of these options require the vscoq2 language server).

We already put extra stuff in the environment anyway. As long as the vscoq language server stays as small as today, I think we can silently add it. We could also load coq-lsp language server for those who want (and the others do not need an executable, so I guess they're fine).