message: fix: remove the lake test because it is too slow, and switch to a test based on the lean-toolchain version string instead.
diff: @@ -22,6 +22,7 @@ import { assert } from './utils/assert'
  import { LeanFileProgressParams, LeanFileProgressProcessingInfo } from '@lean4/infoview-api';
  import { LocalStorageService} from './utils/localStorage'
  import { batchExecute, testExecute } from './utils/batch'
  +import { readLeanVersion } from './utils/projectInfo';
  import { cwd } from 'process'
  import * as fs from 'fs';
  import { URL } from 'url';
  @@ -117,31 +118,22 @@ export class LeanClient implements Disposable {
  // check if the lake process will start.
  let useLake = lakeEnabled();
  - if (useLake && this.folderUri && this.folderUri.scheme === 'file') {
  + if (useLake && this.folderUri) {
  + if (this.folderUri.scheme === 'file') {
  const lakefile = Uri.joinPath(this.folderUri, 'lakefile.lean').toString()
  if (!fs.existsSync(new URL(lakefile))) {
  useLake = false;
  + } else {
  + const toolchainVersion = await readLeanVersion(this.folderUri);
  + if (toolchainVersion) {
  + const date = this.extractToolchainDate(toolchainVersion);
  + if (date < new Date(2022, 1, 1)){
  + useLake = false; // Feb 1 2022 is when the 3.0.0.pre switched to 3.0.0
  }
  }
  -
  - // This is a faster way of finding out lake doesn't work in the current workspace.
  - // The LanguageClient is much slower because it does 10 retries and everything.
  - if (useLake) {
  - // First check we have a version of lake that supports "lake serve"
  - const versionOptions = version ? ['+' + version, '--version'] : ['--version']
  - const lakeVersion = await batchExecute(executable, versionOptions, this.folderUri?.fsPath, undefined);
  - const actual = this.extractVersion(lakeVersion)
  - if (actual.compare('3.0.0') >= 0) {
  - const expectedError = 'Watchdog error: Cannot read LSP request: Stream was closed\n';
  - const serveOptions = version ? ['+' + version, 'serve'] : ['serve'];
  - const rc = await testExecute(executable, serveOptions, this.folderUri?.fsPath, this.outputChannel, true, expectedError);
  - if (rc !== 0) {
  - const failover = 'Lake failed, using lean instead.'
  - console.log(failover);
  - if (this.outputChannel) this.outputChannel.appendLine(failover);
  - useLake = false;
  }
  } else {
  + // probably 'untitled'
  useLake = false;
  }
  }
  @@ -501,4 +493,29 @@ export class LeanClient implements Disposable {
  return new SemVer('0.0.0');
  }
  }
  +
  + private extractToolchainDate(v: string) : Date {
  + // leanprover/lean4:nightly-2022-02-01
  + const parts = v.split('/')
  + if (parts[0] === 'leanprover' && parts.length > 1){
  + const leanVersion = parts[1].split(':');
  + if (leanVersion[0] === 'lean4' && leanVersion.length > 1){
  + const version = leanVersion[1];
  + if (version === 'stable'){
  + return new Date(2022, 2, 1);
  + }
  + // nightly-2022-02-01
  + const dateParts = version.split('-');
  + if (dateParts[0] === 'nightly' && dateParts.length === 4){
  + try {
  + return new Date(parseInt(dateParts[1]),
  + parseInt(dateParts[2]) - 1,
  + parseInt(dateParts[3]));
  +
  + } catch {}
  + }
  + }
  + }
  + return new Date(1995, 1, 1); // unknown, so probably an old build.
  + }
  }
  