bolt/lsp/checker/bend.bend relies on unsafe/foreign

raw source on the hub · import 0x729eecea86ea5a2cdba3a2856a313bca/bolt/lsp/checker/bend.bend as Bend

checker/bend: the real checker: runs bend on the file and reads its report

3 imports

import Base
import ./service.bend as S
import ../report.bend as Rep

Definitions

def only_todos source · line 12 · raw

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

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

def proof_path source · line 20 · raw

@+path:String -> String

the PROOF.bend beside a LAWS.bend

def settle source · line 26 · raw

@open:Bool -> @+ds:List<&2, 0x729eecea86ea5a2cdba3a2856a313bca/bolt/lsp/report.Diag> -> @path:String -> IO(List<&2, 0x729eecea86ea5a2cdba3a2856a313bca/bolt/lsp/report.Diag>)

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.

def checked source · line 37 · raw

@+ds:List<&2, 0x729eecea86ea5a2cdba3a2856a313bca/bolt/lsp/report.Diag> -> @+path:String -> IO(List<&2, 0x729eecea86ea5a2cdba3a2856a313bca/bolt/lsp/report.Diag>)

the diagnostics of a run, settled when they are only the open laws of a LAWS.bend

def check.at source · line 40 · raw

@+path:String -> IO(List<&2, 0x729eecea86ea5a2cdba3a2856a313bca/bolt/lsp/report.Diag>)

def check source · line 46 · raw

@path:String -> IO(List<&2, 0x729eecea86ea5a2cdba3a2856a313bca/bolt/lsp/report.Diag>)

the service's field takes a plain path; quantities are part of its type

def new source · line 50 · raw

0x729eecea86ea5a2cdba3a2856a313bca/bolt/lsp/checker/service.Checker

the real checker

Effects (foreign code)

effect bendcheck.exec source · line 7 · raw

@path:String -> IO(String)

everything bend <path> --check-only printed; it checks, and never runs main

foreign: bolt/lsp/checker/exec.c, bolt/lsp/checker/exec.js