From e0b209c4bed388253dd3ee87e5d144066fcc99e5 Mon Sep 17 00:00:00 2001
From: mhuisi <mhuisi@protonmail.com>
Date: Thu, 4 Aug 2022 19:13:40 +0200
Subject: [PATCH 1/4] fix: avoid coercion in macro

---
 Cli/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cli/Basic.lean b/Cli/Basic.lean
index 47954ef..e1cd017 100644
--- a/Cli/Basic.lean
+++ b/Cli/Basic.lean
@@ -791,7 +791,7 @@ section Macro
       if flag[1].isNone then
         (quote (none : Option String), expandIdentLiterally flag[0])
       else
-        (expandIdentLiterally flag[0], expandIdentLiterally flag[1][1])
+        (← `(some $(expandIdentLiterally flag[0])), expandIdentLiterally flag[1][1])
     let type        := if flag[2].isNone then ← `(Unit) else flag[2][1]
     let description := flag[4]
     `(Flag.mk $shortName $longName $description $type)

From 2245a1dda89cbd3e0340527b8682015b99bcec03 Mon Sep 17 00:00:00 2001
From: mhuisi <mhuisi@protonmail.com>
Date: Thu, 21 Sep 2023 10:52:36 +0200
Subject: [PATCH 2/4] chore: update toolchain to first stable release

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index f42156f..f0a6d66 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-08-23
+leanprover/lean4:v4.0.0

From be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5 Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Wed, 6 Mar 2024 09:29:38 +0100
Subject: [PATCH 3/4] doc: link to lake in lean4 in README

Closes #17
---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 8370a1e..4c23419 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 # lean4-cli
 ## Usage
-See [the documentation of Lake](https://github.com/leanprover/lake).
+See [the documentation of Lake](https://github.com/leanprover/lean4/blob/master/src/lake/README.md).
 
 Use one of the following for the `<tag>` in the dependency source `Source.git "https://github.com/leanprover/lean4-cli.git" "<tag>"`:
 - `main` if you want to stay in sync with Lean 4 stable releases. The `main` branch will contain a working version of lean4-cli for the most recent Lean 4 stable release.

From f9054125e9ab4f9cc3ea9f7ce6cb0ad3c18cdd06 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 4 Nov 2024 12:08:02 +1100
Subject: [PATCH 4/4] chore: adaptations for v4.14.0-rc1

---
 Cli/Basic.lean | 8 ++++----
 lean-toolchain | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Cli/Basic.lean b/Cli/Basic.lean
index b12f2d3..a3e50f4 100644
--- a/Cli/Basic.lean
+++ b/Cli/Basic.lean
@@ -256,7 +256,7 @@ section Configuration
     parse? s := do
       if s == ".lean" then
         none
-      let name := 
+      let name :=
         if s.endsWith ".lean" then
           let pathComponents := (s : FilePath).withExtension "" |>.components
           pathComponents.foldl .mkStr .anonymous
@@ -360,7 +360,7 @@ section Configuration
     -/
     structure Flag where
       /-- Associated flag meta-data. -/
-      flag  : Flag
+      flag  : Cli.Flag
       /-- Parsed value that was validated and conforms to `flag.type`. -/
       value : String
       deriving Inhabited, BEq, Repr
@@ -393,7 +393,7 @@ section Configuration
     -/
     structure Arg where
       /-- Associated argument meta-data. -/
-      arg   : Arg
+      arg   : Cli.Arg
       /-- Parsed value that was validated and conforms to `arg.type`. -/
       value : String
       deriving Inhabited, BEq, Repr
@@ -1630,4 +1630,4 @@ section IO
   end Cmd
 end IO
 
-end Cli
\ No newline at end of file
+end Cli
diff --git a/lean-toolchain b/lean-toolchain
index 4ef27c4..0bef727 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.9.0
+leanprover/lean4:v4.14.0-rc1