Command line arguments to Coqtop

[dailler]

Hello,

Is there a way to pass commandline arguments to Coqtop with Vscoq ? My use case would be to call something like:
code --coqtop-arguments="-R my_lib name_my_lib" my_file.v

I have found the settings option coqtop.args: is there a way to change the settings on the commandline or with environment variables ? Such as:
code --vscoq.settings="coqtop.arguments=[-R ...]"

I have also tried looking at the COQPATH environment variable but it seems that it is not expressive enough for -R.

[Zimmi48]

If that's your use case, then you should probably use a _CoqProject file instead. VsCoq, like most editor support packages, supports reading options (in particular -Q and -R) provided at the top of the _CoqProject file.

[dailler]

My objective is actually to launch Coq from another tool (Why3): we already support editors such as coqide and proofgeneral. In this context, it would have been more convenient to use commandline arguments (to be fair, there are workarounds for my usecase).

I will try to investigate the _CoqProject solution. Thanks for your help.

That said, I am still interested to know if this kind of feature is on the roadmap for vscoq ?

[fakusb]

You can edit the .vscode/settings.json file to adjust the coqtop.args setting, which get's passed to coqidetop. Note coq/vscoq#224 for a common problem when using this option.

As far as I know, vscode does not allow to pass temporary settings via the command line that starts the IDE itself.