inductive Target : Type

Which backend the compiler is asked to target, per the -t/--target flag.

• go : Target
• join : Target

@[implicit_reducible]

instance instReprTarget : Repr Target

Equations

• instReprTarget = { reprPrec := instReprTarget.repr }

def instReprTarget.repr : Target → ℕ → Std.Format

Equations

• instReprTarget.repr Target.go prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Target.go")).group prec✝
• instReprTarget.repr Target.join prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Target.join")).group prec✝

@[implicit_reducible]

instance instDecidableEqTarget : DecidableEq Target

Equations

• instDecidableEqTarget x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instInhabitedTarget : Inhabited Target

Equations

• instInhabitedTarget = { default := instInhabitedTarget.default }

inductive Feature : Type

A -f<name> feature toggle.

This enumeration is the only place a toggle's spelling is written: the CLI validates -f against Feature.list, and every consumer reads one through the accessor named after it (FlagsEnv.colored, FlagsEnv.progress), never through a string literal. Adding a toggle and registering it are therefore the same edit, which a hand-maintained knownFeatures array could not guarantee.

• noColor : Feature

  -fno-color: no ANSI styling in diagnostics or progress output.

• noProgress : Feature

  -fno-progress: no animated spinner, just plain lines.

@[implicit_reducible]

instance instReprFeature : Repr Feature

Equations

• instReprFeature = { reprPrec := instReprFeature.repr }

def instReprFeature.repr : Feature → ℕ → Std.Format

Equations

• instReprFeature.repr Feature.noColor prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Feature.noColor")).group prec✝
• instReprFeature.repr Feature.noProgress prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Feature.noProgress")).group prec✝

@[implicit_reducible]

instance instDecidableEqFeature : DecidableEq Feature

Equations

• instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instInhabitedFeature : Inhabited Feature

Equations

• instInhabitedFeature = { default := instInhabitedFeature.default }

def Feature.name : Feature → String

The -f<name> spelling of a toggle.

Equations

• Feature.noColor.name = "no-color"
• Feature.noProgress.name = "no-progress"

def Feature.description : Feature → String

What the toggle does, as fugue help -f lists it. Here rather than in Fugue.lean for the same reason the spelling is: a toggle added without a description could not be listed.

Equations

• Feature.noColor.description = "Turn off ANSI styling in diagnostics and progress output."
• Feature.noProgress.description = "Turn off the animated progress spinner; report plain lines instead."

def Feature.list : List Feature

Every toggle, in the order -f's help text lists them.

Equations

• Feature.list = [Feature.noColor, Feature.noProgress]

@[implicit_reducible]

instance Feature.instToString : ToString Feature

Equations

• Feature.instToString = { toString := Feature.name }

structure FlagsEnv : Type

The fully-parsed CLI flag surface, computed once by the driver from Cli.Parsed and threaded to every pass via MonadReaderOf FlagsEnv m, rather than an opaque getFlag action: flags aren't uniformly Option String (boolean -f/-W flags vs. valued -d<name>=<value> options vs. -o/-t/-I's own typed values), and the project's Std.Do.WP-based proofs need a transparent Reader effect to reason about, not an opaque one.

• debug : Std.HashMap String (Option String)

  -d<name>[:<value>] debugging options.

• features : Std.HashMap String (Option String)

  -f<name>[:<value>] feature/config toggles.

• warnings : Std.HashMap String Bool

  -W<name> / -Wno-<name> per-warning enable/disable.

• targetOptions : Std.HashMap String (Option String)

  -X<name>[:<value>] backend options. Named for the target rather than the compiler: what is valid depends on which backend -t selects.

• output : Option System.FilePath

  -o/--output.

• target : Target

  -t/--target go|join.

• searchPath : List System.FilePath

  -I <path>, module search path (may be repeated).

@[implicit_reducible]

instance instInhabitedFlagsEnv : Inhabited FlagsEnv

Equations

• instInhabitedFlagsEnv = { default := instInhabitedFlagsEnv.default }

def FlagsEnv.getDebugFlag {m : Type → Type} [Monad m] [MonadReaderOf FlagsEnv m] (name : String) : m Bool

Is -d<name> (with or without a value) present?

Equations

• FlagsEnv.getDebugFlag name = do let __do_lift ← readThe FlagsEnv pure (__do_lift.debug.contains name)

def FlagsEnv.getDebugOption {m : Type → Type} [Monad m] [MonadReaderOf FlagsEnv m] (name : String) : m (Option String)

The value attached to -d<name>=<value>, if any (also none if -d<name> was given without a value).

Equations

• FlagsEnv.getDebugOption name = do let __do_lift ← readThe FlagsEnv pure (__do_lift.debug.get? name).join

def FlagsEnv.hasFeature (flags : FlagsEnv) (f : Feature) : Bool

Is f (with or without a value) present? The non-monadic form: the CLI and the driver hold a FlagsEnv directly rather than reading one out of a monad.

Equations

• flags.hasFeature f = flags.features.contains f.name

