fix: dafny.dotnetExecutablePath works to install custom source (#287)

* fix: `dafny.dotnetExecutablePath` works to install custom source

If `dotnet` is installed
and placed in `dafny.dotnetExecutablePath`
custom source should still be able to be built.

To do this `checkSupportedDotnetVersion`
needs to be the primary way to detect `dotnet`.
This has the side effect of both not double installing from `brew`
but also not requireing an install if `dotnet` is already installed.

The `wget` call is also removed
since there are already helpers to perform this get and unzip.
They are updated to take a `thing` to facilitate logging.
There is also a bit of update to the `Z3` section
to account for this change.

The largest issue with this was
`Source/DafnyCore/DafnyCore.csproj`
has direct `dotnet` build targets.
This means that call to build will fail
if `dotnet` is not on the `PATH`.
This is unfortunate, but…
So we add it for that specific command.

Finnaly, speed up the `git clone`
to both checkout the tag and not get history.

Added a few things to `.gitignore`
and simplified the ReadMe’s use of `vsce`

* lint

Author: seebees

.gitignore

@@ -5,3 +5,5 @@ node_modules/
 .DS_Store
 /dist/*
 !/dist/.gitkeep
+/.history
+*.vsix

README.md

@@ -138,16 +138,10 @@ Because the latest version of the plugin requires recent changes to the Dafny la
 
 ### Packaging
 
-To create a VSIX package of the previously built sources, install the [VSCode Extension Manager](https://github.com/microsoft/vscode-vsce) globally:
+To create a VSIX package of the previously built sources, create the package through the CLI:
 
 ```sh
-npm install -g vsce
-```
-
-Now create the package through the CLI:
-
-```sh
-vsce package
+npx vsce package
 ```
 
 ### Coding Conventions

src/language/dafnyInstallation.ts

@@ -16,6 +16,8 @@ import { exec } from 'child_process';
 import { chdir as processChdir, cwd as processCwd } from 'process';
 import fetch from 'cross-fetch';
 
+import { checkSupportedDotnetVersion, getDotnetExecutablePath } from '../dotnet';
+
 const execAsync = promisify(exec);
 
 const ArchiveFileName = 'dafny.zip';
@@ -165,8 +167,8 @@ export class DafnyInstaller {
         this.writeStatus(`Found a non-supported architecture OSX:${os.arch()}. Going to install from source.`);
         return await this.installFromSource();
       } else {
-        const archive = await this.downloadArchive(await getDafnyDownloadAddress(this.context));
-        await this.extractArchive(archive);
+        const archive = await this.downloadArchive(await getDafnyDownloadAddress(this.context), 'Dafny');
+        await this.extractArchive(archive, 'Dafny');
         await workspace.fs.delete(archive, { useTrash: false });
         this.writeStatus('Dafny installation completed');
         return true;
@@ -200,18 +202,23 @@ export class DafnyInstaller {
     const previousDirectory = processCwd();
     processChdir(installationPath.fsPath);
     try {
-      await this.execLog('brew install dotnet-sdk');
+      await checkSupportedDotnetVersion();
     } catch(error: unknown) {
-      this.writeStatus('An error occurred while running this command.');
-      this.writeStatus(`${error}`);
-      this.writeStatus(`If brew is installed on your system, this can usually be resolved by adding add all brew commands to your ~/.zprofile,
-      e.g. by running the script there https://apple.stackexchange.com/a/430904 :
-
-      > echo 'eval "$(/opt/homebrew/bin/brew shellenv)"' >> ~/.zprofile
-      > eval "$(/opt/homebrew/bin/brew shellenv)"
-
-      and restart VSCode, which may reinstall Dafny.`);
-      return false;
+      try {
+        this.writeStatus('dotnet not found in $PATH, trying to install from brew.');
+        await this.execLog('brew install dotnet-sdk');
+      } catch(error: unknown) {
+        this.writeStatus('An error occurred while running this command.');
+        this.writeStatus(`${error}`);
+        this.writeStatus(`If brew is installed on your system, this can usually be resolved by adding add all brew commands to your ~/.zprofile,
+        e.g. by running the script there https://apple.stackexchange.com/a/430904 :
+  
+        > echo 'eval "$(/opt/homebrew/bin/brew shellenv)"' >> ~/.zprofile
+        > eval "$(/opt/homebrew/bin/brew shellenv)"
+  
+        and restart VSCode, which may reinstall Dafny.`);
+        return false;
+      }
     }
     const configuredVersion = await getConfiguredVersion(this.context);
     if(versionToNumeric(configuredVersion) < versionToNumeric('3.9.0')) {
@@ -231,24 +238,35 @@ export class DafnyInstaller {
         return false;
       }
     }
-    await this.execLog(`git clone --recurse-submodules ${LanguageServerConstants.DafnyGitUrl}`);
+
+    // Clone the right version
+    await this.execLog(`git clone -b v${configuredVersion} --depth 1 --recurse-submodules ${LanguageServerConstants.DafnyGitUrl}`);
     processChdir(Utils.joinPath(installationPath, 'dafny').fsPath);
-    await this.execLog('git fetch --all --tags');
-    await this.execLog(`git checkout v${configuredVersion}`);
-    await this.execLog('dotnet build Source/DafnyLanguageServer/DafnyLanguageServer.csproj');
+
+    const { path: dotnet } = await getDotnetExecutablePath();
+    // The DafnyCore.csproj has a few targets that call `dotnet` directly.
+    // If dotnet is configured in dafny.dotnetExecutablePath
+    // it MAY NOT be on the path.
+    // This will cause the build to fail.
+    // This works around this edge case.
+    const injectPath = `PATH=${path.dirname(dotnet)}:$PATH`;
+    // Build the DafnyLanguageServer
+    await this.execLog(`${injectPath} ${ (await getDotnetExecutablePath()).path } build Source/DafnyLanguageServer/DafnyLanguageServer.csproj`);
     const binaries = Utils.joinPath(installationPath, 'dafny', 'Binaries').fsPath;
     processChdir(binaries);
     try {
       await this.execLog('brew update'); // Could help some users not get "Error: The `brew link` step did not complete successfully"
     } catch(error: unknown) {
       this.writeStatus(`Could not run \`brew update\` but this step is optional (${error})`);
     }
-    await this.execLog('brew install wget');
+
     const z3urlOsx = this.GetZ3DownloadUrlOSX();
     const z3filenameOsx = this.GetZ3FileNameOSX();
-    await this.execLog(`wget ${z3urlOsx}`);
-    await this.execLog(`unzip ${z3filenameOsx}.zip`);
-    await this.execLog(`mv ${z3filenameOsx} z3`);
+    const archive = await this.downloadArchive(z3urlOsx, 'Z3');
+    await this.extractArchive(archive, 'Z3');
+    await workspace.fs.delete(archive, { useTrash: false });
+
+    await this.execLog(`mv ${(await this.getInstallationPath()).fsPath}/${z3filenameOsx} z3`);
     processChdir((await this.getInstallationPath()).fsPath);
     await this.execLog('mkdir -p ./dafny/');
     await this.execLog(`cp -R ${binaries}/* ./dafny/`);
@@ -288,12 +306,12 @@ export class DafnyInstaller {
     }
   }
 
-  private async downloadArchive(downloadUri: string): Promise<Uri> {
+  private async downloadArchive(downloadUri: string, downloadTarget: string): Promise<Uri> {
     await mkdirAsync((await this.getInstallationPath()).fsPath, { recursive: true });
     const archivePath = await this.getZipPath();
     return await new Promise<Uri>((resolve, reject) => {
       const archiveHandle = fs.createWriteStream(archivePath.fsPath);
-      this.writeStatus(`downloading Dafny from ${downloadUri}`);
+      this.writeStatus(`downloading ${downloadTarget} from ${downloadUri}`);
       const progressReporter = new ProgressReporter(this.statusOutput);
       archiveHandle
         .on('finish', () => resolve(archivePath))
@@ -305,9 +323,9 @@ export class DafnyInstaller {
     });
   }
 
-  private async extractArchive(archivePath: Uri): Promise<void> {
+  private async extractArchive(archivePath: Uri, extractName: string): Promise<void> {
     const dirPath = await this.getInstallationPath();
-    this.writeStatus(`extracting Dafny to ${dirPath.fsPath}`);
+    this.writeStatus(`extracting ${extractName} to ${dirPath.fsPath}`);
     const progressReporter = new ProgressReporter(this.statusOutput);
     await extract(
       archivePath.fsPath,