One compile, end to end, as a function: source text in, a PipelineResult out. No process exit, no printing, no progress animation — those belong to whoever is driving.

Driver/Modules.lean's compileModule only takes a module as far as type checking, and caches that; every pass after it (well-formedness, Typed2Computable, Computable2Guarded, Guarded2Network) runs once, here, against the checked main module rather than per EXTENDS dependency. It is separate from the CLI because two consumers need it: the CLI itself, and tests/regression's runner.

inductive PipelineError : Type

Any way a compile can fail, from any stage. One type so a caller handles one thing; PipelineError.stage recovers where it came from.

• driver (e : DriverError) : PipelineError

  Anything up to and including type checking (Driver/Modules.lean).

• wellFormedness (e : WellFormednessError) : PipelineError

  A well-formedness restriction.

• computable (e : ComputableError) : PipelineError

  Typed2Computable.

• guarded (e : GuardedError) : PipelineError

  Computable2Guarded.

• network (e : G2NError) : PipelineError

  Guarded2Network.

• go (e : N2GError) : PipelineError

  Network2Go.

def PipelineError.stage : PipelineError → Stage

Which stage produced this error. The driver's own error type already distinguishes its internal stages, so this is total and exact rather than a guess from message text.

Equations

• (PipelineError.driver (DriverError.lex moduleId e)).stage = Stage.lex
• (PipelineError.driver (DriverError.parse moduleId e)).stage = Stage.parse
• (PipelineError.driver (DriverError.annotation moduleId e)).stage = Stage.annotation
• (PipelineError.driver (DriverError.desugar moduleId e)).stage = Stage.desugar
• (PipelineError.driver (DriverError.moduleNotFound name)).stage = Stage.resolve
• (PipelineError.driver (DriverError.ambiguousModule name foundAt)).stage = Stage.resolve
• (PipelineError.driver (DriverError.cyclicExtends chain)).stage = Stage.resolve
• (PipelineError.driver (DriverError.moduleNameMismatch moduleId declared expected)).stage = Stage.parse
• (PipelineError.driver (DriverError.typeCheck moduleId e)).stage = Stage.typeCheck
• (PipelineError.wellFormedness e).stage = Stage.wellFormedness
• (PipelineError.computable e).stage = Stage.computable
• (PipelineError.guarded e).stage = Stage.guarded
• (PipelineError.network e).stage = Stage.network
• (PipelineError.go e).stage = Stage.go

def PipelineError.code : PipelineError → DiagnosticCode

This error's diagnostic code, from whichever pass produced it. The same identity CompilerDiagnostic.pretty prints in error[E0042]:, available without going through the rendered text — which is what a regression fixture asserts on.

Equations

• (PipelineError.driver e).code = CompilerDiagnostic.code e
• (PipelineError.wellFormedness e).code = CompilerDiagnostic.code e
• (PipelineError.computable e).code = CompilerDiagnostic.code e
• (PipelineError.guarded e).code = CompilerDiagnostic.code e
• (PipelineError.network e).code = CompilerDiagnostic.code e
• (PipelineError.go e).code = CompilerDiagnostic.code e

def PipelineError.posOf : PipelineError → SourceSpan

Where this error points, from whichever pass produced it: the same span CompilerDiagnostic.pretty underlines. What a regression fixture asserts on when the position is the thing under test, which code and stage cannot express — an error relocated to the start of its enclosing production still carries the right code and stage.

Equations

• (PipelineError.driver e).posOf = CompilerDiagnostic.posOf e
• (PipelineError.wellFormedness e).posOf = CompilerDiagnostic.posOf e
• (PipelineError.computable e).posOf = CompilerDiagnostic.posOf e
• (PipelineError.guarded e).posOf = CompilerDiagnostic.posOf e
• (PipelineError.network e).posOf = CompilerDiagnostic.posOf e
• (PipelineError.go e).posOf = CompilerDiagnostic.posOf e