def FlagsEnv.colored (flags : FlagsEnv) : Bool

Is ANSI styling on for this compile's output? -fno-color turns it off.

Equations

• flags.colored = !flags.hasFeature Feature.noColor

def FlagsEnv.progress (flags : FlagsEnv) : Bool

Is the animated progress spinner on? -fno-progress turns it off.

Equations

• flags.progress = !flags.hasFeature Feature.noProgress

def FlagsEnv.getFeatureFlag {m : Type → Type} [Monad m] [MonadReaderOf FlagsEnv m] (f : Feature) : m Bool

Is f (with or without a value) present?

Equations

• FlagsEnv.getFeatureFlag f = do let __do_lift ← readThe FlagsEnv pure (__do_lift.hasFeature f)

def FlagsEnv.getTargetOption {m : Type → Type} [Monad m] [MonadReaderOf FlagsEnv m] (name : String) : m (Option String)

The value attached to -X<name>=<value>, if any (also none for a valueless -X<name>).

Equations

• FlagsEnv.getTargetOption name = do let __do_lift ← readThe FlagsEnv pure (__do_lift.targetOptions.get? name).join

def FlagsEnv.hasTargetOption (flags : FlagsEnv) (name : String) : Bool

Is -X<name> (with or without a value) present? For a valueless option like go-cond, this is the whole check — getTargetOption would answer none either way, present or absent.

Equations

• flags.hasTargetOption name = flags.targetOptions.contains name

def FlagsEnv.getTargetFlag {m : Type → Type} [Monad m] [MonadReaderOf FlagsEnv m] (name : String) : m Bool

Monadic form of hasTargetOption.

Equations

• FlagsEnv.getTargetFlag name = do let __do_lift ← readThe FlagsEnv pure (__do_lift.hasTargetOption name)

def FlagsEnv.getFeatureOption {m : Type → Type} [Monad m] [MonadReaderOf FlagsEnv m] (f : Feature) : m (Option String)

The value attached to -f<name>=<value>, if any.

Equations

• FlagsEnv.getFeatureOption f = do let __do_lift ← readThe FlagsEnv pure (__do_lift.features.get? f.name).join

def FlagsEnv.isWarningEnabled {m : Type → Type} [Monad m] [MonadReaderOf FlagsEnv m] (name : String) : m Bool

Is warning name enabled? Defaults to true (warnings are on unless -Wno-<name> was given).

Equations

• FlagsEnv.isWarningEnabled name = do let __do_lift ← readThe FlagsEnv pure (__do_lift.warnings.getD name true)

There is deliberately no MonadReaderOf FlagsEnv IO instance backed by a global IO.Ref: a FlagsEnv belongs to one compile, not to the process. Driver/Pipeline.lean's runPipeline takes one and supplies it as a real ReaderT layer, so two compiles running concurrently in the same process (the regression runner does exactly this) cannot see each other's flags. The CLI builds its FlagsEnv once from Cli.Parsed and hands it over the same way.

Where -d dump-* debugging artifacts go, and how they get written. Shared because both the driver (Driver/Modules.lean, which dumps the per-module stages it runs — lex, parse, desugar, typecheck) and the pipeline (Driver/Pipeline.lean, which dumps the stages that run past the driver — computable, guarded, network, go) write them, and the two must agree on the directory.

def defaultDumpDir : System.FilePath

Default value of -ddump-dir:<path>.

Equations

• defaultDumpDir = { toString := ".fugue/debug" }

def getDumpDir {m : Type → Type} [Monad m] [MonadReaderOf FlagsEnv m] : m System.FilePath

The directory -d dump-* artifacts are written to: -ddump-dir:<path> if given, defaultDumpDir otherwise. Named like the getDebugOption/getFeatureFlag accessors above, which it is one of.

Equations

• getDumpDir = do let __do_lift ← FlagsEnv.getDebugOption "dump-dir" pure (__do_lift.elim defaultDumpDir fun (x : String) => { toString := x })

def dumpToFile {m : Type → Type} [Monad m] [MonadLiftT IO m] (content : String) (dir : System.FilePath) (name : String) : m Unit

Write a -d dump-* debugging artifact to dir/name, creating dir if needed.

Equations

• dumpToFile content dir name = do liftM (IO.FS.createDirAll dir) liftM (IO.FS.writeFile (dir / { toString := name }) content)

def dumpStage {m : Type → Type} [Monad m] [MonadReaderOf FlagsEnv m] [MonadLiftT IO m] {α : Type} [Repr α] (stage : Stage) (name : String) (value : α) : m Unit

Write value to <dump-dir>/<name>-<stage> if -d dump-<stage> was given; do nothing otherwise.

The one dump point. Every -d dump-* artifact goes through it — the per-module stages the driver runs (Driver/Modules.lean) and the stages the pipeline runs past it (Driver/Pipeline.lean) — so a stage's flag name, the file it writes and its Stage.dumpable entry cannot disagree, and Fugue.lean derives the whole -d allowlist from Stage.list.

Equations

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