Something went wrong. Try again.
A local Git merge queue with content-bound gate verdicts
Something went wrong. Try again.
11 kB · 240 lines
OCaml
at main
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241(** Settling a landing: what follows a move, from a land that has just moved or from the recovery of one a killed run left.
A land writes its intent ({!Intent}) before it moves its target. To settle the intent is to finish the landing it describes or to start it again (doc/design.md, "Recovery"): - the target at the intent's new value, or at a commit that contains it: the landing happened, and settling finishes it: it adds the landing record ({!Landing}) to the note of the landed commit under [refs/notes/mq] and keeps the pre-replay tip with a line of [refs/mq/keep]'s reflog, tidies the branch and its worktree ({!Tidy}), then commits the rest in one ref transaction ({!commit}): the branch's deletion when the tidy waits on it, the hand-out records of the worktree the intent records once it is gone, the pin by a compare-and-swap against the entry's record id, and the intent by a compare-and-swap against its own; - otherwise (the target at its old value, or moved by a writer who did not build on the new one): the landing did not happen, and settling switches back every checkout the intent names that a killed move switched, then clears the intent, the commit's only update; the entry stays queued, and its land replays on the target's current value.
Before either, a settlement that resumes a killed run releases the locks the landing's transactions take: the intent records their update lists (the target from its old value to its new one, the pin verified at the entry's record id; the commit's deletions) before any lock is taken, and the shell removes every lock the transaction would leave, each only while it holds what the transaction writes there, or none when one holds anything else ([Ref_transaction.release] in nox-git, Git's own lock protocol). A lock the release refuses is said, and left.
Every step is idempotent against what it reads, so a settlement killed in its turn is settled again by the next run. A step that meets a held lock, or that the shell could not perform, is said in a clause of the outcome and the settlement goes on: the landing stands. A release, a switch back or a commit that did not happen leaves the intent standing for the next run ({!Unsettled}), and so does a tidy stopped on what may clear ({!Tidy.field-unfinished}): a branch deletion held on another writer's lock, a removal that failed ({!Leftover}). The next round settles the landing again and tidies what is left. A replayed branch whose pre-replay commits no landing record keeps is left queued at them; a keep that did not happen leaves the intent standing too, so the next run keeps the record rather than queue those commits again ({!Leftover}).
Invariants, over every trace: - a resumed settlement emits no step before the release has answered; - the unpin compares against the intent's entry, and the clearing against the intent's own id, so a newer entry of the same name is never unpinned; - a restart writes nothing but the removal of stale locks and the clearing; - every trace ends in [Finished] or [Restarted]. *)
(** The type for lock files, as the ref store names them ([Git_eio.Repository.Ref_transaction.lock_name]). *)type lock = | Ref of Ref_name.t (** The lock of a ref: [<ref>.lock], or its stack's [tables.list.lock] in a reftable repository. *) | Table (** The lock of the ref table: [packed-refs.lock], which a deletion takes, or the common stack's [tables.list.lock], which every transaction of a shared ref takes. *)
val pp_lock : lock Fmt.t(** [pp_lock] formats a lock file as the ref it locks, or the ref table. *)
type held = { lock : lock; path : Fpath.t; (** The lock file. *) holds : Git.Hash.t option; (** The object id it holds, when it holds one. *)}(** The type for a lock file found in place. *)
type facts = { target : Commit.t option; (** The value the target holds now. *) contains : bool; (** Whether that value is the intent's new commit or contains it. *)}(** The type for what recovery read about one intent. *)
(** The type for a settlement's decision. *)type decision = | Finish (** The landing happened. *) | Restart (** The landing did not happen. *)
val decide : Intent.t -> facts -> decision(** [decide intent facts] is whether the landing [intent] describes happened: read from the target's value alone, never from its log. *)
type request = { id : Record.id; (** The intent's record id. *) intent : Intent.t; role : Tidy.role; (** What the landed branch is, for its tidy. *) decision : decision; resumed : bool; (** Whether the intent is a killed run's, found by recovery: its move's locks are released first, and a branch gone by then is one its tidy deleted. *)}(** The type for what to settle. *)
type deletion = { queued : Commit.t; (** The tip the branch must hold. *) landed : Commit.t; (** What a race's count leaves out with {!field-queued}. *)}(** The type for the deletion of the landed branch. *)
type commit = { name : Pin_name.t; (** The pin of the land that moved. *) branch : deletion option; (** The branch's deletion, which the tidy waits on. *) worktree : Fpath.t option; (** The worktree the intent records: its hand-out records go, once nothing stands at its path. *) pin : Record.id option; (** The pin at this entry, which goes with the resolver's candidate of the name, whatever that holds. *) intent : Record.id option; (** The intent, at its own id. *)}(** The type for the settlement's ref updates, made in one ref transaction. A pin, an intent or a record that holds another value by then is settled already, and is left out. *)
(** The type for the events. *)type event = | Released (** The move's locks are gone, or were never left. *) | Released_leaving of { paths : Fpath.t list } (** The move's locks are gone but these, which hold what the move did not write there: another writer's, live or killed, which stay. *) | Unswitched (** Each checkout the intent names that holds the move's new tree is switched back to the target's old one. *) | Kept (** The landing record is in the note of the landed commit, and the pre-replay tip is kept by a line of [refs/mq/keep]'s reflog. *) | Tidy of Tidy.event | Committed (** Every update of the commit is made, or was settled already. *) | Branch_kept of Tidy.event (** The branch's deletion was refused, as the tidy's event says: nothing of the commit is made. *) | Held of { lock : lock; path : Fpath.t } (** A step met a lock file another process holds. *) | Unanswered of action * Machine.unanswered
(** The type for the actions. *)and action = | Release of Intent.t (** Remove the locks the intent's move would leave, each only while it holds what that move writes there. *) | Unswitch of Intent.t (** Switch back each checkout the intent names that holds the move's new tree, from that tree to the target's old value, as [git merge --ff-only] would switch it the other way. *) | Keep of { name : Branch.t; landing : Landing.t; worktree : Fpath.t option } (** Add the landing record to the note of the landed commit under [refs/notes/mq], unless it holds it already, and keep the pre-replay tip with a line of [refs/mq/keep]'s reflog ({!Landing.kept}) that names the hand-out of [worktree], the intent's. *) | Tidy of Tidy.action | Commit of commit (** Make the commit's updates in one ref transaction, the branch's deletion only while no worktree has it out. *)
(** The type for why an intent stays for the next run. *)type standing = | Leftover (** Only the landed branch's own leftovers stand: its worktree's removal, its branch's deletion or the keep of its tip. No other land needs them, so the work goes on beside them. *) | Unsettled (** A step of the move stands: a checkout's release or switch back, or the settlement's ref transaction, its pin among its updates. No land may move past it. *)
type report = { landing : Landing.t; tidy : Tidy.report option; (** What the tidy did, once it ran. *) clauses : string list; (** What could not be done, as the outcome says it. *) standing : standing option; (** Why the intent stays for the next run, a step it covers not having happened; [None] when it is cleared. *)}(** The type for a finished landing. *)
(** The type for how a settlement ends. *)type ending = | Finished of report | Restarted of { clauses : string list; standing : standing option } (** The landing did not happen; [standing] as for {!report}. *)
include Machine.S with type event := event and type action := action and type ending := ending
val v : request -> t * action list(** [v request] is the settlement of [request], and its first actions. *)
val request : t -> request(** [request t] is what [t] settles. *)
val reading : t -> bool(** [reading t] is whether [t] waits on its tidy's read of its facts, having written nothing since its release: a run may end then and leave the intent to the next. *)
val landed : t -> bool(** [landed t] is whether the target has moved and its landing record is kept. Only the branch's tidy and the settlement's ref transaction remain. *)
val stage : t -> string(** The current settlement step for a land's progress. *)
val control : t -> string(** [control t] is the finite control of [t], in words: the shape of its request (finish or restart, whether it resumes a killed run, whether the intent names checkouts, whether the branch landed as its queued tip), its step with the {!Tidy.control} of its tidy, what its commit updates, whether the record is kept and whether the intent stays. It leaves out the names, commits, paths and the clauses said, which no transition reads to choose the next step. *)
val unjournaled_outcome : killed:bool -> Landing.t -> Outcome.t(** [unjournaled_outcome ~killed l] is the outcome recovery journals for the landing [l], whose settlement a run committed and whose landed record it never appended: [landed NAME into TARGET: N commits, journaled after a run that was killed] when a run was killed, [... that stopped before its end] otherwise. *)
val complete : report -> bool(** [complete r] is whether the landing completes its branch, as its tidy found it ({!Tidy.report}): [false] when no tidy ran. *)
val recovered_outcome : killed:bool -> report -> Outcome.t(** [recovered_outcome ~killed r] is the outcome of a landing a run finished after the run that moved its target ended before settling it: [landed NAME into TARGET: N commits, finished after a run that was killed] when that run was killed, [... that stopped before its end] when it ended with its intent standing (a lock it could not take), and the report's clauses. *)