src/hub/get.bend fails

raw source on the hub · import 0x886223f5c47e4983fe57d887c034bc7f/src/hub/get.bend as Get

hub/get: a file fetched from the hub over ezhttp, or read off the disk for a file: url, and judged by hub/hub against the hash that names it. The GET lives apart from the judging because ezhttp reaches foreign code, and bend 2.0.32 fails a proof whose imports reach foreign code, so a law may import hub/hub but never this.

7 imports

import Base
import 0xf1c957a470368870a6d1d62a8c0cbe32/main.bend as Http
import 0xf1c957a470368870a6d1d62a8c0cbe32/src/client.bend as Client
import 0xf1c957a470368870a6d1d62a8c0cbe32/src/url.bend as Url
import 0xabe575924687afad4cee1a2c1194d639/main.bend as R
import ../io/file.bend as F
import ./hub.bend as Hub

Definitions

def get.reply source · line 16 · raw

@response:0xf1c957a470368870a6d1d62a8c0cbe32/src/client.Response -> String

what ezhttp answered. It folds a socket that would not open and a reply that came apart into one Err, so both are 6.

def get.http source · line 24 · raw

@url:String -> IO(String)

a url fetched over a socket

def get.file source · line 30 · raw

@+path:String -> IO(String)

a file url read off the disk

def get.scheme source · line 36 · raw

@file:Bool -> @url:String -> @path:String -> IO(String)

a url whose scheme decides where the body comes from

def get.loc source · line 44 · raw

@loc:0xf1c957a470368870a6d1d62a8c0cbe32/src/url.Loc -> @url:String -> IO(String)

a url that came apart, or the reason it did not

def get source · line 52 · raw

@+url:String -> IO(String)

the body at a url: "0" and the body, or a status and the reason

def fetch source · line 56 · raw

@+url:String -> @want:String -> IO(0x886223f5c47e4983fe57d887c034bc7f/src/hub/hub.Got)

the file at a url, accepted only when it hashes to want