~/bend-docscommunity

src/lock/lock.bend checks

raw source on the hub · import 0x886223f5c47e4983fe57d887c034bc7f/src/lock/lock.bend as Lock

lock/lock: the lock document. What a package is (its source and its files), where the ledger says each package comes from, the imports a package's sources name, and the text of ez.lock.toml, written and read back. Nix reads the lock and fetches each file as a fixed-output derivation, so bend never touches the network inside the sandbox.

A package resolves from the hub, or, when it was vendored from a repo that never published, from the git rev recorded for it. Both end up as the same BEND_LIB tree. ez.toml is the only record of where a package comes from.

Everything here is pure. Deciding the lock is lock/plan.bend's, over the World lock/world.bend describes, and reading and writing are lock/run.bend's. ez fetch reads a lock back in fetch/plan.bend.

4 imports
import Base
import ../toml/toml.bend as T
import ../ledger/manifest.bend as M
import ../pkg/pkg.bend as K

Types

type Src source · line 22 · raw

Data

where a package's bytes come from. A hub package needs nothing else; a git one pins a commit, the entry its hash was computed from, the directory inside the checkout its paths are written from, and the NAR hash nix rebuilds it by.

type Pack source · line 27 · raw

Data

a package the lock records

type Origin source · line 31 · raw

Data

a package's origin, as ez.toml records it

type Name source · line 38 · raw

Data

a <name>@<version> and the 0x name it names. The hub rules that a version never moves (EZ-TRUST-6), so once a name has named a hash the pair is a fact, and the lock records it under [names] beside the package it names, which is recorded under its hash like any hub package.

Definitions

def spec.hash source · line 42 · raw

@spec:String -> String

the 0x name an import carries, which is everything before its first /

def spec.put source · line 46 · raw

@+spec:String -> List<&2, String>

an import's package, or nothing when it names a module of this project

def specs source · line 50 · raw

@ms:List<&2, String> -> List<&2, String>

every package a list of imports names

def kids source · line 58 · raw

@srcs:List<&2, String> -> List<&2, String>

every package the sources of one package import

def named.put source · line 68 · raw

@+spec:String -> List<&2, String>

an import's <name>@<version>, or nothing when it names no package by name. A named import is a dependency, never a module of this project (EZ-HUB-3), whether or not the hub rules its name in.

def named source · line 73 · raw

@ms:List<&2, String> -> List<&2, String>

every name a list of imports names

def kids.named source · line 81 · raw

@srcs:List<&2, String> -> List<&2, String>

every name the sources of one package import

def name.at source · line 90 · raw

@hit:Bool -> @hash:String -> @rest:(@_:Unit -> String) -> String

the hash this name names when it is the one looked for, otherwise the rest's. The rest arrives as a thunk, so the first hit ends the scan.

def name.find source · line 99 · raw

@ns:List<&2, Name> -> @+nv:String -> String

the hash a table of names gives a name, the first it records for it, or "" when it records none

def name.put source · line 107 · raw

@+hash:String -> List<&2, String>

a name's hash, or nothing when the table does not resolve it

def name.hashes source · line 112 · raw

@+ns:List<&2, Name> -> @nvs:List<&2, String> -> List<&2, String>

the hashes a table gives a list of names, leaving out the ones it does not resolve

def kids.in source · line 121 · raw

@+ns:List<&2, Name> -> @+srcs:List<&2, String> -> List<&2, String>

every package the sources of one package import, by hash and by a name the table resolves

def name.one source · line 125 · raw

@+nv:String -> @+hash:String -> List<&2, Name>

a name with the hash the table gives it, or nothing when it gives none

def name.pairs source · line 129 · raw

@+ns:List<&2, Name> -> @nvs:List<&2, String> -> List<&2, Name>

each name the table resolves, with its hash; one it does not is left out

def hex.char source · line 138 · raw

@+ch:Char -> Bool

whether a hash is a package's 0x name as bend reads one out of a names file: 0x and 32 lowercase hex digits

def hex.all source · line 142 · raw

@text:String -> Bool

def hash.ok source · line 150 · raw

@+hash:String -> Bool

def name.text source · line 155 · raw

@+hash:String -> String

the text of the file bend reads a name's hash from, $BEND_LIB/names/<nv>

def name.valid source · line 160 · raw

@name:Name -> Bool

a name kept when the hub rules it in and it names a 0x hash, since that is the only pair bend would read back

def names.valid.pick source · line 164 · raw

@ok:Bool -> @+name:Name -> @rest:List<&2, Name> -> List<&2, Name>

def names.valid source · line 172 · raw

@ns:List<&2, Name> -> List<&2, Name>

the names of a list that bend would read back

def segs source · line 180 · raw

