[ fix ] Add path of downloaded ALS after the user chooce to download it

Author: banacorn

CHANGELOG.md

@@ -5,7 +5,7 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html)
 
-## v0.6.5 - 2025-??-??
+## v0.6.5 - 2025-08-21
 
 ### Fixed
 - #250: Misplaced hole when a line contains some special characters

lib/js/src/Main/Mock.bs.js

@@ -86,8 +86,47 @@ module Platform = {
       let downloadLatestALS = (_logChannel, _memento, _globalStorageUri) => _platform =>
         Promise.resolve(Ok(downloadedPath))
 
-      let getFetchSpec = (_memento, _globalStorageUri, _platform) =>
-        Promise.resolve(Error(Connection__Download.Error.CannotFindCompatibleALSRelease))
+      let getFetchSpec = (_memento, _globalStorageUri, _platform) => {
+        // Create a mock fetch spec that will make Download.getAvailableDownload work
+        let mockAsset = {
+          Connection__Download__GitHub.Asset.url: "https://mock.url/download.zip",
+          id: 123456,
+          node_id: "mock_node_id",
+          name: "als-Agda-2.6.3-macOS-arm64.zip",
+          label: "",
+          content_type: "application/zip",
+          state: "uploaded",
+          size: 1000000,
+          created_at: "2023-01-01T00:00:00Z",
+          updated_at: "2023-01-01T00:00:00Z",
+          browser_download_url: "https://mock.url/download.zip",
+        }
+        let mockRelease = {
+          Connection__Download__GitHub.Release.url: "https://mock.url/release",
+          assets_url: "https://mock.url/assets",
+          upload_url: "https://mock.url/upload",
+          html_url: "https://mock.url/html",
+          id: 789012,
+          node_id: "mock_release_node_id",
+          tag_name: "v0.2.10",
+          target_commitish: "main",
+          name: "v0.2.10",
+          draft: false,
+          prerelease: false,
+          created_at: "2023-01-01T00:00:00Z",
+          published_at: "2023-01-01T00:00:00Z",
+          assets: [mockAsset],
+          tarball_url: "https://mock.url/tarball",
+          zipball_url: "https://mock.url/zipball",
+          body: Some("Mock release"),
+        }
+        let mockFetchSpec = {
+          Connection__Download__GitHub.FetchSpec.asset: mockAsset,
+          release: mockRelease,
+          saveAsFileName: "als-Agda-2.6.3-macOS-arm64",
+        }
+        Promise.resolve(Ok(mockFetchSpec))
+      }
       let findCommand = (_command, ~timeout as _timeout=1000) =>
         Promise.resolve(Error(Connection__Command.Error.NotFound))
       let openFolder = _uri => Promise.resolve()

lib/js/src/State/State__SwitchVersion.bs.js

@@ -592,6 +592,24 @@ module Handler = {
               )
 
               if alreadyDownloaded {
+                // Add the already downloaded path to config
+                // We need to get the downloaded path - use the same logic as the download case
+                switch await Download.getAvailableDownload(state, platformDeps) {
+                | Some((_, _)) =>
+                  // Get the path from the fetchSpec
+                  module PlatformOps = unpack(platformDeps)
+                  switch await PlatformOps.determinePlatform() {
+                  | Ok(platform) =>
+                    switch await PlatformOps.getFetchSpec(state.memento, state.globalStorageUri, platform) {
+                    | Ok(fetchSpec) =>
+                      let downloadedPath = VSCode.Uri.joinPath(state.globalStorageUri, [fetchSpec.saveAsFileName, "als"])->VSCode.Uri.fsPath
+                      await Config.Connection.addAgdaPath(state.channels.log, downloadedPath)
+                    | Error(_) => ()
+                    }
+                  | Error(_) => ()
+                  }
+                | None => ()
+                }
                 // Show "already downloaded" message
                 VSCode.Window.showInformationMessage(
                   versionString ++ " is already downloaded",
@@ -619,7 +637,9 @@ module Handler = {
                       [],
                     )->Promise.done
                     state.channels.log->Chan.emit(Log.SwitchVersionUI(SelectionCompleted))
-                  | Ok(_) =>
+                  | Ok(downloadedPath) =>
+                    // Add the downloaded path to config
+                    await Config.Connection.addAgdaPath(state.channels.log, downloadedPath)
                     // Refresh the UI to show new status
                     let newDownloadInfo = await Download.getAvailableDownload(state, platformDeps)
                     let _ = SwitchVersionManager.refreshFromMemento(manager)

lib/js/test/tests/Connection/Test__Connection__Config.bs.js

@@ -70,24 +70,6 @@ describe("Config.Connection paths", () => {
     ): Platform.t
   )
 
-  // Mock platform with download capability for testing download actions
-  let platformWithMockDownload = (
-    module(
-      {
-        include Desktop.Desktop
-        let findCommand = (_command, ~timeout as _timeout=1000) => {
-          Promise.resolve(Ok(systemAgda.contents))
-        }
-        let determinePlatform = async () => Ok(Connection__Download__Platform.MacOS_Arm)
-        let alreadyDownloaded = _globalStorageUri => async () => None
-
-        let downloadLatestALS = (_logChannel, _memento, _globalStorageUri) => _platform => {
-          Promise.resolve(Ok(downloadedALS.contents))
-        }
-      }
-    ): Platform.t
-  )
-
   // Helper function to create a connection with given config paths
   // also returns a Log listener to capture config changes
   let makeConnection = async (configPaths: array<string>, platform: Platform.t) => {
@@ -350,7 +332,11 @@ describe("Config.Connection paths", () => {
           detail: "ALS v0.2.10, Agda v2.7.0.1",
         }
 
-        await executeUITest(mockState, platformWithMockDownload, mockSelectedItem)
+        await executeUITest(
+          mockState,
+          Mock.Platform.makeWithSuccessfulDownload(downloadedALS.contents),
+          mockSelectedItem,
+        )
         let logs = listener(~filter=Log.isConfig)
         let finalConfig = Config.Connection.getAgdaPaths()
         (logs, finalConfig)
@@ -408,7 +394,6 @@ describe("Config.Connection paths", () => {
       }
     }
 
-
     describe(
       "Switch version UI selection",
       () => {
@@ -418,7 +403,11 @@ describe("Config.Connection paths", () => {
             let initialConfig = [userAgda.contents]
             let selectedPath = alternativeAgda.contents // not in initial config
 
-            let (logs, finalConfig) = await UITestBuilders.simulatePathSelection(initialConfig, selectedPath, ~description="")
+            let (logs, finalConfig) = await UITestBuilders.simulatePathSelection(
+              initialConfig,
+              selectedPath,
+              ~description="",
+            )
 
             // Should add the selected path to config
             let expectedConfig = Array.concat(initialConfig, [selectedPath])
@@ -451,7 +440,11 @@ describe("Config.Connection paths", () => {
             let initialConfig = [userAgda.contents]
             let selectedPath = alternativeAgda.contents
 
-            let (logs, finalConfig) = await UITestBuilders.simulatePathSelection(initialConfig, selectedPath, ~description="")
+            let (logs, finalConfig) = await UITestBuilders.simulatePathSelection(
+              initialConfig,
+              selectedPath,
+              ~description="",
+            )
 
             // Should add the new path to existing config
             let expectedConfig = Array.concat(initialConfig, [selectedPath])
@@ -475,15 +468,15 @@ describe("Config.Connection paths", () => {
               ~isAlreadyDownloaded=false,
             )
 
-            // Download action should not modify config in test environment
-            // (real downloads would modify config, but test environment doesn't have download capability)
-            Assert.deepStrictEqual(logs, [])
-            Assert.deepStrictEqual(finalConfig, initialConfig)
+            // Should add the downloaded ALS path to config
+            let expectedConfig = Array.concat(initialConfig, [downloadedALS.contents])
+            Assert.deepStrictEqual(logs, [Log.Config(Changed(initialConfig, expectedConfig))])
+            Assert.deepStrictEqual(finalConfig, expectedConfig)
           },
         )
 
         Async.it(
-          "should show already downloaded message when user selects already downloaded ALS",
+          "should add already downloaded path to config when user selects already downloaded ALS",
           async () => {
             let initialConfig = [userAgda.contents]
 
@@ -492,10 +485,10 @@ describe("Config.Connection paths", () => {
               ~isAlreadyDownloaded=true,
             )
 
-            // Download action should not modify config in test environment
-            // (shows message but doesn't download or modify config)
-            Assert.deepStrictEqual(logs, [])
-            Assert.deepStrictEqual(finalConfig, initialConfig)
+            // Should add the already downloaded ALS path to config
+            let expectedConfig = Array.concat(initialConfig, [downloadedALS.contents])
+            Assert.deepStrictEqual(logs, [Log.Config(Changed(initialConfig, expectedConfig))])
+            Assert.deepStrictEqual(finalConfig, expectedConfig)
           },
         )
       },