Skip to content

Commit

Permalink
Fix relative paths in .fst.config.json fstar exe
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
amosr committed May 6, 2024
1 parent 3fdf711 commit e866b78
Showing 1 changed file with 10 additions and 2 deletions.
12 changes: 10 additions & 2 deletions server/src/fstar.ts
Original file line number Diff line number Diff line change
Expand Up @@ -67,15 +67,23 @@ export class FStar {

// check if fstar_exe can be found in the current path
// using which
let fstar_exe_resolved: string = config.fstar_exe;
try {
which.sync(config.fstar_exe);
// If there are any slashes in the fstar.exe, turn it into an absolute
// path relative to the config's working directory. If it is already
// absolute, the working directory will be ignored.
if (fstar_exe_resolved.indexOf(path.sep) >= 0) {
fstar_exe_resolved = path.resolve(config.cwd, fstar_exe_resolved);
}
// Search in $PATH
fstar_exe_resolved = which.sync(fstar_exe_resolved);
}
catch (err) {
throw new Error("Failed to find fstar.exe in path: " + err);
}

const proc = cp.spawn(
config.fstar_exe,
fstar_exe_resolved,
options,
{ cwd: config.cwd }
);
Expand Down

0 comments on commit e866b78

Please sign in to comment.