@sect:0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect -> List<&2, String>

a table's path, as segments

def is3 source · line 185 · raw

@+ss:List<&2, String> -> @first:String -> @second:String -> @third:String -> Bool

whether a table's path is these three segments

def named1 source · line 191 · raw

@+ss:List<&2, String> -> @first:String -> Bool

whether a table's path is one segment, this one

def named3 source · line 196 · raw

@+ss:List<&2, String> -> @first:String -> @third:String -> Bool

whether a table's path is three segments, headed and tailed by these, whatever the hash between them is

def at.pick source · line 201 · raw

@hit:Bool -> @sect:0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect -> @rest:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv> -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv>

the pairs of a table when it is the one asked for, otherwise the rest's

def at3 source · line 210 · raw

@ss:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect> -> @+first:String -> @+second:String -> @+third:String -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv>

the pairs of the table at this three segment path, or none

def src.go source · line 218 · raw

@git:Bool -> @+ps:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv> -> Src

a git origin keeps every key it was written with; anything else is the hub

def src_of source · line 227 · raw

@+ps:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv> -> Src

where a table says a package's bytes come from

def ledger.put source · line 234 · raw

@git:Bool -> @+dep:0x886223f5c47e4983fe57d887c034bc7f/src/ledger/manifest.Dep -> List<&2, Origin>

a ledger's dependency as an origin: the repo and rev it names, or the hub. A hub dependency is recorded too, so that a package the ledger names is told apart from one it does not, which also resolves from the hub but is not vouched for by anything a clone has.

def ledger.origins source · line 245 · raw

@ds:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/ledger/manifest.Dep> -> List<&2, Origin>

every origin a ledger's dependencies record, in the order written

def ledger.read source · line 255 · raw

@parsed:0x886223f5c47e4983fe57d887c034bc7f/src/ledger/manifest.Read -> List<&2, Origin>

every origin a ledger records. A ledger that would not parse records none, so a broken ez.toml leaves the lock exactly where it was without a guess.

def ledger.name source · line 264 · raw

@+dep:0x886223f5c47e4983fe57d887c034bc7f/src/ledger/manifest.Dep -> List<&2, Name>

a dependency's name, when the ledger records it by one

def ledger.names.of source · line 270 · raw

@ds:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/ledger/manifest.Dep> -> List<&2, Name>

every name a ledger's dependencies record, each with the hash it named when it was added

def ledger.names source · line 278 · raw

@parsed:0x886223f5c47e4983fe57d887c034bc7f/src/ledger/manifest.Read -> List<&2, Name>

every name a ledger records. One that would not parse records none.

def origin.at source · line 287 · raw

@known:Origin -> @rest:Src -> @wanted:String -> Src

this origin's source when the hash matches, otherwise whatever the rest gave

def origin source · line 292 · raw

@ds:List<&2, Origin> -> @+wanted:String -> Src

where a package comes from, which is the hub unless an origin says otherwise

def origin.hash source · line 300 · raw

@known:Origin -> String

the hash an origin is recorded under

def line.put source · line 305 · raw

@+ws:List<&2, String> -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/pkg/pkg.Item>

one <sha256> <path> line of a manifest

def manifest.files source · line 310 · raw

@ls:List<&2, String> -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/pkg/pkg.Item>

every file a manifest names

def url_of source · line 318 · raw

@+hub:String -> @+hash:String -> @at:String -> String

a url under the hub

def want source · line 323 · raw

@+hash:String -> String

bend accepts any prefix of the sha256, and a package's 0x name is the first 32 characters of its manifest's digest

def nar.why.go source · line 331 · raw

@none:Bool -> @same:Bool -> @+want:String -> @+got:String -> @+url:String -> @+rev:String -> String

why a fetched checkout is not the one the ledger pins, or "" when it is. The NAR hash is over the whole checkout, so a rev that no longer holds what it held when it was pinned is caught here, before anything is laid out. A ledger with no NAR hash has nothing to check the checkout against, and an unchecked tree is not one a lock may record.

def nar.why source · line 344 · raw

@+want:String -> @+got:String -> @+url:String -> @+rev:String -> String

def pack.hash source · line 348 · raw

@package:Pack -> String

the hash a package is recorded under

def any.step source · line 360 · raw

@here:Bool -> @rest:(@_:Unit -> Bool) -> Bool

one step of a scan that is looking for one hit. Every scan in this file wants it, so it is stated once here.

Bool.or is an ordinary function and reduces both of its sides, so a scan written with it reads the whole list even when the head answers. The rest of the scan arrives as a thunk, which is a value, and only the arm that wants it applies it; handed in as an ordinary argument it would be reduced before this def could decline it.

