refactor: lake: manifest semver & code cleanup (#4083)

Switches the manifest format to use `major.minor.patch` semantic versions. Major version increments indicate breaking changes (e.g., new required fields and semantic changes to existing fields). Minor version increments (after `0.x`) indicate backwards-compatible extensions (e.g., adding optional fields, removing fields). This change is backwards compatible. Lake will still successfully read old manifest with numeric versions. It will treat the numeric version `N` as semantic version `0.N.0`. Lake will also accept manifest versions with `-` suffixes (e.g., `x.y.z-foo`) and then ignore the suffix. This change also includes the general cleanup/refactoring of the manifest code and data structures that was part of #3174.
2024-05-24 17:32:41 -04:00 · 2024-05-24 17:32:41 -04:00 · def00d3920
commit def00d3920
parent cd16975946
11 changed files with 371 additions and 150 deletions
--- a/src/lake/Lake/Load/Main.lean
+++ b/src/lake/Lake/Load/Main.lean
@ -213,7 +213,7 @@ def Workspace.updateAndMaterialize
          if depPkg.name ≠ dep.name then
            if dep.name = .mkSimple "std" then
              let rev :=
-                match dep.manifestEntry with
+                match dep.manifestEntry.src with
                | .git (inputRev? := some rev) .. => s!" @ {repr rev}"
                | _ => ""
              logError (stdMismatchError depPkg.name.toString rev)
@ -290,7 +290,7 @@ def Workspace.materializeDeps
              s!"manifest out of date: {what} of dependency '{dep.name}' changed; " ++
              s!"use `lake update {dep.name}` to update it"
          if let .some entry := pkgEntries.find? dep.name then
-          match dep.src, entry with
+          match dep.src, entry.src with
          | .git (url := url) (rev := rev) .., .git (url := url') (inputRev? := rev')  .. =>
            if url ≠ url' then warnOutOfDate "git url"
            if rev ≠ rev' then warnOutOfDate "git revision"
--- a/src/lake/Lake/Load/Manifest.lean
+++ b/src/lake/Lake/Load/Manifest.lean
@ -6,6 +6,8 @@ Authors: Mac Malone, Gabriel Ebner
 import Lake.Util.Log
 import Lake.Util.Name
 import Lake.Util.FilePath
+import Lake.Util.JsonObject
+import Lake.Util.Version
 import Lake.Load.Config
 import Lake.Config.Workspace

@ -18,139 +20,145 @@ to create, modify, serialize, and deserialize it.

 namespace Lake

-/-- Current version of the manifest format. -/
-def Manifest.version : Nat := 7
+/--
+The current version of the manifest format.

-/-- An entry for a package stored in the manifest. -/
+Three-part semantic versions were introduced in `v1.0.0`.
+Major version increments indicate breaking changes
+(e.g., new required fields and semantic changes to existing fields).
+Minor version increments (after `0.x`) indicate backwards-compatible extensions
+(e.g., adding optional fields, removing fields).
+
+Lake supports reading manifests with versions that have `-` suffixes.
+When checking for version compatibility, Lake expects a manifest with version
+`x.y.z-foo` to have all the features of the official manifest version `x.y.z`.
+That is, Lake ignores the `-` suffix.
+
+**VERSION HISTORY**
+
+**v0.x.0** (versioned by a natural number)
+- `1`: First version
+- `2`: Adds optional `inputRev` package entry field
+- `3`: Changes entry to inductive (with `path`/`git`)
+- `4`: Adds required `packagesDir` manifest field
+- `5`: Adds optional `inherited` package entry field (and removed `opts`)
+- `6`: Adds optional package root `name` manifest field
+- `7`: `type` refactor, custom to/fromJson
+
+**v1.x.x** (versioned by a string)
+- `"1.0.0"`: Switches to a semantic versioning scheme
+-/
+@[inline] def Manifest.version : LeanVer := v!"1.0.0"
+
+/-- Manifest version `0.6.0` package entry. For backwards compatibility. -/
 inductive PackageEntryV6
 | path (name : Name) (opts : NameMap String) (inherited : Bool) (dir : FilePath)
 | git (name : Name) (opts : NameMap String) (inherited : Bool) (url : String) (rev : String)
    (inputRev? : Option String) (subDir? : Option FilePath)
 deriving FromJson, ToJson, Inhabited

-/-- An entry for a package stored in the manifest. -/
-inductive PackageEntry
+/--
+The package source for an entry in the manifest.
+Describes exactly how Lake should materialize the package.
+-/
+inductive PackageEntrySrc
  /--
  A local filesystem package. `dir` is relative to the package directory
  of the package containing the manifest.
  -/
  | path
-    (name : Name)
-    (inherited : Bool)
-    (configFile : FilePath)
-    (manifestFile? : Option FilePath)
    (dir : FilePath)
  /-- A remote Git package. -/
  | git
-    (name : Name)
-    (inherited : Bool)
-    (configFile : FilePath)
-    (manifestFile? : Option FilePath)
    (url : String)
    (rev : String)
    (inputRev? : Option String)
    (subDir? : Option FilePath)
  deriving Inhabited

+/-- An entry for a package stored in the manifest. -/
+structure PackageEntry where
+  name : Name
+  inherited : Bool
+  configFile : FilePath := defaultConfigFile
+  manifestFile? : Option FilePath := none
+  src : PackageEntrySrc
+  deriving Inhabited
+
 namespace PackageEntry

-protected def toJson : PackageEntry → Json
-| .path name inherited configFile manifestFile? dir => Json.mkObj [
-  ("type", "path"),
-  ("inherited", toJson inherited),
-  ("name", toJson name),
-  ("configFile" , toJson configFile),
-  ("manifestFile", toJson manifestFile?),
-  ("inherited", toJson inherited),
-  ("dir", toJson dir)
-]
-| .git name inherited configFile manifestFile? url rev inputRev? subDir? => Json.mkObj [
-  ("type", "git"),
-  ("inherited", toJson inherited),
-  ("name", toJson name),
-  ("configFile" , toJson configFile),
-  ("manifestFile", toJson manifestFile?),
-  ("url", toJson url),
-  ("rev", toJson rev),
-  ("inputRev", toJson inputRev?),
-  ("subDir", toJson subDir?)
-]
+protected def toJson (entry : PackageEntry) : Json :=
+  let fields := [
+    ("name", toJson entry.name),
+    ("configFile" , toJson entry.configFile),
+    ("manifestFile", toJson entry.manifestFile?),
+    ("inherited", toJson entry.inherited),
+  ]
+  let fields :=
+    match entry.src with
+    | .path  dir =>
+      ("type", "path") :: fields.append [
+        ("dir", toJson dir),
+      ]
+    | .git url rev inputRev? subDir? =>
+      ("type", "git") :: fields.append [
+        ("url", toJson url),
+        ("rev", toJson rev),
+        ("inputRev", toJson inputRev?),
+        ("subDir", toJson subDir?),
+      ]
+  Json.mkObj fields

 instance : ToJson PackageEntry := ⟨PackageEntry.toJson⟩

 protected def fromJson? (json : Json) : Except String PackageEntry := do
-  let obj ← json.getObj?
-  let type ← get obj "type"
-  let name ← get obj "name"
-  let inherited ← get obj "inherited"
-  let configFile ← getD obj "configFile" defaultConfigFile
-  let manifestFile ← getD obj "manifestFile" defaultManifestFile
-  match type with
-  | "path"=>
-    let dir ← get obj "dir"
-    return .path name inherited configFile manifestFile dir
-  | "git" =>
-    let url ← get obj "url"
-    let rev ← get obj "rev"
-    let inputRev? ← get? obj "inputRev"
-    let subDir? ← get? obj "subDir"
-    return .git name inherited configFile manifestFile url rev inputRev? subDir?
-  | _ =>
-    throw s!"unknown package entry type '{type}'"
-where
-  get {α} [FromJson α] obj prop : Except String α :=
-    match obj.find compare prop with
-    | none => throw s!"package entry missing required property '{prop}'"
-    | some val => fromJson? val |>.mapError (s!"in package entry property '{prop}': {·}")
-  get? {α} [FromJson α] obj prop : Except String (Option α) :=
-    match obj.find compare prop with
-    | none => pure none
-    | some val => fromJson? val |>.mapError (s!"in package entry property '{prop}': {·}")
-  getD {α} [FromJson α] obj prop (default : α) : Except String α :=
-    (Option.getD · default) <$> get? obj prop
+  let obj ← JsonObject.fromJson? json |>.mapError (s!"package entry: {·}")
+  let name ← obj.get "name" |>.mapError (s!"package entry: {·}")
+  try
+    let type ← obj.get "type"
+    let inherited ← obj.get "inherited"
+    let configFile ← obj.getD "configFile" defaultConfigFile
+    let manifestFile ← obj.getD "manifestFile" defaultManifestFile
+    let src : PackageEntrySrc ← id do
+      match type with
+      | "path" =>
+        let dir ← obj.get "dir"
+        return .path dir
+      | "git" =>
+        let url ← obj.get "url"
+        let rev ← obj.get "rev"
+        let inputRev? ← obj.get? "inputRev"
+        let subDir? ← obj.get? "subDir"
+        return .git url rev inputRev? subDir?
+      | _ =>
+        throw s!"unknown package entry type '{type}'"
+    return {
+      name, inherited,
+      configFile, manifestFile? := manifestFile, src
+      : PackageEntry
+    }
+  catch e =>
+    throw s!"package entry '{name}': {e}"

 instance : FromJson PackageEntry := ⟨PackageEntry.fromJson?⟩

-@[inline] protected def name : PackageEntry → Name
-| .path (name := name) .. | .git (name := name) .. => name
+@[inline] def setInherited (entry : PackageEntry) : PackageEntry :=
+  {entry with inherited := true}

-@[inline] protected def inherited : PackageEntry → Bool
-| .path (inherited := inherited) .. | .git (inherited := inherited) .. => inherited
+@[inline] def setConfigFile (path : FilePath) (entry : PackageEntry) : PackageEntry :=
+  {entry with configFile := path}

-def setInherited : PackageEntry → PackageEntry
-| .path name _ configFile manifestFile? dir =>
-  .path name true configFile manifestFile? dir
-| .git name _ configFile manifestFile? url rev inputRev? subDir? =>
-  .git name true configFile manifestFile? url rev inputRev? subDir?
+@[inline] def setManifestFile (path? : Option FilePath) (entry : PackageEntry) : PackageEntry :=
+  {entry with manifestFile? := path?}

-@[inline] protected def configFile : PackageEntry → FilePath
-| .path (configFile := configFile) .. | .git (configFile := configFile) .. => configFile
-
-@[inline] protected def manifestFile? : PackageEntry →  Option FilePath
-| .path (manifestFile? := manifestFile?) .. | .git (manifestFile? := manifestFile?) .. => manifestFile?
-
-def setConfigFile (path : FilePath) : PackageEntry → PackageEntry
-| .path name inherited _ manifestFile? dir =>
-  .path name inherited path manifestFile? dir
-| .git name inherited _ manifestFile? url rev inputRev? subDir? =>
-  .git name inherited path manifestFile? url rev inputRev? subDir?
-
-def setManifestFile (path? : Option FilePath) : PackageEntry → PackageEntry
-| .path name inherited configFile _ dir =>
-  .path name inherited configFile path? dir
-| .git name inherited configFile _ url rev inputRev? subDir? =>
-  .git name inherited configFile path? url rev inputRev? subDir?
-
-def inDirectory (pkgDir : FilePath) : PackageEntry → PackageEntry
-| .path name inherited configFile manifestFile? dir =>
-  .path name inherited configFile manifestFile? (pkgDir / dir)
-| entry => entry
+@[inline] def inDirectory (pkgDir : FilePath) (entry : PackageEntry) : PackageEntry :=
+  {entry with src := match entry.src with | .path dir => .path (pkgDir / dir) | s => s}

 def ofV6 : PackageEntryV6 → PackageEntry
 | .path name _opts inherited dir =>
-  .path name inherited defaultConfigFile none dir
+  {name, inherited, src := .path dir}
 | .git name _opts inherited url rev inputRev? subDir? =>
-  .git name inherited defaultConfigFile none url rev inputRev? subDir?
+  {name, inherited, src := .git url rev inputRev? subDir?}

 end PackageEntry

@ -169,50 +177,38 @@ def addPackage (entry : PackageEntry) (self : Manifest) : Manifest :=

 protected def toJson (self : Manifest) : Json :=
  Json.mkObj [
-    ("version", version),
+    ("version", toJson version),
    ("name", toJson self.name),
    ("lakeDir", toJson self.lakeDir),
    ("packagesDir", toJson self.packagesDir?),
-    ("packages", toJson self.packages)
+    ("packages", toJson self.packages),
  ]

 instance : ToJson Manifest := ⟨Manifest.toJson⟩

 protected def fromJson? (json : Json) : Except String Manifest := do
-  let .ok obj := json.getObj?
-    | throw "manifest not a JSON object"
-  let ver : Json ← get obj "version"
-  let .ok ver := ver.getNat?
-    | throw s!"unknown manifest version '{ver}'"
-  if ver < 5 then
+  let obj ← JsonObject.fromJson? json
+  let ver : SemVerCore ←
+    match (← obj.get "version" : Json) with
+    | (n : Nat) => pure {minor := n}
+    | (s : String) => LeanVer.parse s
+    | ver => throw s!"unknown manifest version format '{ver}'; \
+      you may need to update your 'lean-toolchain'"
+  if ver.major > 1 then
+    throw s!"manifest version '{ver}' is of a higher major version than this \
+      Lake's '{Manifest.version}'; you may need to update your 'lean-toolchain'"
+  else if ver < v!"0.5.0" then
    throw s!"incompatible manifest version '{ver}'"
-  else if ver ≤ 6 then
-    let name ← getD obj "name" Name.anonymous
-    let lakeDir ← getD obj "lakeDir" defaultLakeDir
-    let packagesDir? ← get? obj "packagesDir"
-    let pkgs : Array PackageEntryV6 ← getD obj "packages" #[]
-    return {name, lakeDir, packagesDir?, packages := pkgs.map PackageEntry.ofV6}
-  else if ver = 7 then
-    let name ← getD obj "name" Name.anonymous
-    let lakeDir ← get obj "lakeDir"
-    let packagesDir ← get obj "packagesDir"
-    let packages : Array PackageEntry ← getD obj "packages" #[]
-    return {name, lakeDir, packagesDir? := packagesDir, packages}
  else
-    throw <|
-      s!"manifest version `{ver}` is higher than this Lake's '{Manifest.version}'; " ++
-      "you may need to update your `lean-toolchain`"
-where
-  get {α} [FromJson α] obj prop : Except String α :=
-    match obj.find compare prop with
-    | none => throw s!"manifest missing required property '{prop}'"
-    | some val => fromJson? val |>.mapError (s!"in manifest property '{prop}': {·}")
-  get? {α} [FromJson α] obj prop : Except String (Option α) :=
-    match obj.find compare prop with
-    | none => pure none
-    | some val => fromJson? val |>.mapError (s!"in manifest property '{prop}': {·}")
-  getD {α} [FromJson α] obj prop (default : α) : Except String α :=
-    (Option.getD · default) <$> get? obj prop
+    let name ← obj.getD "name" Name.anonymous
+    let lakeDir ← obj.getD "lakeDir" defaultLakeDir
+    let packagesDir? ← obj.get? "packagesDir"
+    let packages ←
+      if ver < v!"0.7.0" then
+        (·.map PackageEntry.ofV6) <$> obj.getD "packages" #[]
+      else
+        obj.getD "packages" #[]
+    return {name, lakeDir, packagesDir?, packages}

 instance : FromJson Manifest := ⟨Manifest.fromJson?⟩

--- a/src/lake/Lake/Load/Materialize.lean
+++ b/src/lake/Lake/Load/Materialize.lean
@ -113,7 +113,7 @@ def Dependency.materialize (dep : Dependency) (inherited : Bool)
    return {
      relPkgDir
      remoteUrl? := none
-      manifestEntry := .path dep.name inherited defaultConfigFile none relPkgDir
+      manifestEntry := mkEntry <| .path relPkgDir
      configDep := dep
    }
  | .git url inputRev? subDir? => do
@ -127,9 +127,11 @@ def Dependency.materialize (dep : Dependency) (inherited : Bool)
    return {
      relPkgDir
      remoteUrl? := Git.filterUrl? url
-      manifestEntry := .git dep.name inherited defaultConfigFile none url rev inputRev? subDir?
+      manifestEntry := mkEntry <| .git url rev inputRev? subDir?
      configDep := dep
    }
+where
+  mkEntry src : PackageEntry := {name := dep.name, inherited, src}

 /--
 Materializes a manifest package entry, cloning and/or checking it out as necessary.
@ -137,7 +139,7 @@ Materializes a manifest package entry, cloning and/or checking it out as necessa
 def PackageEntry.materialize (manifestEntry : PackageEntry)
 (configDep : Dependency) (wsDir relPkgsDir : FilePath) (pkgUrlMap : NameMap String)
 : LogIO MaterializedDep :=
-  match manifestEntry with
+  match manifestEntry.src with
  | .path (dir := relPkgDir) .. =>
    return {
      relPkgDir
@ -145,8 +147,8 @@ def PackageEntry.materialize (manifestEntry : PackageEntry)
      manifestEntry
      configDep
    }
-  | .git name (url := url) (rev := rev) (subDir? := subDir?) .. => do
-    let sname := name.toString (escape := false)
+  | .git (url := url) (rev := rev) (subDir? := subDir?) .. => do
+    let sname := manifestEntry.name.toString (escape := false)
    let relGitDir := relPkgsDir / sname
    let gitDir := wsDir / relGitDir
    let repo := GitRepo.mk gitDir
@ -161,10 +163,10 @@ def PackageEntry.materialize (manifestEntry : PackageEntry)
        if (← repo.hasDiff) then
          logWarning s!"{sname}: repository '{repo.dir}' has local changes"
      else
-        let url := pkgUrlMap.find? name |>.getD url
+        let url := pkgUrlMap.find? manifestEntry.name |>.getD url
        updateGitRepo sname repo url rev
    else
-      let url := pkgUrlMap.find? name |>.getD url
+      let url := pkgUrlMap.find? manifestEntry.name |>.getD url
      cloneGitPkg sname repo url rev
    let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
    return {
--- a/src/lake/Lake/Util/JsonObject.lean
+++ b/src/lake/Lake/Util/JsonObject.lean
@ -0,0 +1,50 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lean.Data.Json
+
+open Lean
+
+/-! # JSON Object
+Defines a convenient wrapper type for JSON object data that makes
+indexing fields more convenient.
+-/
+
+namespace Lake
+
+/-- A JSON object (`Json.obj` data). -/
+abbrev JsonObject :=
+  RBNode String (fun _ => Json)
+
+namespace JsonObject
+
+@[inline] protected def toJson (obj : JsonObject) : Json :=
+  .obj obj
+
+instance : ToJson JsonObject := ⟨JsonObject.toJson⟩
+
+@[inline] protected def fromJson? (json : Json) : Except String JsonObject :=
+  json.getObj?
+
+instance : FromJson JsonObject := ⟨JsonObject.fromJson?⟩
+
+@[inline] nonrec def erase (obj : JsonObject) (prop : String) : JsonObject :=
+  obj.erase compare prop
+
+@[inline] def getJson? (obj : JsonObject) (prop : String) : Option Json :=
+  obj.find compare prop
+
+@[inline] def get [FromJson α] (obj : JsonObject) (prop : String) : Except String α :=
+  match obj.getJson? prop with
+  | none => throw s!"property not found: {prop}"
+  | some val => fromJson? val |>.mapError (s!"{prop}: {·}")
+
+@[inline] def get? [FromJson α] (obj : JsonObject) (prop : String) : Except String (Option α) :=
+  match obj.getJson? prop with
+  | none => pure none
+  | some val => fromJson? val |>.mapError (s!"{prop}: {·}")
+
+@[inline] def getD  [FromJson α] (obj : JsonObject) (prop : String) (default : α) : Except String α :=
+  (Option.getD · default) <$> obj.get? prop
--- a/src/lake/Lake/Util/Version.lean
+++ b/src/lake/Lake/Util/Version.lean
@ -0,0 +1,152 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lean.Elab.Eval
+
+/-! # Version
+
+This module contains useful definitions for manipulating versions.
+It also defines a `v!"<ver>"` syntax for version literals.
+-/
+
+open Lean
+
+namespace Lake
+
+/-- The major-minor-patch triple of a [SemVer](https://semver.org/). -/
+structure SemVerCore where
+  major : Nat := 0
+  minor : Nat := 0
+  patch : Nat := 0
+  deriving Inhabited, Repr, DecidableEq, Ord
+
+instance : LT SemVerCore := ltOfOrd
+instance : LE SemVerCore := leOfOrd
+instance : Min SemVerCore := minOfLe
+instance : Max SemVerCore := maxOfLe
+
+def SemVerCore.parse (ver : String) : Except String SemVerCore := do
+  try
+    match ver.split (· == '.') with
+    | [major, minor, patch] =>
+        let parseNat (v : String) (what : String) := do
+          let some v := v.toNat?
+            | throw s!"expect numeral {what} version, got '{v}'"
+          return v
+        return {
+          major := ← parseNat major "major"
+          minor := ← parseNat minor "minor"
+          patch := ← parseNat patch "patch"
+        }
+    | ps => throw s!"incorrect number of components: got {ps.length}, expected 3"
+  catch e =>
+    throw s!"invalid version core: {e}"
+
+protected def SemVerCore.toString (ver : SemVerCore) : String :=
+  s!"{ver.major}.{ver.minor}.{ver.patch}"
+
+instance : ToString SemVerCore := ⟨SemVerCore.toString⟩
+instance : ToJson SemVerCore := ⟨(·.toString)⟩
+instance : FromJson SemVerCore := ⟨(do SemVerCore.parse <| ← fromJson? ·)⟩
+
+instance : ToExpr SemVerCore where
+  toExpr ver := mkAppN (mkConst ``SemVerCore.mk)
+    #[toExpr ver.major, toExpr ver.minor, toExpr ver.patch]
+  toTypeExpr := mkConst ``SemVerCore
+
+/--
+A Lean-style semantic version.
+A major-minor-patch triple with an optional arbitrary `-` suffix.
+-/
+structure LeanVer extends SemVerCore where
+  specialDescr : String := ""
+  deriving Inhabited, Repr, DecidableEq
+
+instance : Coe LeanVer SemVerCore := ⟨LeanVer.toSemVerCore⟩
+
+@[inline] protected def LeanVer.ofSemVerCore (ver : SemVerCore) : LeanVer :=
+  {toSemVerCore := ver, specialDescr := ""}
+
+instance : Coe SemVerCore LeanVer := ⟨LeanVer.ofSemVerCore⟩
+
+protected def LeanVer.compare (a b : LeanVer) : Ordering :=
+  match compare a.toSemVerCore b.toSemVerCore with
+  | .eq =>
+    match a.specialDescr, b.specialDescr with
+    | "", "" => .eq
+    |  _, "" => .lt
+    | "",  _ => .gt
+    | a, b => compare a b
+  | ord => ord
+
+instance : Ord LeanVer := ⟨LeanVer.compare⟩
+
+instance : LT LeanVer := ltOfOrd
+instance : LE LeanVer := leOfOrd
+instance : Min LeanVer := minOfLe
+instance : Max LeanVer := maxOfLe
+
+def LeanVer.parse (ver : String) : Except String LeanVer := do
+  let sepPos := ver.find (· == '-')
+  if h : ver.atEnd sepPos then
+    SemVerCore.parse ver
+  else
+    let core ← SemVerCore.parse <| ver.extract 0 sepPos
+    let specialDescr := ver.extract (ver.next' sepPos h) ver.endPos
+    if specialDescr.isEmpty then
+      throw "invalid Lean version: '-' suffix cannot be empty"
+    return {toSemVerCore := core, specialDescr}
+
+protected def LeanVer.toString (ver : LeanVer) : String :=
+  if ver.specialDescr.isEmpty then
+    ver.toSemVerCore.toString
+  else
+    s!"{ver.toSemVerCore}-{ver.specialDescr}"
+
+instance : ToString LeanVer := ⟨LeanVer.toString⟩
+instance : ToJson LeanVer := ⟨(·.toString)⟩
+instance : FromJson LeanVer := ⟨(do LeanVer.parse <| ← fromJson? ·)⟩
+
+instance : ToExpr LeanVer where
+  toExpr ver := mkAppN (mkConst ``LeanVer.mk)
+    #[toExpr ver.toSemVerCore, toExpr ver.specialDescr]
+  toTypeExpr := mkConst ``LeanVer
+
+/-! ## Version Literals
+
+Defines the `v!"<ver>"` syntax for version literals.
+The elaborator attempts to synthesize an instance of `ToVersion` for the
+expected type and then applies it to the string literal.
+-/
+
+open Elab Term Meta
+
+/-- Parses a version from a string. -/
+class DecodeVersion (α : Type u) where
+  decodeVersion : String → Except String α
+
+export DecodeVersion (decodeVersion)
+
+instance : DecodeVersion SemVerCore := ⟨SemVerCore.parse⟩
+instance : DecodeVersion LeanVer := ⟨LeanVer.parse⟩
+
+private def toResultExpr [ToExpr α] (x : Except String α) : Except String Expr :=
+  Functor.map toExpr x
+
+/-- A Lake version literal. -/
+scoped syntax:max (name := verLit) "v!" noWs interpolatedStr(term) : term
+
+@[term_elab verLit] def elabVerLit : TermElab := fun stx expectedType? => do
+  let `(v!$v) := stx | throwUnsupportedSyntax
+  tryPostponeIfNoneOrMVar expectedType?
+  let some expectedType := expectedType?
+    | throwError "expected type is not known"
+  let ofVerT? ← mkAppM ``Except #[mkConst ``String, expectedType]
+  let ofVerE ← elabTermEnsuringType (← ``(decodeVersion s!$v)) ofVerT?
+  let resT ← mkAppM ``Except #[mkConst ``String, mkConst ``Expr]
+  let resE ← mkAppM ``toResultExpr #[ofVerE]
+  match (← unsafe evalExpr (Except String Expr) resT resE) with
+  | .ok ver => return ver
+  | .error e => throwError e
--- a/src/lake/examples/deps/bar/lake-manifest.expected.json
+++ b/src/lake/examples/deps/bar/lake-manifest.expected.json
@ -1,4 +1,4 @@
-{"version": 7,
+{"version": "1.0.0",
 "packagesDir": ".lake/packages",
 "packages":
 [{"type": "path",
--- a/src/lake/tests/manifest/lake-manifest-v1.0.0.json
+++ b/src/lake/tests/manifest/lake-manifest-v1.0.0.json
@ -0,0 +1,20 @@
+{"version": "1.0.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"type": "path",
+   "name": "foo",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "./foo",
+   "configFile": "lakefile.lean"},
+  {"url": "bar",
+   "type": "git",
+   "subDir": null,
+   "rev": "0538596b94a0510f55dc820cabd3bde41ad93c3e",
+   "name": "bar",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "«foo-bar»",
+ "lakeDir": ".lake"}
--- a/src/lake/tests/manifest/lake-manifest-v4.json
+++ b/src/lake/tests/manifest/lake-manifest-v4.json
@ -4,7 +4,7 @@
 [{"git":
   {"url": "bar",
    "subDir?": null,
-    "rev": "253735aaee71d8bb0f29ae5cfc3ce086a4b9e64f",
+    "rev": "0538596b94a0510f55dc820cabd3bde41ad93c3e",
    "name": "bar",
    "inputRev?": null}},
  {"path": {"opts": {}, "name": "foo", "inherited": false, "dir": "./foo"}}]}
--- a/src/lake/tests/manifest/lake-manifest-v5.json
+++ b/src/lake/tests/manifest/lake-manifest-v5.json
@ -4,7 +4,7 @@
 [{"git":
   {"url": "bar",
    "subDir?": null,
-    "rev": "253735aaee71d8bb0f29ae5cfc3ce086a4b9e64f",
+    "rev": "0538596b94a0510f55dc820cabd3bde41ad93c3e",
    "opts": {},
    "name": "bar",
    "inputRev?": null,
--- a/src/lake/tests/manifest/lake-manifest-v6.json
+++ b/src/lake/tests/manifest/lake-manifest-v6.json
@ -5,7 +5,7 @@
  {"git":
   {"url": "bar",
    "subDir?": null,
-    "rev": "dab525a78710d185f3d23622b143bdd837e44ab0",
+    "rev": "0538596b94a0510f55dc820cabd3bde41ad93c3e",
    "opts": {},
    "name": "bar",
    "inputRev?": null,
--- a/src/lake/tests/manifest/test.sh
+++ b/src/lake/tests/manifest/test.sh
@ -25,7 +25,7 @@ git commit -m "initial commit"
 GIT_REV=`git rev-parse HEAD`
 popd

-LATEST_VER=v7
+LATEST_VER=v1.0.0
 LOCKED_REV='0538596b94a0510f55dc820cabd3bde41ad93c3e'

 # Test an update produces the expected manifest of the latest version
@ -41,10 +41,10 @@ test_update() {

 # Test loading of a V4 manifest fails
 cp lake-manifest-v4.json lake-manifest.json
-($LAKE resolve-deps 2>&1 && exit 1 || true) | grep --color "incompatible manifest version '4'"
+($LAKE resolve-deps 2>&1 && exit 1 || true) | grep --color "incompatible manifest version '0.4.0'"

 # Test package update fails as well
-($LAKE update bar 2>&1 && exit 1 || true) | grep --color "incompatible manifest version '4'"
+($LAKE update bar 2>&1 && exit 1 || true) | grep --color "incompatible manifest version '0.4.0'"

 # Test bare update works
 test_update
@ -57,11 +57,12 @@ rm -rf .lake
 # Test successful load & update of a supported manifest version
 test_manifest() {
  cp lake-manifest-$1.json lake-manifest.json
-  sed_i "s/$2/$GIT_REV/g" lake-manifest.json
+  sed_i "s/$LOCKED_REV/$GIT_REV/g" lake-manifest.json
  $LAKE resolve-deps
  test_update
 }

-test_manifest v5 253735aaee71d8bb0f29ae5cfc3ce086a4b9e64f
-test_manifest v6 dab525a78710d185f3d23622b143bdd837e44ab0
-test_manifest v7 0538596b94a0510f55dc820cabd3bde41ad93c3e
+test_manifest v5
+test_manifest v6
+test_manifest v7
+test_manifest v1.0.0