cairn_atproto

Use it

With the cairn tool:

cairn add cairn_atproto@^0.2.0

Which writes cairn.toml, and the lakefile line that it keeps in step:

[dependencies]
cairn_atproto = "^0.2.0"

cairn.toml

[[require]]
name = "cairn_atproto"
scope = "iamnbutler"
version = "^0.2.0"

lean/lakefile.toml

Depends on

cairn ^0.3.0
cairn_json ^0.1.0

Versions

Version	Published	Commit	Claims	Docs
0.3.0	Oct 26, 2026	`11db1badce`	28 active5 retired	docs
0.2.0	Oct 25, 2026	`a015e7b1fc`	11 active5 retired	docs
0.1.1	Oct 25, 2026	`e7b834944a`	10 active	docs
0.1.0	Oct 25, 2026	`d2c27568e4`	10 active	docs

What changed in 0.2.0

Claims new, retired or moved since 0.1.1.

Id	Change	Kind	Claim
`cairn_atproto^5`	retired	invariant	One refresh at a time
`cairn_atproto^6`	retired	invariant	A call is sent at most twice
`cairn_atproto^7`	retired	invariant	A second send only after a successful refresh
`cairn_atproto^8`	retired	invariant	Signed out, no secret is sent
`cairn_atproto^10`	retired	assume	No Lean value holds a token
`cairn_atproto^11`	new	invariant	One refresh at a time
`cairn_atproto^12`	new	invariant	A call is sent at most twice
`cairn_atproto^13`	new	invariant	A second send only after a successful refresh
`cairn_atproto^14`	new	invariant	Signed out, no secret is sent
`cairn_atproto^15`	new	assume	No Lean value holds a token
`cairn_atproto^16`	new	move	Cancel a call

Claims in 0.2.0

Every id this package has issued, as its claims.lock held them at this version. An id never moves or changes meaning: the registry refuses a version that drops, renumbers or redefines one. The claim pages show each claim by place, with what it does and its evidence.

Id	Kind	Status	Claim
`cairn_atproto^1`	move	active	Sign in
`cairn_atproto^2`	move	active	Resume
`cairn_atproto^3`	move	active	Make a call
`cairn_atproto^4`	move	active	Sign out
`cairn_atproto^5`	invariant	retired	One refresh at a time
`cairn_atproto^6`	invariant	retired	A call is sent at most twice
`cairn_atproto^7`	invariant	retired	A second send only after a successful refresh
`cairn_atproto^8`	invariant	retired	Signed out, no secret is sent
`cairn_atproto^9`	invariant	active	A failed refresh ends the held calls
`cairn_atproto^10`	assume	retired	No Lean value holds a token
`cairn_atproto^11`	invariant	active	One refresh at a time
`cairn_atproto^12`	invariant	active	A call is sent at most twice
`cairn_atproto^13`	invariant	active	A second send only after a successful refresh
`cairn_atproto^14`	invariant	active	Signed out, no secret is sent
`cairn_atproto^15`	assume	active	No Lean value holds a token
`cairn_atproto^16`	move	active	Cancel a call