From 2705cc3e8d862f5f446660375eee1ea4dab298ea Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 5 Jun 2025 20:21:51 +1000 Subject: [PATCH 1/4] toolchain --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 1efd365..a8cce63 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.21.0-rc3 +leanprover/lean4:nightly-2025-06-05 From 88e435f7b94b7e77c2006a72bf0702750684a8fb Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 20 Oct 2025 09:57:14 +0200 Subject: [PATCH 2/4] deprecation --- Cli/Basic.lean | 2 +- lean-toolchain | 6 +----- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/Cli/Basic.lean b/Cli/Basic.lean index 55d7f7d..0daab90 100644 --- a/Cli/Basic.lean +++ b/Cli/Basic.lean @@ -88,7 +88,7 @@ section Utils wordWrappedLines.map trimTrailingSpaces |>.map fun line => Id.run do if line = "" then return "" - if line.get! 0 ≠ '\n' then + if String.Pos.Raw.get! line 0 ≠ '\n' then return line return line.drop 1 return "\n".intercalate trimmed diff --git a/lean-toolchain b/lean-toolchain index 55ddcfc..31decf5 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1,5 +1 @@ -<<<<<<< HEAD -leanprover/lean4:nightly-2025-06-05 -======= -leanprover/lean4:v4.24.0 ->>>>>>> main +leanprover/lean4:nightly-2025-10-19 From 3d95b2cf0e2abf1806db839df343b1a0e4d6849a Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Tue, 21 Oct 2025 12:57:26 +1100 Subject: [PATCH 3/4] chore: use 'module' (#56) This should not be merged to `main`, until `v4.25.0-rc1` is available. Merging into `nightly-testing` in the meantime. --- Cli.lean | 6 ++++-- Cli/Basic.lean | 22 ++++++++++++---------- Cli/Extensions.lean | 12 +++++++++--- lakefile.toml | 3 +++ lean-toolchain | 2 +- 5 files changed, 29 insertions(+), 16 deletions(-) diff --git a/Cli.lean b/Cli.lean index 418fa3a..ec8c71e 100644 --- a/Cli.lean +++ b/Cli.lean @@ -1,2 +1,4 @@ -import Cli.Basic -import Cli.Extensions \ No newline at end of file +module + +public import Cli.Basic +public import Cli.Extensions \ No newline at end of file diff --git a/Cli/Basic.lean b/Cli/Basic.lean index 0daab90..ca7583d 100644 --- a/Cli/Basic.lean +++ b/Cli/Basic.lean @@ -1,4 +1,8 @@ -import Std.Data.TreeSet +module + +public import Std.Data.TreeSet + +public section namespace Cli @@ -169,8 +173,6 @@ section Utils end Array namespace Option - def join (x : Option (Option α)) : Option α := do ←x - /-- Returns `""` if the passed `Option` is `none`, otherwise converts the contained value using a `ToString` instance. @@ -224,7 +226,7 @@ section Configuration /-- A type synonym for `Name`, which will carry a `ParseableType ModuleName` instance, supporting parsing either a module name (e.g. `Mathlib.Topology.Basic`) or a relative path to a Lean file (e.g. `Mathlib/Topology/Basic.lean`). -/ - def ModuleName := Lean.Name + @[expose] def ModuleName := Lean.Name deriving Inhabited, BEq, Repr, ToString /-- Check that a `ModuleName` has no `.num` or empty components, and is not `.anonymous`. -/ @@ -1016,17 +1018,17 @@ section Macro ("EXTENSIONS: " sepBy(term, ";", "; "))? "\n]" : term - def expandNameableStringArg (t : TSyntax `Cli.nameableStringArg) : MacroM Term := + meta def expandNameableStringArg (t : TSyntax `Cli.nameableStringArg) : MacroM Term := pure ⟨t.raw[0]⟩ - def expandLiteralIdent (t : TSyntax `Cli.literalIdent) : MacroM Term := + meta def expandLiteralIdent (t : TSyntax `Cli.literalIdent) : MacroM Term := let s := t.raw[0] if s.getKind == identKind then pure <| quote s.getId.toString else pure ⟨s⟩ - def expandRunFun (runFun : TSyntax `Cli.runFun) : MacroM Term := + meta def expandRunFun (runFun : TSyntax `Cli.runFun) : MacroM Term := match runFun with | `(Cli.runFun| VIA $run) => `($run) @@ -1034,17 +1036,17 @@ section Macro `(fun _ => pure 0) | _ => Macro.throwUnsupported - def expandPositionalArg (positionalArg : TSyntax `Cli.positionalArg) : MacroM Term := do + meta def expandPositionalArg (positionalArg : TSyntax `Cli.positionalArg) : MacroM Term := do let `(Cli.positionalArg| $name : $type; $description) := positionalArg | Macro.throwUnsupported `(Arg.mk $(← expandLiteralIdent name) $(← expandNameableStringArg description) $type) - def expandVariableArg (variableArg : TSyntax `Cli.variableArg) : MacroM Term := do + meta def expandVariableArg (variableArg : TSyntax `Cli.variableArg) : MacroM Term := do let `(Cli.variableArg| ...$name : $type; $description) := variableArg | Macro.throwUnsupported `(Arg.mk $(← expandLiteralIdent name) $(← expandNameableStringArg description) $type) - def expandFlag (flag : TSyntax `Cli.flag) : MacroM Term := do + meta def expandFlag (flag : TSyntax `Cli.flag) : MacroM Term := do let `(Cli.flag| $flagName1 $[, $flagName2]? $[ : $type]?; $description) := flag | Macro.throwUnsupported let mut shortName := quote (none : Option String) diff --git a/Cli/Extensions.lean b/Cli/Extensions.lean index 0141d3d..1ed1142 100644 --- a/Cli/Extensions.lean +++ b/Cli/Extensions.lean @@ -1,8 +1,14 @@ -import Cli.Basic +module + +public import Cli.Basic +public import Std.Data.TreeMap.Basic +public import Std.Data.TreeSet.Basic + +section namespace Cli -section Utils +public section Utils namespace Array /-- Appends those elements of `right` to `left` whose `key` is not already @@ -38,7 +44,7 @@ section Utils end Array end Utils -section Extensions +public section Extensions /-- Prepends an author name to the description of the command. -/ def author (author : String) : Extension := { extend := fun cmd => cmd.update (description := s!"{author}\n{cmd.description}") diff --git a/lakefile.toml b/lakefile.toml index f5f8d59..0fe8cbf 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -2,6 +2,9 @@ name = "Cli" defaultTargets = ["Cli"] testDriver = "CliTest" +[leanOptions] +experimental.module = true + [[lean_lib]] name = "Cli" diff --git a/lean-toolchain b/lean-toolchain index 31decf5..4208d09 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-10-19 +leanprover/lean4:nightly-2025-10-20 From d725ce72cec6d8394a8ed8712391ee4a41891420 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 18 Nov 2025 16:54:52 +1100 Subject: [PATCH 4/4] chore: bump toolchain to v4.26.0-rc1 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 4bd92b6..bd7c1fd 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.25.1 +leanprover/lean4:v4.26.0-rc1