refactor: use new version info from Lean + cleanup

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
 

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)

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

Lake/LeanVersion.lean

@@ -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})"

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 :=

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})"