Text Workflow Configuration

Display helpers, generation and corpus option records, training-log metadata, and CLI parsers for text workflows.

Causal LM Display Helpers

def TorchLean.text.tokenWindow (t : Tokenizer) (n : ℕ) (input : String) (offset padId : ℕ := 0) : List ℕ

Return a fixed-length token window from a text string.

offset = 0 is the model prompt window; offset = 1 is the usual next-token target window for causal language modeling. Missing tokens are padded with padId, matching causalLmXYOneHotMatFloat.

def TorchLean.text.decodeWindow (t : Tokenizer) (n : ℕ) (input : String) (offset padId : ℕ := 0) : String

Decode a fixed token window extracted by tokenWindow.

def TorchLean.text.escapeForDisplay (s : String) : String

Escape a short text fragment for one-line terminal output.

Display-only: this does not change tokenizer semantics. Quotes and backslashes use their usual escapes, common whitespace controls use \\n, \\r, and \\t, and every other ASCII control character is written as \\xNN. Thus byte-token predictions cannot turn a log into a binary file.

Sampling Helpers (Top-k)

structure TorchLean.text.GenerationOptions : Type

Shared text-generation flags for GPT-style examples.

• prompt : String

  Prompt used to seed autoregressive generation.

• generate : ℕ

  Number of new tokens to append.

• temperature : Float

  Softmax temperature. Must be positive.

• topK : ℕ

  Top-k cutoff. 1 gives greedy decoding.

• repeatPenalty : Float

  Penalty subtracted for repeated recent tokens. 0 disables it.

• repeatWindow : ℕ

  Number of recent tokens considered by the repeat penalty. 0 disables the window.

• seed : ℕ

  Deterministic RNG seed for sampling.

• asciiOnly : Bool

  Restrict generated ids to a model-specific ASCII allow-list.

def TorchLean.text.instReprGenerationOptions.repr : GenerationOptions → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.text.instReprGenerationOptions : Repr GenerationOptions

structure TorchLean.text.GenerationDefaults : Type

Defaults for parseGenerationOptions.

• prompt : String
• generate : ℕ
• temperature : Float
• topK : ℕ
• repeatPenalty : Float
• repeatWindow : ℕ
• seed : ℕ
• asciiOnly : Bool

def TorchLean.text.instReprGenerationDefaults.repr : GenerationDefaults → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.text.instReprGenerationDefaults : Repr GenerationDefaults

def TorchLean.text.parseAsciiOnlyFlag (exeName : String) (args : List String) : Except String (Bool × List String)

Parse --ascii-only, accepting either a bare flag or true/false value.

def TorchLean.text.parseGenerationOptions (exeName : String) (args : List String) (defaults : GenerationDefaults := { }) : Except String (GenerationOptions × List String)

Parse the generation flags shared by GPT-style examples.

The model file still owns its training/data flags. This helper only handles prompt, sampling, repeat penalty, deterministic seed, and ASCII restriction.

def TorchLean.text.GenerationOptions.toDefaults (opts : GenerationOptions) : GenerationDefaults

def TorchLean.text.GenerationOptions.parse (exeName : String) (args : List String) (defaults : GenerationOptions) : Except String (GenerationOptions × List String)

Parse generation flags using a full GenerationOptions value as defaults.

This is the public API shape used by model commands: they provide a concrete default prompt and sampling policy, and the shared parser handles the stable CLI surface.

Text Workflow Option Records

structure TorchLean.text.TextCorpusOptions : Type

Required text-corpus path plus the explicit small-data option used by local corpus trainers.

• dataFile : System.FilePath

  UTF-8 or raw-byte corpus path selected by --data-file.

• allowSmallData : Bool

  Allow local runs below the normal corpus-size floor.

def TorchLean.text.instReprTextCorpusOptions.repr : TextCorpusOptions → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.text.instReprTextCorpusOptions : Repr TextCorpusOptions

