If the include_dirs is empty, then add the directory of the file to the include path.

nikswamy · nikswamy · commit 1eb8faea2cf1 · 2025-01-27T10:34:30.000-08:00
diff --git a/lspserver/src/fstar.ts b/lspserver/src/fstar.ts
@@ -61,6 +61,10 @@ export class FStar {
 		if (config.include_dirs) {
 			config.include_dirs.forEach((dir) => { options.push("--include"); options.push(dir); });
 		}
+		if (!config.include_dirs || config.include_dirs.length === 0) {
+			options.push("--include");
+			options.push(path.dirname(filePath));
+		}
 		if (!config.fstar_exe) {
 			config.fstar_exe = "fstar.exe";
 		}

Original file line number	Diff line number	Diff line change
`@@ -61,6 +61,10 @@ export class FStar {`
`61`	`61`	`if (config.include_dirs) {`
`62`	`62`	`config.include_dirs.forEach((dir) => { options.push("--include"); options.push(dir); });`
`63`	`63`	`}`
	`64`	`+ if (!config.include_dirs \|\| config.include_dirs.length === 0) {`
	`65`	`+ options.push("--include");`
	`66`	`+ options.push(path.dirname(filePath));`
	`67`	`+ }`
`64`	`68`	`if (!config.fstar_exe) {`
`65`	`69`	`config.fstar_exe = "fstar.exe";`
`66`	`70`	`}`