def PipelineError.render (sources : SourceRegistry) (mainLines : List String.Slice) (colored : Bool) : PipelineError → String

Rendered form of err, against the source lines it belongs to: a driver error renders against its own module's lines (an error inside an EXTENDS-ed dependency is not about the main module), looked up in sources; everything past the driver only ever concerns the main module, so it renders against mainLines. Pure — rendering a diagnostic needs no IO.

Equations

• PipelineError.render sources mainLines colored (PipelineError.driver e) = CompilerDiagnostic.pretty e ((DriverError.sourceLines sources e).getD mainLines) colored
• PipelineError.render sources mainLines colored (PipelineError.wellFormedness e) = CompilerDiagnostic.pretty e mainLines colored
• PipelineError.render sources mainLines colored (PipelineError.computable e) = CompilerDiagnostic.pretty e mainLines colored
• PipelineError.render sources mainLines colored (PipelineError.guarded e) = CompilerDiagnostic.pretty e mainLines colored
• PipelineError.render sources mainLines colored (PipelineError.network e) = CompilerDiagnostic.pretty e mainLines colored
• PipelineError.render sources mainLines colored (PipelineError.go e) = CompilerDiagnostic.pretty e mainLines colored

inductive PipelineWarning : Type

A compile's non-fatal diagnostics, from any stage. Mirrors PipelineError, one constructor per group of stages that can produce one: everything up to type checking reports through DriverWarning, and well-formedness through its own. The passes after it still report at MonadDiagnostic Empty ε and so cannot warn at all; each grows a constructor here on the day it can.

• driver (w : DriverWarning) : PipelineWarning

  Anything up to and including type checking (Driver/Modules.lean).

• wellFormedness (w : WellFormednessWarning) : PipelineWarning

  A well-formedness finding that does not stop the compile.

def PipelineWarning.name : PipelineWarning → String

The -W<name>/-Wno-<name> name a given warning is filtered under — forwards to whichever wrapped warning's own.

Equations

• (PipelineWarning.driver w).name = w.name
• (PipelineWarning.wellFormedness w).name = w.name

def PipelineWarning.sourceLines (registry : SourceRegistry) : PipelineWarning → Option (List String.Slice)

The source lines this warning should render against, or none to fall back to the main module's. Only a driver warning can belong to another module — everything past the driver runs on the main module alone, the same way PipelineError.render treats those errors.

Equations

• PipelineWarning.sourceLines registry (PipelineWarning.driver w) = DriverWarning.sourceLines registry w
• PipelineWarning.sourceLines registry (PipelineWarning.wellFormedness w) = none

@[implicit_reducible]

instance instCompilerDiagnosticPipelineWarningString : CompilerDiagnostic PipelineWarning String

Equations

• One or more equations did not get rendered due to their size.

structure PipelineResult : Type

Everything one compile produced: its diagnostics, how far it got, the sources it read (needed to render those diagnostics), and each stage's output for whoever wants to inspect or dump it. An artifact is none when its stage never ran — either because the compile failed earlier, or because the module has no PlusCal algorithm, in which case there is nothing for Computable2Guarded onward to do and reached stops at .computable.

• warnings : List PipelineWarning

  Warnings, in the order they were reported. Present whether or not the compile then failed.

• error : Option PipelineError

  The fatal error, if the compile failed.

• reached : Stage

  The last stage that completed.

• sources : SourceRegistry

  Every module's source by moduleId, for rendering.

• typed : Option TypedModule

  The checked module.

• computable : Option (ComputableTLAPlus.Module ComputablePlusCal.Algorithm ComputableTLAPlus.Typ)

  Typed2Computable's output.

• guarded : Option ComputableGuardedPlusCal.Algorithm

  Computable2Guarded's output.

• network : Option ComputableNetworkPlusCal.Algorithm

  Guarded2Network's output.

• go : Option String

  Network2Go's output: the whole compiled Go file, ready to write.

def PipelineResult.succeeded (r : PipelineResult) : Bool