def TorchLean.text.TextCorpusOptions.parse (exeName : String) (args : List String) : Except String (TextCorpusOptions × List String)

Parse the required --data-file corpus flag and optional --allow-small-data switch.

structure TorchLean.text.TextCorpusPathOptions : Type

Optional text-corpus path selected by --data-file, with caller-supplied default.

• path : System.FilePath

  Local text corpus path.

def TorchLean.text.instReprTextCorpusPathOptions.repr : TextCorpusPathOptions → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.text.instReprTextCorpusPathOptions : Repr TextCorpusPathOptions

def TorchLean.text.TextCorpusPathOptions.parse (args : List String) (defaultPath : System.FilePath) : Except String (TextCorpusPathOptions × List String)

Parse an optional --data-file flag using the supplied default path.

structure TorchLean.text.FinetuneOptions : Type

Optional second corpus pass after the main training run.

• finetuneFile? : Option System.FilePath

  Optional corpus used for a second fine-tuning pass.

• finetuneSteps : ℕ

  Number of optimizer steps used on that second corpus when present.

@[implicit_reducible]

instance TorchLean.text.instReprFinetuneOptions : Repr FinetuneOptions

def TorchLean.text.instReprFinetuneOptions.repr : FinetuneOptions → ℕ → Std.Format

def TorchLean.text.FinetuneOptions.parse (args : List String) (defaultSteps : ℕ) : Except String (FinetuneOptions × List String)

Parse the optional --finetune-file / --finetune-steps pair.

The caller supplies the default step count so commands can reuse their main training-step default.

structure TorchLean.text.BpeCorpusOptions : Type

Optional GPT-2 BPE tokenizer bundle plus an optional bounded-text cap.

• bpeVocab? : Option System.FilePath

  Optional GPT-2 vocab.json path. Must be paired with bpeMerges?.

• bpeMerges? : Option System.FilePath

  Optional GPT-2 merges.txt path. Must be paired with bpeVocab?.

• maxChars? : Option ℕ

  Optional text-character cap for bounded local BPE runs.

@[implicit_reducible]

instance TorchLean.text.instReprBpeCorpusOptions : Repr BpeCorpusOptions

def TorchLean.text.instReprBpeCorpusOptions.repr : BpeCorpusOptions → ℕ → Std.Format

def TorchLean.text.BpeCorpusOptions.parse (args : List String) : Except String (BpeCorpusOptions × List String)

Parse the optional GPT-2 BPE tokenizer bundle.

--bpe-vocab and --bpe-merges must appear together; --max-chars is independent.

structure TorchLean.text.InteractiveOptions : Type

Shared terminal-REPL toggle used by interactive text examples.

• interactive : Bool

  Keep the trained model alive and read prompts from stdin.

@[implicit_reducible]

instance TorchLean.text.instReprInteractiveOptions : Repr InteractiveOptions

def TorchLean.text.instReprInteractiveOptions.repr : InteractiveOptions → ℕ → Std.Format

def TorchLean.text.InteractiveOptions.parse (args : List String) : Except String (InteractiveOptions × List String)

Parse the shared --interactive flag used by text examples with a terminal prompt loop.

structure TorchLean.text.PromptGenerationOptions : Type

Shared prompt plus continuation-length options for simple text-generation commands.

• prompt : String

  Prompt used for before/after reports and generation.

• generate : ℕ

  Number of generated tokens or characters after training.

@[implicit_reducible]

instance TorchLean.text.instReprPromptGenerationOptions : Repr PromptGenerationOptions

def TorchLean.text.instReprPromptGenerationOptions.repr : PromptGenerationOptions → ℕ → Std.Format

def TorchLean.text.PromptGenerationOptions.parse (args : List String) (defaults : PromptGenerationOptions) : Except String (PromptGenerationOptions × List String)

Parse the shared --prompt / --generate flags.

Text TrainLog Notes

