message: Warn users if they are not using leanpkg.
diff: @@ -77,8 +77,12 @@ export class LeanpkgService implements TaskProvider, Disposable {
  }
  checkLeanpkgPathFile() {
  - if (!fs.existsSync(this.leanpkgToml)) {
  - // TODO(gabriel): encourage users to use leanpkg
  + if (!fs.existsSync(this.leanpkgToml) && !fs.existsSync(this.leanpkgPath)) {
  + window.showWarningMessage(`
  +You are running Lean in a directory without a leanpkg.toml file, this is NOT
  +supported. Please open the directoy containing the leanpkg.toml file
  +instead. [More details
  +here](https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md)`);
  } else if (!fs.existsSync(this.leanpkgPath)) {
  this.requestLeanpkgConfigure('Lean: leanpkg.path does not exist');
  } else if (fs.statSync(this.leanpkgPath) < fs.statSync(this.leanpkgToml)) {
  