Did the compile succeed?

Equations

• r.succeeded = r.error.isNone

structure PipelineHooks : Type

What the driver reports as it goes. Plain IO actions: a caller drives a spinner, a test runner collects them into a list, and neither needs to know the driver's monad.

• onModuleEvent : String → ModuleOutcome → IO Unit

  A module finished (or failed).

• onModuleProgress : String → IO Unit

  Work started, or resumed, on a module.

• logLine : String → IO Unit

  A line the driver wants shown now, ahead of the final result.

def runPipeline (source : String) (containingDir : Option System.FilePath) (moduleId : String) (expectedName : Option String := none) (hooks : PipelineHooks := { }) : Base PipelineResult

Compile source all the way through, reporting progress through hooks.

containingDir is where EXTENDS resolution starts looking (none when the source came from stdin, which has no directory of its own); moduleId is the key this module's source is registered under, and the one DriverErrors from it are tagged with; expectedName is what the module must call itself, i.e. its file's stem — none for stdin, which has no filename to agree with.

Never throws and never exits: every failure comes back as PipelineResult.error, tagged with the stage it came from.

Equations

• One or more equations did not get rendered due to their size.

def runPipelineIO (flags : FlagsEnv) (source : String) (containingDir : Option System.FilePath) (moduleId : String) (expectedName : Option String := none) (hooks : PipelineHooks := { }) : IO PipelineResult

runPipeline with its flags and its state supplied: one compile, self-contained, from IO. Each call starts from a fresh DriverState, so nothing — module cache, fresh-name counter, source registry — carries over between two compiles in the same process. Common/Position.lean's span map is the one piece of per-compile state that is not in DriverState, and needs none: it is process-global and grows rather than resets, which is safe for the reason its own module doc gives.

Equations

• runPipelineIO flags source containingDir moduleId expectedName hooks = (ReaderT.run (runPipeline source containingDir moduleId expectedName hooks) flags).run' { }

def PipelineResult.reportedWarnings (flags : FlagsEnv) (r : PipelineResult) : List PipelineWarning

The warnings this compile actually reports, in the order they were raised: everything a pass raised, minus what -Wno-<name> turns off.

Separate from renderWarnings because "which warnings survive -W" and "what they look like" are different questions, and more than one caller wants the first without the second — PipelineResult .warnings is deliberately the unfiltered record of what the passes raised, so anything asking whether a warning is suppressed has to apply the filter, and should not have to re-implement it.

Equations

• PipelineResult.reportedWarnings flags r = List.filter (fun (w : PipelineWarning) => flags.warnings.getD w.name true) r.warnings

def PipelineResult.renderWarnings (flags : FlagsEnv) (mainLines : List String.Slice) (r : PipelineResult) : List String

This compile's reported warnings, rendered, in the order they were raised. Each renders against its own module's source lines, falling back to mainLines. Pure: the caller decides where the lines go (Fugue.lean routes them through its spinner, the regression runner asserts on them).

Equations

• One or more equations did not get rendered due to their size.

def PipelineResult.renderError (flags : FlagsEnv) (mainLines : List String.Slice) (r : PipelineResult) : Option String

This compile's fatal error, rendered, if it failed.

Equations

• PipelineResult.renderError flags mainLines r = Option.map (PipelineError.render r.sources mainLines flags.colored) r.error

def PipelineResult.renderDiagnostics (flags : FlagsEnv) (mainLines : List String.Slice) (r : PipelineResult) : List String

Every diagnostic line this result should print, in report order: warnings first, then the error if there was one.

Equations

• PipelineResult.renderDiagnostics flags mainLines r = PipelineResult.renderWarnings flags mainLines r ++ (PipelineResult.renderError flags mainLines r).toList

def PipelineResult.renderSummary (r : PipelineResult) : Option String

The one-line account of what a successful compile produced, or none if it failed before producing a checked module.

Equations

• One or more equations did not get rendered due to their size.