fix: use manifest packagesDir entry instead of lake-packages

leanprover · Nov 14, 2023 · ba5c660 · ba5c660
1 parent ddf645d
commit ba5c660
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/vscode-lean4/src/projectoperations.ts b/vscode-lean4/src/projectoperations.ts
@@ -168,7 +168,7 @@ export class ProjectOperationProvider implements Disposable {
             await this.tryFetchingCache(lakeRunner)
 
             const localToolchainPath: string = join(activeClient.folderUri.fsPath, 'lean-toolchain')
-            const dependencyToolchainPath: string = join(activeClient.folderUri.fsPath, 'lake-packages', dependencyChoice.name, 'lean-toolchain')
+            const dependencyToolchainPath: string = join(activeClient.folderUri.fsPath, manifestResult.packagesDir, dependencyChoice.name, 'lean-toolchain')
             const dependencyToolchainResult: string | 'DoNotUpdate' | 'Cancelled' = await this.determineDependencyToolchain(localToolchainPath, dependencyToolchainPath, dependencyChoice.name)
             if (dependencyToolchainResult === 'Cancelled') {
                 return

diff --git a/vscode-lean4/src/utils/manifest.ts b/vscode-lean4/src/utils/manifest.ts
@@ -11,6 +11,7 @@ export interface DirectGitDependency {
 }
 
 export interface Manifest {
+    packagesDir: string
     directGitDependencies: DirectGitDependency[]
 }
 
@@ -23,6 +24,7 @@ export function parseAsManifest(jsonString: string): Manifest | undefined {
     }
 
     const schema = z.object({
+        packagesDir: z.string(),
         packages: z.array(
             z.union([
                 z.object({
@@ -45,7 +47,7 @@ export function parseAsManifest(jsonString: string): Manifest | undefined {
         return undefined
     }
 
-    const manifest: Manifest = { directGitDependencies: [] }
+    const manifest: Manifest = { packagesDir: result.data.packagesDir, directGitDependencies: [] }
 
     for (const pkg of result.data.packages) {
         if (!('git' in pkg)) {