def known source · line 371 · raw

@ds:List<&2, Origin> -> @+wanted:String -> Bool

whether the ledger names a package. One it does not name still resolves from the hub, since the hub serves bytes by the hash they digest to, but when the hub does not have it there is nothing else to ask: nothing a clone has says where it came from, so the lock says that and stops.

def has source · line 381 · raw

@ds:List<&2, Pack> -> @+wanted:String -> Bool

whether a package is already resolved. The wanted hash is compared first, the way pkg's fresh compares a path, so a walk that passes over a hash it has is a walk whose hashes are distinct without a symmetry lemma.

def seen.holds source · line 392 · raw

@xs:List<&2, String> -> @+needle:String -> Bool

whether a name is already among the ones a walk has seen. Base's List.contains applies an erased equality, which Bend's termination check cannot see through; this scan is structural. any.step is what lets it stop at the name it was looking for instead of reading past it.

def kv source · line 401 · raw

@key:String -> @+val:String -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv>

a key worth writing, or nothing at all when its value is empty, so an absent tag leaves no trace

def src.pairs source · line 405 · raw

@source:Src -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv>

the keys a source contributes to the lock

def file.pair source · line 415 · raw

@item:0x886223f5c47e4983fe57d887c034bc7f/src/pkg/pkg.Item -> 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv

a file of a package as a "<path>" = "<sha256>" pair

def file.pairs source · line 420 · raw

@fs:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/pkg/pkg.Item> -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv>

every file of a package, in path order

def pack.sects.of source · line 429 · raw

@hash:String -> @src:Src -> @fs:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/pkg/pkg.Item> -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect>

the two tables a package is written as, from its files already in path order and each one once

def pack.sects source · line 435 · raw

@package:Pack -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect>

the two tables a package is written as

def pack.all source · line 440 · raw

@ps:List<&2, Pack> -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect>

every package, in hash order

def pack.le source · line 449 · raw

@left:Pack -> @right:Pack -> Bool

packages are written in hash order, so a lock is the same text however it was resolved

def pack.ins.put source · line 455 · raw

@le:Bool -> @item:Pack -> @head:Pack -> @tail:List<&2, Pack> -> @rest:List<&2, Pack> -> List<&2, Pack>

where a package goes among the packages already in order. The rest of the insertion is a parameter, because two defs that call each other are not allowed.

def pack.ins source · line 463 · raw

@ps:List<&2, Pack> -> @+item:Pack -> List<&2, Pack>

a package inserted into a list already in hash order

def pack.sort source · line 475 · raw

@ps:List<&2, Pack> -> List<&2, Pack>

the packages in hash order. Insertion rather than Base's List.sort: that one is a fuelled bottom-up merge sort, whose recursion Bend cannot check, so it is reported as unsafe and every proof downstream of it inherits the report. An insertion sort shrinks its list at every step, so Bend checks it, and a lock names tens of packages, not thousands.

def lock.sect source · line 486 · raw

@hub:String -> 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect

the [lock] table: what resolved the lock. The bend that ran the lock is not recorded: it is not something a clone has, and the flake pins the bend a build uses. A lock written before this that records one still reads, since nothing reads the key.

def doc source · line 492 · raw

@hub:String -> @ps:List<&2, Pack> -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect>

the lock as a document: what resolved it, then every package it resolved, in hash order. render writes its text a block at a time; that the two agree is lock/LAWS.bend's render_is_doc.

def pack.block source · line 501 · raw

@package:Pack -> 0x886223f5c47e4983fe57d887c034bc7f/src/pkg/pkg.Item

a package's two tables as one block of text, filed under its hash. The lock puts packages in hash order by sorting these blocks with K.file.sort, whose order-independence pkg proves; a second sort over packages would need that proof again, and Bend's function values are linear, so one sort by a key function applied at every comparison cannot be written. A block's path is its package's hash, so distinct hashes are distinct paths.

def pack.blocks source · line 506 · raw

@ps:List<&2, Pack> -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/pkg/pkg.Item>

every package, as its block

def block.texts source · line 514 · raw

@bs:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/pkg/pkg.Item> -> List<&2, String>

the text of every block, in the order given

def text.of source · line 525 · raw

@hub:String -> @bs:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/pkg/pkg.Item> -> @rest:List<&2, String> -> String

the lock's text: the [lock] table, each block in the order given, then the rest, assembled as ez's document text (T.render) and written as eztoml writes it (T.normal). Every part of it is fixed by the blocks' order, so the order the walk found packages in does not reach the file (EZ-DOC-2).

def render source · line 530 · raw

@hub:String -> @ps:List<&2, Pack> -> String

the lock as the text written to ez.lock.toml, its packages in hash order

