From ba5c660d578fc60dc17089293593d94df6bceb94 Mon Sep 17 00:00:00 2001
From: mhuisi <mhuisi@protonmail.com>
Date: Fri, 10 Nov 2023 21:28:43 +0100
Subject: [PATCH] fix: use manifest packagesDir entry instead of lake-packages

---
 vscode-lean4/src/projectoperations.ts | 2 +-
 vscode-lean4/src/utils/manifest.ts    | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/vscode-lean4/src/projectoperations.ts b/vscode-lean4/src/projectoperations.ts
index 8ceb5f7e0..0af237276 100644
--- 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
index 81fb1af46..dea9e8b72 100644
--- 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)) {