Testing vscoq2

[CohenCyril]

Testing nix PR NixOS/nixpkgs#256515

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

[Zimmi48]

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]

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]

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]

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).