1	# git/exec: the git commands the interpreters run: a shallow clone of one
2	# commit, a checkout weighed for its NAR hash, HEAD on a remote, and whether
3	# one commit descends from another. What they print is read by the pure
4	# functions in git/git.bend. They live apart from those because git runs
5	# through snap's foreign effect, and bend 2.0.32 fails a proof whose imports
6	# reach foreign code, so a law may import git/git but never this.
7	import Base
8	import 0xead4c7939c9eaca8d47da53b4496b731/main.bend as R
9	import ../pkg/path.bend as P
10	import ../sha/dump.bend as Dump
11	import ../share/say.bend as Say
12	import ../share/spin.bend as Spin
13	import ./git.bend as G
14	
15	# a git command that failed stops the command, with whatever git said
16	def ran(ok: Bool, what: String, text: String) -> IO(Unit):
17	  match ok:
18	    case True{}:
19	      IO.pure(Unit, Unit{})
20	    case False{}:
21	      IO.die(Unit, 1, "ez: git " ++ what ++ ": " ++ text)
22	
23	# one git command
24	def run(what: String, args: List<&2, String>) -> IO(Unit):
25	  do IO<Unit>:
26	    +out : String <- R.exec(args)
27	    ran(R.ok(out), what, R.text(out))
28	
29	# a source as git is to read it. A ledger records a local path as it was
30	# given, relative to the project, which is the directory ez runs in, so the
31	# ledger reads the same on every clone. git reads such a path from somewhere
32	# else: a fetch from inside its work directory, and `ls-remote` from the top
33	# of any repository around it. Every git command here that is handed a source
34	# is handed this instead.
35	def anchored(+url: String) -> IO(String):
36	  do IO<String>:
37	    +here : String <- R.exec(["pwd"])
38	    return P.anchor(String.trim(R.text(here)), url)
39	
40	# the checkout a package is taken from: the pinned commit alone, at the depth
41	# of one, so a repo with a long history costs nothing to vendor. The fetch is
42	# quiet; the line above it is what a person sees while it runs.
43	def clone.say(+work: String, +url: String, +rev: String, +msg: String) -> IO(Unit):
44	  do IO<Unit>:
45	    +s : Say.Spin <- Spin.hold(msg)
46	    +from : String <- anchored(url)
47	    run("init", ["git", "init", "-q", work])
48	    run("fetch", ["git", "-C", work, "fetch", "-q", "--depth", "1", from, rev])
49	    run("checkout", ["git", "-C", work, "checkout", "-q", rev])
50	    Spin.done(s)
51	
52	# a shallow clone of one commit into `work`, with a line saying what it fetches
53	def clone(+work: String, +url: String, +rev: String) -> IO(Unit):
54	  clone.say(work, url, rev, Say.git.fetch(url))
55	
56	# the NAR hash nix rebuilds the checkout by. `fetchgit` hashes the working
57	# tree with its `.git` taken off, so that is what is weighed here and the
58	# caller strips `.git` before asking. Computed in Bend; nix is not required.
59	def nar(+work: String) -> IO(String):
60	  Dump.path(work)
61	
62	# the NAR hash of one commit. The checkout is weighed the way `fetchgit`
63	# weighs it, then removed. Nothing is laid under BEND_LIB.
64	def weigh(+url: String, +rev: String) -> IO(String):
65	  +work = ".ez/weigh-" ++ rev
66	  do IO<String>:
67	    _rm : String <- R.exec(["rm", "-rf", work])
68	    _mk : String <- R.exec(["mkdir", "-p", work])
69	    clone(work, url, rev)
70	    _dg : String <- R.exec(["rm", "-rf", work ++ "/.git"])
71	    +s : Say.Spin <- Spin.hold(Say.hashing(rev))
72	    +nh : String <- nar(work)
73	    Spin.done(s)
74	    _cl : String <- R.exec(["rm", "-rf", work])
75	    return nh
76	
77	# a remote with no HEAD is not a repo an upgrade can move
78	def remote.got(empty: Bool, +rev: String, +branch: String, +url: String) -> IO(G.Tip):
79	  match empty:
80	    case True{}:
81	      IO.die(G.Tip, 1, "ez: " ++ url ++ " has no HEAD")
82	    case False{}:
83	      IO.pure(G.Tip, G.Tip{rev, branch})
84	
85	# what ls-remote said, or why it said nothing
86	def remote.said(ok: Bool, +url: String, +text: String) -> IO(G.Tip):
87	  match ok:
88	    case False{}:
89	      IO.die(G.Tip, 1, "ez: git ls-remote " ++ url ++ ": " ++ text)
90	    case True{}:
91	      +rs = G.rows(String.lines(text))
92	      remote.got(String.is_empty(G.tip.rev(rs)), G.tip.rev(rs), G.tip.branch(rs), url)
93	
94	# HEAD on the remote: the commit the default branch tips, and that branch's
95	# name. `--symref` is what puts the branch on the line in front of the commit.
96	def remote(+url: String) -> IO(G.Tip):
97	  do IO<G.Tip>:
98	    +from : String <- anchored(url)
99	    +out : String <- R.exec(["git", "ls-remote", "--symref", from, "HEAD"])
100	    remote.said(R.ok(out), url, R.text(out))
101	
102	# a bare clone, blobs left behind. Ancestry only needs the commits. The clone
103	# is quiet; the line is what shows while it runs.
104	def clone.bare(+work: String, +url: String) -> IO(Unit):
105	  do IO<Unit>:
106	    +s : Say.Spin <- Spin.hold(Say.git.fetch(url))
107	    +from : String <- anchored(url)
108	    run("clone", ["git", "clone", "--bare", "--filter=blob:none", "-q", from, work])
109	    Spin.done(s)
110	
111	# merge-base answers 0 for a descendant, 1 for anything else, and some other
112	# status when the question itself could not be asked
113	def descendant.no(no: Bool, +text: String) -> IO(Bool):
114	  match no:
115	    case True{}:
116	      IO.pure(Bool, False{})
117	    case False{}:
118	      IO.die(Bool, 1, "ez: git merge-base: " ++ text)
119	
120	# the status, read
121	def descendant.pick(yes: Bool, no: Bool, text: String) -> IO(Bool):
122	  match yes:
123	    case True{}:
124	      IO.pure(Bool, True{})
125	    case False{}:
126	      descendant.no(no, text)
127	
128	# the status a merge-base answered with
129	def descendant.code(+code: String, +text: String) -> IO(Bool):
130	  descendant.pick(String.eq(code, "0"), String.eq(code, "1"), text)
131	
132	# the clone, the question, the clone gone. The same commit is a descendant
133	# of itself and needs no clone to say so.
134	def descendant.clone(+work: String, +url: String, +pin: String, +tip: String) -> IO(Bool):
135	  do IO<Bool>:
136	    _rm : String <- R.exec(["rm", "-rf", work])
137	    clone.bare(work, url)
138	    +out : String <- R.exec(["git", "-C", work, "merge-base", "--is-ancestor",
139	      pin, tip])
140	    _cl : String <- R.exec(["rm", "-rf", work])
141	    descendant.code(R.code(out), R.text(out))
142	
143	# whether `tip` descends from `pin`, the same commit included
144	def descendant.go(same: Bool, work: String, url: String, pin: String, tip: String) -> IO(Bool):
145	  match same:
146	    case True{}:
147	      IO.pure(Bool, True{})
148	    case False{}:
149	      descendant.clone(work, url, pin, tip)
150	
151	# whether `tip` descends from `pin`. `work` is a directory the clone may use.
152	def descendant.at(+work: String, +url: String, +pin: String, +tip: String) -> IO(Bool):
153	  descendant.go(String.eq(pin, tip), work, url, pin, tip)