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 (tokenizer : Tokenizer) (length : ℕ) (text : String) (offset paddingTokenId : ℕ := 0) : Tensor ℕ [length]

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 paddingTokenId, matching Data.CausalLM.oneHotSample.

Example:

-- `offset = 0` is the prompt window and `offset = 1` is its next-token target. That pair is the
-- whole of causal language-model supervision.
def prompt : Tensor Nat [8] :=
  text.tokenWindow text.Tokenizer.byte 8 "hello world"

def target : Tensor Nat [8] :=
  text.tokenWindow text.Tokenizer.byte 8 "hello world" (offset := 1)

def TorchLean.text.decodeWindow (tokenizer : Tokenizer) (length : ℕ) (text : String) (offset paddingTokenId : ℕ := 0) : String

Decode a fixed token window extracted by tokenWindow.

def TorchLean.text.escape (fragment : 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.

The argument is called fragment rather than text so it cannot shadow the text namespace inside the body; a local named text makes every text.foo spelling in scope resolve to a field access instead, which is a genuinely confusing error to read.

Sampling Helpers (Top-k)

structure TorchLean.text.GenerationOptions : Type

Shared text-generation flags for GPT-style examples.

Example:

-- `topK := 1` is greedy decoding; anything larger samples, and `seed` is what makes that sampling
-- reproducible from one run to the next.
def greedy : text.GenerationOptions :=
  { prompt := "Once upon a time"
    newTokenCount := 64
    temperature := 1.0
    topK := 1
    repeatPenalty := 0.0
    repeatWindow := 0
    seed := 0
    asciiOnly := true }

• prompt : String

  Prompt used to seed autoregressive generation.

• newTokenCount : ℕ

  Number of new tokens to append.

• temperature : Float

  Softmax temperature. Must be finite and positive for sampling; ignored by greedy decoding.

• topK : ℕ

  Top-k cutoff. 0 samples the full vocabulary; 1 gives greedy decoding.

• repeatPenalty : Float

  Finite nonnegative 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

@[instance_reducible]

instance TorchLean.text.instReprGenerationOptions : Repr GenerationOptions

def TorchLean.text.Internal.parseAsciiOnlyFlag (exeName : String) (arguments : List String) (default : Bool) : Except String (Bool × List String)

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

Internal on purpose: GenerationOptions.parse is the entry point, and parsing this flag on its own would let a command accept it without recording it in the training log.

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

Parse the generation flags shared by GPT-style examples.

The model command supplies its concrete default prompt and sampling policy. This parser owns only the stable generation flags and returns arguments belonging to the caller.

Text Workflow Option Records

structure TorchLean.text.CorpusFileOptions : 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.instReprCorpusFileOptions.repr : CorpusFileOptions → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.text.instReprCorpusFileOptions : Repr CorpusFileOptions

def TorchLean.text.CorpusFileOptions.parse (exeName : String) (arguments : List String) : Except String (CorpusFileOptions × List String)

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

structure TorchLean.text.CorpusPathOptions : Type

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

• path : System.FilePath

  Local text corpus path.

def TorchLean.text.instReprCorpusPathOptions.repr : CorpusPathOptions → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.text.instReprCorpusPathOptions : Repr CorpusPathOptions

def TorchLean.text.CorpusPathOptions.parse (arguments : List String) (defaultPath : System.FilePath) : Except String (CorpusPathOptions × 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.

@[instance_reducible]

instance TorchLean.text.instReprFinetuneOptions : Repr FinetuneOptions

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

def TorchLean.text.FinetuneOptions.parse (arguments : 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.

• vocabularyFile? : Option System.FilePath

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

• mergesFile? : Option System.FilePath

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

• maximumCharacters? : Option ℕ

  Optional text-character cap for bounded local BPE runs.

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

@[instance_reducible]

instance TorchLean.text.instReprBpeCorpusOptions : Repr BpeCorpusOptions

def TorchLean.text.BpeCorpusOptions.parse (arguments : 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.

@[instance_reducible]

instance TorchLean.text.instReprInteractiveOptions : Repr InteractiveOptions

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

def TorchLean.text.InteractiveOptions.parse (arguments : 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.

• newTokenCount : ℕ

  Number of generated tokens or characters after training.

@[instance_reducible]

instance TorchLean.text.instReprPromptGenerationOptions : Repr PromptGenerationOptions

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

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

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

Text TrainLog Notes

def TorchLean.text.Internal.generationNotes (options : GenerationOptions) (generated? : Option String := none) (extraNotes : 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.

Internal on purpose: these note arrays only make sense inside the Log.write* wrappers below, which pair them with the matching loss comparison.

def TorchLean.text.Internal.promptGenerationNotes (options : PromptGenerationOptions) (generated? : Option String := none) (extraNotes : Array String := #[]) : Array String

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

Training logs

text.Log is the whole logging surface for text commands. It lives in its own namespace so that text. completion shows tokenizers, sampling, and option parsers rather than a pair of long write*TrainLog names.

def TorchLean.text.Log.writeGeneration (destination : Training.LogDestination) (title : String) (trainingSteps : ℕ) (lossBefore lossAfter : Float) (options : GenerationOptions) (generated? : Option String := none) (extraNotes : Array String := #[]) : IO Unit

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

def TorchLean.text.Log.writePrompt (destination : Training.LogDestination) (title : String) (trainingSteps : ℕ) (lossBefore lossAfter : Float) (options : PromptGenerationOptions) (generated? : Option String := none) (extraNotes : Array String := #[]) : IO Unit

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

Text Training Option Combinators

structure TorchLean.text.WindowOptions : Type

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

• windowCount : ℕ

  Number of windows available to the training sampler.

@[instance_reducible]

instance TorchLean.text.instReprWindowOptions : Repr WindowOptions

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

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

Parse a positive --windows value.

structure TorchLean.text.CheckpointOptions : Type

Optional model-checkpoint paths for text training and generation.

• loadCheckpoint? : Option System.FilePath

  Checkpoint loaded before training or generation.

• saveCheckpoint? : Option System.FilePath

  Checkpoint written after training.

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

@[instance_reducible]

instance TorchLean.text.instReprCheckpointOptions : Repr CheckpointOptions

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

Parse --load-checkpoint and --save-checkpoint.