From 1b96c466ca5da63cd099b7642ea34276cf7fef31 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sun, 19 Dec 2021 21:59:17 -0500
Subject: [PATCH] refactor: use new version info from Lean + cleanup

---
 Lake/CLI/Help.lean       |  1 -
 Lake/CLI/Init.lean       |  5 +++--
 Lake/Config/Package.lean |  1 -
 Lake/LeanVersion.lean    | 27 ---------------------------
 Lake/Util/Git.lean       |  2 --
 Lake/Version.lean        | 18 ++++++++++++++----
 6 files changed, 17 insertions(+), 37 deletions(-)
 delete mode 100644 Lake/LeanVersion.lean

diff --git a/Lake/CLI/Help.lean b/Lake/CLI/Help.lean
index 06e5a8d21c..e9c86ffd1e 100644
--- a/Lake/CLI/Help.lean
+++ b/Lake/CLI/Help.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lake.Version
-import Lake.LeanVersion
 
 namespace Lake
 
diff --git a/Lake/CLI/Init.lean b/Lake/CLI/Init.lean
index 6995972c8b..bdd75ebebc 100644
--- a/Lake/CLI/Init.lean
+++ b/Lake/CLI/Init.lean
@@ -60,8 +60,9 @@ def initPkg (dir : FilePath) (name : String) : IO PUnit := do
   unless (← mainFile.pathExists) do
     IO.FS.writeFile mainFile <| mainFileContents libRoot
 
-  -- write current toolchain to file for `elan`
-  IO.FS.writeFile (dir / toolchainFileName) <| leanVersionString ++ "\n"
+  -- write Lean's toolchain to file (if it has one) for `elan`
+  if Lean.toolchain ≠ "" then
+    IO.FS.writeFile (dir / toolchainFileName) <| Lean.toolchain ++ "\n"
 
   -- update `.gitignore`
   let h ← IO.FS.Handle.mk (dir / ".gitignore") IO.FS.Mode.append (bin := false)
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index ecc1cfa37f..9fd8b06708 100644
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@@ -6,7 +6,6 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 import Lean.Data.Name
 import Lean.Elab.Import
 import Std.Data.HashMap
-import Lake.LeanVersion
 import Lake.Build.TargetTypes
 import Lake.Config.Glob
 import Lake.Config.Opaque
diff --git a/Lake/LeanVersion.lean b/Lake/LeanVersion.lean
deleted file mode 100644
index ba26ace91f..0000000000
--- a/Lake/LeanVersion.lean
+++ /dev/null
@@ -1,27 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
--/
-namespace Lake
-
-def leanVersionStringCore :=
-  s!"{Lean.version.major}.{Lean.version.minor}.{Lean.version.patch}"
-
-def leanOrigin := "leanprover/lean4"
-
-def leanVersionString :=
-  if Lean.version.isRelease then
-    s!"{leanOrigin}:{leanVersionStringCore}"
-  else if Lean.version.specialDesc ≠ "" then
-    s!"{leanOrigin}:{Lean.version.specialDesc}"
-  else
-    s!"{leanOrigin}:master"
-
-def uiLeanVersionString :=
-if Lean.version.isRelease then
-  leanVersionStringCore
-else if Lean.version.specialDesc ≠ "" then
-  s!"{leanVersionStringCore}-{Lean.version.specialDesc}"
-else
-  s!"master ({leanVersionStringCore})"
diff --git a/Lake/Util/Git.lean b/Lake/Util/Git.lean
index bde51c16cb..287dc4ddef 100644
--- a/Lake/Util/Git.lean
+++ b/Lake/Util/Git.lean
@@ -3,10 +3,8 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
-import Lake.LeanVersion
 
 open System
-
 namespace Lake.Git
 
 def upstreamBranch :=
diff --git a/Lake/Version.lean b/Lake/Version.lean
index 5a2eb4367a..c8abd96c53 100644
--- a/Lake/Version.lean
+++ b/Lake/Version.lean
@@ -3,14 +3,24 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.LeanVersion
 
 namespace Lake
 
 def version.major := 3
 def version.minor := 0
 def version.patch := 0
-def version.isPre := true
-def versionString := s!"{version.major}.{version.minor}.{version.patch}-pre"
+
+def version.isRelease := false
+def version.specialDesc := "pre"
+
+def versionStringCore :=
+  s!"{version.major}.{version.minor}.{version.patch}"
+
+def versionString :=
+  if version.specialDesc ≠ "" then
+    s!"{versionStringCore}-{version.specialDesc}"
+  else
+    versionStringCore
+
 def uiVersionString :=
-  s!"Lake version {versionString} (Lean version {uiLeanVersionString})"
+  s!"Lake version {versionString} (Lean version {Lean.versionString})"