def TorchLean.text.generationNotes (gen : GenerationOptions) (generated? : Option String := none) (extra : Array String := #[]) : Array String

TrainLog note fields for generation-capable text commands.

The stable generation surface is prompt, continuation length, temperature/top-k, repetition control, RNG seed, and ASCII-only filtering. Model commands can prepend dataset or architecture notes through extra.

def TorchLean.text.promptGenerationNotes (gen : PromptGenerationOptions) (generated? : Option String := none) (extra : Array String := #[]) : Array String

TrainLog note fields for prompt-based text commands that do not expose the full sampling surface.

def TorchLean.text.writeGenerationTrainLog (log : Training.LogDestination) (title : String) (steps : ℕ) (beforeLoss afterLoss : Float) (gen : GenerationOptions) (generated? : Option String := none) (extra : Array String := #[]) : IO Unit

Write a before/after loss log for a generation-capable text training command.

def TorchLean.text.writePromptTrainLog (log : Training.LogDestination) (title : String) (steps : ℕ) (beforeLoss afterLoss : Float) (gen : PromptGenerationOptions) (generated? : Option String := none) (extra : Array String := #[]) : IO Unit

Write a before/after loss log for a prompt-based text training command.

structure TorchLean.text.SavedParamsGenerationOptionsextends TorchLean.text.GenerationOptions : Type

Shared "load one parameter pack, then sample" option surface.

• prompt : String
• generate : ℕ
• temperature : Float
• topK : ℕ
• repeatPenalty : Float
• repeatWindow : ℕ
• seed : ℕ
• asciiOnly : Bool
• paramsPath : System.FilePath

  JSON bits checkpoint loaded before sampling starts.

@[implicit_reducible]

instance TorchLean.text.instReprSavedParamsGenerationOptions : Repr SavedParamsGenerationOptions

def TorchLean.text.instReprSavedParamsGenerationOptions.repr : SavedParamsGenerationOptions → ℕ → Std.Format

def TorchLean.text.SavedParamsGenerationOptions.parse (exeName : String) (args : List String) (defaults : GenerationOptions) : Except String (SavedParamsGenerationOptions × List String)

Parse the shared saved-parameter sampling flags used by inference-only text commands.

Text Training Option Combinators

structure TorchLean.text.WindowOptions : Type

Number of corpus windows used by a finite or cyclic text-training command.

• windows : ℕ

  Number of windows available to the training sampler.

def TorchLean.text.instReprWindowOptions.repr : WindowOptions → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.text.instReprWindowOptions : Repr WindowOptions

def TorchLean.text.WindowOptions.parse (exeName : String) (args : List String) (defaultWindows : ℕ) : Except String (WindowOptions × List String)

Parse a positive --windows value.

structure TorchLean.text.CheckpointOptions : Type

Optional parameter-checkpoint paths for text training and generation.

• loadParams? : Option System.FilePath

  Checkpoint loaded before training or generation.

• saveParams? : Option System.FilePath

  Checkpoint written after training.

@[implicit_reducible]

instance TorchLean.text.instReprCheckpointOptions : Repr CheckpointOptions

def TorchLean.text.instReprCheckpointOptions.repr : CheckpointOptions → ℕ → Std.Format

def TorchLean.text.CheckpointOptions.parse (args : List String) : Except String (CheckpointOptions × List String)

Parse --load-params and --save-params.

structure TorchLean.text.LoggedInteractiveOptionsextends TorchLean.CLI.Training.RunOptions, TorchLean.text.InteractiveOptions : Type

Logged-training options plus the terminal-REPL toggle.

• steps : ℕ
• batchSize : ℕ
• log : Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• interactive : Bool

def TorchLean.text.instReprLoggedInteractiveOptions.repr : LoggedInteractiveOptions → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.text.instReprLoggedInteractiveOptions : Repr LoggedInteractiveOptions

def TorchLean.text.mkLoggedInteractiveOptions (train : CLI.Training.RunOptions) (interactive : InteractiveOptions) : LoggedInteractiveOptions

Build the shared logged-training + interactive option record.

structure TorchLean.text.InteractiveTrainOptionsextends TorchLean.CLI.Training.OptimizerOptions, TorchLean.text.InteractiveOptions : Type

Standard training flags plus the terminal-REPL toggle.

• steps : ℕ
• batchSize : ℕ
• log : Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• lr : Float
• interactive : Bool

@[implicit_reducible]

instance TorchLean.text.instReprInteractiveTrainOptions : Repr InteractiveTrainOptions

def TorchLean.text.instReprInteractiveTrainOptions.repr : InteractiveTrainOptions → ℕ → Std.Format

def TorchLean.text.mkInteractiveTrainOptions (train : CLI.Training.OptimizerOptions) (interactive : InteractiveOptions) : InteractiveTrainOptions

Build the shared train-flags + interactive option record.

def TorchLean.text.InteractiveTrainOptions.parse (exeName : String) (args : List String) (defaultLogJson : System.FilePath) (defaultSteps : ℕ) (defaultLr : Float) (allowZeroSteps : Bool := false) : Except String (InteractiveTrainOptions × List String)

Parse the shared "train + interactive" option surface.

structure TorchLean.text.LoggedPromptInteractiveOptionsextends TorchLean.text.LoggedInteractiveOptions, TorchLean.text.PromptGenerationOptions : Type

Logged-training options for promptable interactive text commands.

• steps : ℕ
• batchSize : ℕ
• log : Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• interactive : Bool
• prompt : String
• generate : ℕ

@[implicit_reducible]

instance TorchLean.text.instReprLoggedPromptInteractiveOptions : Repr LoggedPromptInteractiveOptions

def TorchLean.text.instReprLoggedPromptInteractiveOptions.repr : LoggedPromptInteractiveOptions → ℕ → Std.Format

def TorchLean.text.mkLoggedPromptInteractiveOptions (train : CLI.Training.RunOptions) (prompt : PromptGenerationOptions) (interactive : InteractiveOptions) : LoggedPromptInteractiveOptions

Build the shared logged-training + prompt + interactive option record.

def TorchLean.text.LoggedPromptInteractiveOptions.parse (exeName : String) (args : List String) (defaultLogJson : System.FilePath) (defaultSteps : ℕ) (promptDefaults : PromptGenerationOptions) : Except String (LoggedPromptInteractiveOptions × List String)

Parse the shared "logged train + prompt + interactive" option surface.

structure TorchLean.text.CorpusLoggedPromptInteractiveOptionsextends TorchLean.text.LoggedPromptInteractiveOptions : Type

Corpus-training options for promptable text commands.

This combines the common corpus, fine-tune, BPE, prompt, logging, and interactive controls without tying them to a particular model implementation.

• steps : ℕ
• batchSize : ℕ
• log : Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• interactive : Bool
• prompt : String
• generate : ℕ
• corpus : TextCorpusOptions

  Required primary corpus path plus the small-data override.

• finetune : FinetuneOptions

  Optional second corpus pass after the main training run.

• bpe : BpeCorpusOptions

  Optional GPT-2 BPE tokenizer bundle.

@[implicit_reducible]

instance TorchLean.text.instReprCorpusLoggedPromptInteractiveOptions : Repr CorpusLoggedPromptInteractiveOptions

def TorchLean.text.instReprCorpusLoggedPromptInteractiveOptions.repr : CorpusLoggedPromptInteractiveOptions → ℕ → Std.Format

def TorchLean.text.CorpusLoggedPromptInteractiveOptions.parse (exeName : String) (args : List String) (defaultLogJson : System.FilePath) (defaultSteps : ℕ) (promptDefaults : PromptGenerationOptions) : Except String (CorpusLoggedPromptInteractiveOptions × List String)

Parse the shared "corpus + logged train + prompt + interactive + optional fine-tune/BPE" surface.

structure TorchLean.text.TrainGenerationOptionsextends TorchLean.CLI.Training.OptimizerOptions, TorchLean.text.GenerationOptions : Type

Training options for text commands that train and then sample.

• steps : ℕ
• batchSize : ℕ
• log : Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• lr : Float
• prompt : String
• generate : ℕ
• temperature : Float
• topK : ℕ
• repeatPenalty : Float
• repeatWindow : ℕ
• seed : ℕ
• asciiOnly : Bool

@[implicit_reducible]

instance TorchLean.text.instReprTrainGenerationOptions : Repr TrainGenerationOptions

def TorchLean.text.instReprTrainGenerationOptions.repr : TrainGenerationOptions → ℕ → Std.Format

def TorchLean.text.mkTrainGenerationOptions (train : CLI.Training.OptimizerOptions) (gen : GenerationOptions) : TrainGenerationOptions

Build the shared train + generation option record.

structure TorchLean.text.WindowedTrainGenerationOptionsextends TorchLean.text.TrainGenerationOptions, TorchLean.text.WindowOptions : Type

Training options for cyclic text trainers that also expose --windows.

• steps : ℕ
• batchSize : ℕ
• log : Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• lr : Float
• prompt : String
• generate : ℕ
• temperature : Float
• topK : ℕ
• repeatPenalty : Float
• repeatWindow : ℕ
• seed : ℕ
• asciiOnly : Bool
• windows : ℕ

@[implicit_reducible]

instance TorchLean.text.instReprWindowedTrainGenerationOptions : Repr WindowedTrainGenerationOptions

def TorchLean.text.instReprWindowedTrainGenerationOptions.repr : WindowedTrainGenerationOptions → ℕ → Std.Format

def TorchLean.text.mkWindowedTrainGenerationOptions (train : CLI.Training.OptimizerOptions) (gen : GenerationOptions) (window : WindowOptions) : WindowedTrainGenerationOptions

Build the shared train + generation + windows option record.

def TorchLean.text.WindowedTrainGenerationOptions.parse (exeName : String) (args : List String) (defaultLogJson : System.FilePath) (defaultSteps : ℕ) (defaultLr : Float) (defaultWindows : ℕ) (genDefaults : GenerationOptions) (allowZeroSteps : Bool := false) : Except String (WindowedTrainGenerationOptions × List String)

Parse the standard "train + generate + windows" option surface.

structure TorchLean.text.CheckpointedWindowedTrainGenerationOptionsextends TorchLean.text.WindowedTrainGenerationOptions, TorchLean.text.CheckpointOptions : Type

Training options for text commands that support save/load checkpoints.

• steps : ℕ
• batchSize : ℕ
• log : Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• lr : Float
• prompt : String
• generate : ℕ
• temperature : Float
• topK : ℕ
• repeatPenalty : Float
• repeatWindow : ℕ
• seed : ℕ
• asciiOnly : Bool
• windows : ℕ
• loadParams? : Option System.FilePath
• saveParams? : Option System.FilePath

def TorchLean.text.instReprCheckpointedWindowedTrainGenerationOptions.repr : CheckpointedWindowedTrainGenerationOptions → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.text.instReprCheckpointedWindowedTrainGenerationOptions : Repr CheckpointedWindowedTrainGenerationOptions

def TorchLean.text.mkCheckpointedWindowedTrainGenerationOptions (train : CLI.Training.OptimizerOptions) (gen : GenerationOptions) (window : WindowOptions) (checkpoint : CheckpointOptions) : CheckpointedWindowedTrainGenerationOptions

Build the shared train + generation + windows + checkpoint option record.

def TorchLean.text.CheckpointedWindowedTrainGenerationOptions.parse (exeName : String) (args : List String) (defaultLogJson : System.FilePath) (defaultSteps : ℕ) (defaultLr : Float) (defaultWindows : ℕ) (genDefaults : GenerationOptions) (allowZeroSteps : Bool := false) : Except String (CheckpointedWindowedTrainGenerationOptions × List String)

Parse the shared "train + generate + windows + checkpoint" option surface.

structure TorchLean.text.BatchedCheckpointedWindowedTrainGenerationOptionsextends TorchLean.text.CheckpointedWindowedTrainGenerationOptions : Type

Training options for text commands with generic batch and context-length controls.

• steps : ℕ
• batchSize : ℕ
• log : Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• lr : Float
• prompt : String
• generate : ℕ
• temperature : Float
• topK : ℕ
• repeatPenalty : Float
• repeatWindow : ℕ
• seed : ℕ
• asciiOnly : Bool
• windows : ℕ
• loadParams? : Option System.FilePath
• saveParams? : Option System.FilePath
• batch : ℕ

  Number of independently sampled training windows per optimizer step.

• seqLen : ℕ

  Context length in tokens or characters.

@[implicit_reducible]

instance TorchLean.text.instReprBatchedCheckpointedWindowedTrainGenerationOptions : Repr BatchedCheckpointedWindowedTrainGenerationOptions

def TorchLean.text.instReprBatchedCheckpointedWindowedTrainGenerationOptions.repr : BatchedCheckpointedWindowedTrainGenerationOptions → ℕ → Std.Format

def TorchLean.text.BatchedCheckpointedWindowedTrainGenerationOptions.parse (exeName : String) (args : List String) (defaultLogJson : System.FilePath) (defaultSteps : ℕ) (defaultLr : Float) (defaultWindows defaultBatch defaultSeqLen : ℕ) (genDefaults : GenerationOptions) (allowZeroSteps : Bool := false) : Except String (BatchedCheckpointedWindowedTrainGenerationOptions × List String)

Parse the shared "train + generate + windows + checkpoint + batch + seq-len" option surface.

structure TorchLean.text.InteractiveCheckpointedWindowedTrainGenerationOptionsextends TorchLean.text.CheckpointedWindowedTrainGenerationOptions, TorchLean.text.InteractiveOptions : Type

Training options for text commands with sampling, checkpointing, and an interactive prompt loop.

• steps : ℕ
• batchSize : ℕ
• log : Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• lr : Float
• prompt : String
• generate : ℕ
• temperature : Float
• topK : ℕ
• repeatPenalty : Float
• repeatWindow : ℕ
• seed : ℕ
• asciiOnly : Bool
• windows : ℕ
• loadParams? : Option System.FilePath
• saveParams? : Option System.FilePath
• interactive : Bool

def TorchLean.text.instReprInteractiveCheckpointedWindowedTrainGenerationOptions.repr : InteractiveCheckpointedWindowedTrainGenerationOptions → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.text.instReprInteractiveCheckpointedWindowedTrainGenerationOptions : Repr InteractiveCheckpointedWindowedTrainGenerationOptions

def TorchLean.text.mkInteractiveCheckpointedWindowedTrainGenerationOptions (train : CLI.Training.OptimizerOptions) (gen : GenerationOptions) (window : WindowOptions) (checkpoint : CheckpointOptions) (interactive : InteractiveOptions) : InteractiveCheckpointedWindowedTrainGenerationOptions

Build the full train + generation + windows + checkpoint + interactive option record.

def TorchLean.text.InteractiveCheckpointedWindowedTrainGenerationOptions.parse (exeName : String) (args : List String) (defaultLogJson : System.FilePath) (defaultSteps : ℕ) (defaultLr : Float) (defaultWindows : ℕ) (genDefaults : GenerationOptions) (allowZeroSteps : Bool := false) : Except String (InteractiveCheckpointedWindowedTrainGenerationOptions × List String)

Parse the full "train + generate + windows + checkpoint + interactive" option surface.