src/lsp/checker/argv.bend checks

raw source on the hub · import 0xde9bb08f7de298b03207fb5797ede9a5/src/lsp/checker/argv.bend as Argv

checker/argv: the runs of bend the real checker makes, as data. Pure: the effect (bend.bend) only performs them, so LAWS.bend states over every path and every first report that each run carries --check-only, the flag that makes bend check the file and never run its main (BOLT-LSP-5; that bend honours it is BOLT-TRUST-5).

3 imports

import Base
import ../../paths.bend as Paths
import ../report.bend as Rep

Types

type Run source · line 11 · raw

Data

a run of bend: the file it is given and the flag after it

Run
```
@path:String -> @flag:String -> Run
```

Definitions

def flag source · line 15 · raw

@rr:Run -> String

the flag of a run

def run_of source · line 20 · raw

@path:String -> Run

the run that checks a file: bend <path> --check-only

def only_todos source · line 24 · raw

@ds:List<&2, 0xde9bb08f7de298b03207fb5797ede9a5/src/lsp/report.Diag> -> Bool

only the open-laws report ("N TODOs found"), and nothing else

def proof_path source · line 32 · raw

@+path:String -> String

the PROOF.bend beside a LAWS.bend

def followup source · line 39 · raw

@+ds:List<&2, 0xde9bb08f7de298b03207fb5797ede9a5/src/lsp/report.Diag> -> @+path:String -> Maybe<&2, Run>

By convention LAWS.bend states its laws as open claims and PROOF.bend, beside it, fills them: alone, LAWS.bend always has TODOs. They are an error only while PROOF.bend does not check clean, so a first report that is only the open laws of a LAWS.bend is followed by a run on that PROOF.bend