Fix relative paths in .fst.config.json fstar exe #40
Conversation
|
I think this is a useful feature and wasn't much effort, but happy to discuss if I'm holding it wrong |
|
Looks good to me, thanks! @gebner, wdyt? |
There was a problem hiding this comment.
I am a bit lukewarm about this change. There are at the very least two executables that need to be in PATH: fstar.exe and z3. This PR only helps with the first one (if you're willing to manually set the vscode configuration option).
Additionally, many F* projects require you to set even more environment variables. (Note that since #17, .fst.config.json files can contain references to environment variables.) For example, everparse references KRML_HOME (and soon PULSE_HOME too).
FWIW, I usually open vscode from a command-line environment with all the right environment variables set:
eval `opam env`
export FSTAR_HOME=$HOME/FStar KRML_HOME=$HOME/karamel PATH=$HOME/FStar/bin:$PATH PULSE_HOME=$HOME/pulse
code .With the new configuration setting from this PR, I would still to set all the other environment variables and add Z3 to the PATH. It would be really amazing if we could improve on that workflow, but this PR isn't it. I wonder if we should officially bless an extension like direnv?
As for your particular set up, from what I can tell you already have the F*-specific z3 in the PATH. Could you also add fstar.exe to the PATH for now?
package.json
Outdated
| "scope": "resource", | ||
| "type": "string", | ||
| "default": "", | ||
| "description": "Prefix PATH environment variable" |
There was a problem hiding this comment.
It is not clear to me based on the description alone how you would use it. For example, I would expect to write /home/amosr/bin: here, but reading through the code the : is implicit. An example would be helpful in the description.
server/src/fstar.ts
Outdated
| // Check if fstar_exe can be found in the current path, taking into account | ||
| // the specified working directory and path overrides | ||
| const pathEnv = | ||
| configurationSettings.pathPrefix + path.delimiter + process.env.PATH; |
There was a problem hiding this comment.
Does this do the right thing if pathPrefix is empty?
|
Hi Gabriel, Thanks for your feedback and especially your pointer to the direnv extension - this does exactly what I want! It resolves the main issue for me. (I couldn't figure out how to manually modify the environment variables because I was using Remote-SSH, which loads the remote host's default environment.) So, there were actually two changes here - the environment issue is resolved, so I'll delete that part. The other change was a bugfix, which I still believe is a legitimate bug. If you agree I'll kill the path change and just keep the bugfix. The bug is related to local paths relative to the configuration file. The exact bug I've hit (a student here has hit it too) is where the x.fst.config.json sets fstar_exe to |
This change fixes a small bug in `.fst.config.json` where specifying the fstar executable with a relative path such as `_opam/bin/fstar.exe` was failing. Instead, we now interpret such a path as relative to the configuration file.
amosr
changed the title
|
Hi Gabriel, hi Nik, I've changed this PR to just fix the inconsistency in how relative paths are handled by which and spawn. Amos |
|
The relative path change looks good to me. (Although it is not a setup that is commonly used---the Thanks for the PR! |
This commit adds a
pathPrefixoption to allow modifying the search path without needing to change the project-specific.fst.config.json(which are often included in source control).This also fixes a small bug in
.fst.config.jsonwhere specifying the fstar executable with a relative path such as_opam/bin/fstar.exewas failing. Instead, we now interpret such a path as relative to the configuration file.Workspace-specific .vscode/settings.json: