message: fix: check elan status should also be a progress notication, not an outputChannel write.
diff: @@ -158,8 +158,33 @@ export class LeanInstaller implements Disposable {
  // Specifically, if the extension was not opened inside of a folder, it
  // looks for a global (default) installation of Lean. This way, we can support
  // single file editing.
  - let stdout = '';
  + const stdout = await this.executeWithProgress('Checking Lean setup...', cmd, options,folderPath)
  + if (!stdout) {
  + throw new Error('lean not found');
  + }
  + if (stdout.indexOf('no default toolchain') > 0) {
  + return { version: '', error: 'no default toolchain' };
  + }
  + const filterVersion = /version (\d+)\.\d+\..+/
  + const match = filterVersion.exec(stdout)
  + if (!match) {
  + if (!stdout) {
  + return { version: '', error: `lean4: '${cmd}' program not found.` }
  + } else {
  + return { version: '', error: `lean4: '${cmd} ${options}' returned incorrect version string '${stdout}'.` }
  + }
  + }
  + const major = match[1]
  + return { version: major, error: null }
  + } catch (err) {
  + if (this.outputChannel) this.outputChannel.appendLine(err);
  + return { version: '', error: err };
  + }
  + }
  +
  + async executeWithProgress(prompt: string, cmd: string, options: string[], workingDirectory: string): Promise<string>{
  let inc = 0;
  + let stdout = ''
  await window.withProgress({
  location: ProgressLocation.Notification,
  title: '',
  @@ -184,30 +209,10 @@ export class LeanInstaller implements Disposable {
  hide() { /* empty */ },
  dispose() { /* empty */ }
  }
  - progress.report({increment:0, message: 'Checking Lean setup...'});
  - return batchExecute(cmd, options, folderPath, progressChannel);
  + progress.report({increment:0, message: prompt});
  + return batchExecute(cmd, options, workingDirectory, progressChannel);
  });
  - if (!stdout) {
  - throw new Error('lean not found');
  - }
  - if (stdout.indexOf('no default toolchain') > 0) {
  - return { version: '', error: 'no default toolchain' };
  - }
  - const filterVersion = /version (\d+)\.\d+\..+/
  - const match = filterVersion.exec(stdout)
  - if (!match) {
  - if (!stdout) {
  - return { version: '', error: `lean4: '${cmd}' program not found.` }
  - } else {
  - return { version: '', error: `lean4: '${cmd} ${options}' returned incorrect version string '${stdout}'.` }
  - }
  - }
  - const major = match[1]
  - return { version: major, error: null }
  - } catch (err) {
  - if (this.outputChannel) this.outputChannel.appendLine(err);
  - return { version: '', error: err };
  - }
  + return stdout;
  }
  async getDefaultToolchain(): Promise<string> {
  @@ -254,9 +259,8 @@ export class LeanInstaller implements Disposable {
  let elanInstalled = false;
  // See if we have elan already.
  try {
  - this.outputChannel.show(true);
  const options = ['--version']
  - const stdout = await batchExecute('elan', options, undefined, this.outputChannel);
  + const stdout = await this.executeWithProgress('Checking Elan setup...', 'elan', options, undefined)
  const filterVersion = /elan (\d+)\.\d+\..+/
  const match = filterVersion.exec(stdout)
  if (match) {
  