def tool.pairs source · line 535 · raw

@+entry:String -> @+binary:String -> @source:0x886223f5c47e4983fe57d887c034bc7f/src/ledger/manifest.Source -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv>

the keys a pinned CLI contributes. The same names a [tools.*] section uses in ez.toml, and not the [packages.*] source table.

def tool.sect source · line 545 · raw

@pin:0x886223f5c47e4983fe57d887c034bc7f/src/ledger/manifest.Tool -> 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect

one [tools.<name>] table

def tool.sects source · line 550 · raw

@ts:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/ledger/manifest.Tool> -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect>

every pinned CLI, in the order the ledger holds them

def render.tools source · line 559 · raw

@ts:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/ledger/manifest.Tool> -> @hub:String -> @ps:List<&2, Pack> -> String

the lock with its tools after the packages. An empty tool list adds no table, so a ledger with no tools writes the lock render writes.

def name.file source · line 565 · raw

@name:Name -> 0x886223f5c47e4983fe57d887c034bc7f/src/pkg/pkg.Item

a name as the pair the [names] table writes it as, which is the shape a file of a package is written in: its <name>@<version> as a quoted key and its hash as the value

def name.files source · line 570 · raw

@ns:List<&2, Name> -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/pkg/pkg.Item>

every name, so

def names.sects source · line 581 · raw

@ns:List<&2, Name> -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect>

the [names] table: every name the lock resolved, in name order and each once, sorted and deduplicated the way a package's files are. A lock that resolved no name has no such table, so a project with no named import locks to the text it always did.

def render.names source · line 589 · raw

@ns:List<&2, Name> -> @ts:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/ledger/manifest.Tool> -> @hub:String -> @ps:List<&2, Pack> -> String

the lock with its names and then its tools after the packages

def render.pick source · line 594 · raw

@empty:Bool -> @hub:String -> @ps:List<&2, Pack> -> @ts:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/ledger/manifest.Tool> -> String

the same, told whether the tool list is empty

def lock.pairs source · line 602 · raw

@ss:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect> -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv>

the [lock] table of a lock that was read

def lock.hub source · line 610 · raw

@ss:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect> -> String

the hub a lock was resolved against

def names.pairs source · line 614 · raw

@ss:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect> -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv>

the [names] table of a lock that was read

def pair.name source · line 622 · raw

@kv:0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv -> Name

a pair of the [names] table as a name

def pair.names source · line 627 · raw

@ps:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv> -> List<&2, Name>

every pair of the [names] table, as names

def names source · line 635 · raw

@+ss:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect> -> List<&2, Name>

every name a lock records, in the order its table holds them

def names.read source · line 640 · raw

@text:String -> List<&2, Name>

every name a lock's text records that bend would read back. A lock that does not parse records none.

def hash.put source · line 644 · raw

@hit:Bool -> @sect:0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect -> @rest:List<&2, String> -> List<&2, String>

every hash a lock records, one per [packages."<hash>".files] table

def hashes source · line 653 · raw

@ss:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect> -> List<&2, String>

every hash a lock records

def pair.file source · line 661 · raw

@kv:0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv -> 0x886223f5c47e4983fe57d887c034bc7f/src/pkg/pkg.Item

a pair of a files table as a file

def pair.files source · line 666 · raw

@ps:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Kv> -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/pkg/pkg.Item>

every pair of a files table, as files

def pack_of source · line 674 · raw

@+ss:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect> -> @+key:String -> Pack

the package a lock records under this hash

def packs.at source · line 679 · raw

@+ss:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect> -> @hs:List<&2, String> -> List<&2, Pack>

every package a lock records

def packs source · line 687 · raw

@+ss:List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/toml/toml.Sect> -> List<&2, Pack>

every package a lock records

def pack.src source · line 691 · raw

@package:Pack -> Src

a package's source

def pack.files source · line 696 · raw

@package:Pack -> List<&2, 0x886223f5c47e4983fe57d887c034bc7f/src/pkg/pkg.Item>

a package's files

def pack.manifest source · line 701 · raw

@package:Pack -> String

the manifest text a package is served with

def src.kind source · line 705 · raw

@source:Src -> String

where a package comes from, in a word

def src.rev source · line 713 · raw

@source:Src -> String

the commit a package is pinned to, or "" when it comes from the hub

def src.url source · line 721 · raw

@source:Src -> String

the repo a package was vendored from, or "" when it comes from the hub

def src.root source · line 729 · raw

@source:Src -> String

the directory inside a checkout a vendored package's paths are written from

def src.nar source · line 738 · raw

@source:Src -> String

the NAR hash nix rebuilds a vendored package's checkout by, or "" when it comes from the hub