Char-GPT (minGPT-style) Example

This example mirrors the classic "character-level GPT on a single text file" walkthrough popularized by Andrej Karpathy's minGPT/nanoGPT teaching material:

• build an alphabet (itos) from the training text,
• build a stoi tokenizer from that alphabet,
• train a small causal Transformer to predict the next character,
• sample text continuations from a prompt.

It uses TorchLean's one-hot token interface (batch × seqLen × vocab) so the whole demo stays in the same typed tensor world as the rest of the codebase.

Implementation note: training draws a fresh deterministic random window each step (minGPT-style get_batch). The --windows flag is still accepted for compatibility, but it no longer controls how many windows are precomputed.

lake build -R -K cuda=true torchlean:exe
lake exe torchlean chargpt --cuda --tiny-shakespeare --steps 500 \
  --prompt \"First Citizen:\" --generate 200

def NN.Examples.Models.Sequence.CharGpt.exeName : String

def NN.Examples.Models.Sequence.CharGpt.tinyShakespearePath : System.FilePath

def NN.Examples.Models.Sequence.CharGpt.missingTextHint : String

def NN.Examples.Models.Sequence.CharGpt.takeInputText (args : List String) : IO (String × List String)

def NN.Examples.Models.Sequence.CharGpt.buildAlphabet (s : String) : Array Char

structure NN.Examples.Models.Sequence.CharGpt.TrainOptions : Type

• base : API.Common.ModelTrainFlags
• batch : ℕ
• seqLen : ℕ
• windows : ℕ

  Accepted for CLI compatibility with fixed-window trainer entrypoints.

  CharGPT draws a fresh random window each step (minGPT-style), so training does not depend on precomputing a fixed windows array. We still accept --windows so scripts don't break.

• prompt : String
• generate : ℕ
• temperature : Float
• topK : ℕ
• repeatPenalty : Float
• repeatWindow : ℕ
• seed : ℕ
• asciiOnly : Bool
• loadParams? : Option System.FilePath
• saveParams? : Option System.FilePath

@[implicit_reducible]

instance NN.Examples.Models.Sequence.CharGpt.instReprTrainOptions : Repr TrainOptions

def NN.Examples.Models.Sequence.CharGpt.instReprTrainOptions.repr : TrainOptions → ℕ → Std.Format

def NN.Examples.Models.Sequence.CharGpt.defaultLogJson : System.FilePath

def NN.Examples.Models.Sequence.CharGpt.TrainOptions.steps (train : TrainOptions) : ℕ

def NN.Examples.Models.Sequence.CharGpt.TrainOptions.lr (train : TrainOptions) : Float

def NN.Examples.Models.Sequence.CharGpt.TrainOptions.log (train : TrainOptions) : Runtime.Training.LogDestination

def NN.Examples.Models.Sequence.CharGpt.TrainOptions.logPath (train : TrainOptions) : System.FilePath

def NN.Examples.Models.Sequence.CharGpt.parseTrainOptions (opts : Runtime.Autograd.Torch.Options) (args : List String) : Except String (TrainOptions × List String)

def NN.Examples.Models.Sequence.CharGpt.escapeCharIdsForDisplay (t : API.text.Tokenizer) (ids : List ℕ) : String

def NN.Examples.Models.Sequence.CharGpt.asciiAllowed (c : Char) : Bool

def NN.Examples.Models.Sequence.CharGpt.generateSampledFromIds (batch seqLen vocab : ℕ) (opts : Runtime.Autograd.Torch.Options) (model : API.nn.Sequential (Tensor.shapeOfDims [batch, seqLen, vocab]) (Tensor.shapeOfDims [batch, seqLen, vocab])) (params : Runtime.Autograd.Torch.ParamList Float (Runtime.Autograd.TorchLean.NN.Seq.paramShapes model)) (promptIds : List ℕ) (steps : ℕ) (temperature : Float) (topK seed repeatWindow : ℕ) (repeatPenalty : Float) (allowId : ℕ → Bool := fun (x : ℕ) => true) (padId : ℕ := 0) : IO (List ℕ)

partial def NN.Examples.Models.Sequence.CharGpt.generateSampledFromIds.loop (batch seqLen vocab : ℕ) (opts : Runtime.Autograd.Torch.Options) (model : API.nn.Sequential (Tensor.shapeOfDims [batch, seqLen, vocab]) (Tensor.shapeOfDims [batch, seqLen, vocab])) (params : Runtime.Autograd.Torch.ParamList Float (Runtime.Autograd.TorchLean.NN.Seq.paramShapes model)) (steps : ℕ) (temperature : Float) (topK seed repeatWindow : ℕ) (repeatPenalty : Float) (allowId : ℕ → Bool) (padId : ℕ) (hSeqLen : ¬seqLen = 0) (b0 : Fin batch) (ids : List ℕ) : ℕ → IO (List ℕ)

def NN.Examples.Models.Sequence.CharGpt.main (args : List String) : IO UInt32