-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmetal.hoon
322 lines (322 loc) · 9.85 KB
/
metal.hoon
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
::
:::: /hoon/metal/gen
::
/? 310
::
::::
!:
:- %say
|= $: {now/@da * bec/beak}
{{who/@p ~} try/_| ~}
==
::
:: we're creating an event series E whose lifecycle can be computed
:: with the urbit lifecycle formula L, `[2 [0 3] [0 2]]`. that is:
:: if E is the list of events processed by a computer in its life,
:: its final state is S, where S is nock(E L).
::
:: in practice, the first five nouns in E are: two boot formulas,
:: a hoon compiler as a nock formula, the same compiler as source,
:: and the arvo kernel as source.
::
:: after the first five special events, we enter an iterative
:: sequence of regular events which continues for the rest of the
:: computer's life. during this sequence, each state is a function
:: that, passed the next event, produces the next state.
::
:: each event is a `[date wire type data]` tuple, where `date` is a
:: 128-bit Urbit date; `wire` is an opaque path which output can
:: match to track causality; `type` is a symbol describing the type
:: of input; and `data` is input data specific to `type`.
::
:: in real life we don't actually run the lifecycle loop,
:: since real life is updated incrementally and also cares
:: about things like output. we couple to the internal
:: structure of the state machine and work directly with
:: the underlying arvo engine.
::
:: this arvo core, which is at `+7` (Lisp `cddr`) of the state
:: function (see its public interface in `sys/arvo`), gives us
:: extra features, like output, which are relevant to running
:: a real-life urbit vm, but don't affect the formal definition.
::
:: so a real-life urbit interpreter is coupled to the shape of
:: the arvo core. it becomes very hard to change this shape.
:: fortunately, it is not a very complex interface.
::
:- %noun
::
:: boot-one: lifecycle formula
::
=+ ^= boot-one
::
:: event 1 is the lifecycle formula which computes the final
:: state from the full event sequence.
::
:: the formal urbit state is always just a gate (function)
:: which, passed the next event, produces the next state.
::
=> [boot-formula=* full-sequence=*]
!= ::
:: first we use the boot formula (event 1) to set up
:: the pair of state function and main sequence. the boot
:: formula peels off the first n (currently 3) events
:: to set up the lifecycle loop.
::
=+ [state-gate main-sequence]=.*(full-sequence boot-formula)
::
:: in this lifecycle loop, we replace the state function
:: with its product, called on the next event, until
:: we run out of events.
::
|- ?@ main-sequence
state-gate
%= $
main-sequence +.main-sequence
state-gate .*(state-gate [%9 2 %10 [6 %1 -.main-sequence] %0 1])
==
::
:: boot-two: startup formula
::
=+ ^= boot-two
::
:: event 2 is the startup formula, which verifies the compiler
:: and starts the main lifecycle.
::
=> :* :: event 3: a formula producing the hoon compiler
::
compiler-formula=**
::
:: event 4: hoon compiler source, compiling to event 2
::
compiler-source=*@t
::
:: event 5: arvo kernel source
::
arvo-source=*@t
::
:: events 6..n: main sequence with normal semantics
::
main-sequence=**
==
!= :_ main-sequence
::
:: activate the compiler gate. the product of this formula
:: is smaller than the formula. so you might think we should
:: save the gate itself rather than the formula producing it.
:: but we have to run the formula at runtime, to register jets.
::
:: as always, we have to use raw nock as we have no type.
:: the gate is in fact ++ride.
::
~> %slog.[0 leaf+"1-b"]
=+ ^= compiler-gate
.*(0 compiler-formula)
::
:: compile the compiler source, producing (pair span nock).
:: the compiler ignores its input so we use a trivial span.
::
~> %slog.[0 leaf+"1-c"]
=+ ^= compiler-tool
.*(compiler-gate [%9 2 %10 [6 %1 [%noun compiler-source]] %0 1])
::
:: switch to the second-generation compiler. we want to be
:: able to generate matching reflection nouns even if the
:: language changes -- the first-generation formula will
:: generate last-generation spans for `!>`, etc.
::
~> %slog.[0 leaf+"1-d"]
=. compiler-gate .*(0 +:compiler-tool)
::
:: get the span (type) of the kernel core, which is the context
:: of the compiler gate. we just compiled the compiler,
:: so we know the span (type) of the compiler gate. its
:: context is at tree address `+>` (ie, `+7` or Lisp `cddr`).
:: we use the compiler again to infer this trivial program.
::
~> %slog.[0 leaf+"1-e"]
=+ ^= kernel-span
-:.*(compiler-gate [%9 2 %10 [6 %1 [-.compiler-tool '+>']] %0 1])
::
:: compile the arvo source against the kernel core.
::
~> %slog.[0 leaf+"1-f"]
=+ ^= kernel-tool
.*(compiler-gate [%9 2 %10 [6 %1 [kernel-span arvo-source]] %0 1])
::
:: create the arvo kernel, whose subject is the kernel core.
::
~> %slog.[0 leaf+"1-g"]
.*(+>:compiler-gate +:kernel-tool)
::
:: sys: root path to boot system, `/~me/[desk]/now/sys`
::
=+ sys=`path`/(scot %p p.bec)/[q.bec]/(scot %da now)/sys
::
:: compiler-source: hoon source file producing compiler, `sys/hoon`
::
=+ compiler-source=.^(@t %cx (welp sys /hoon/hoon))
::
:: compiler-twig: compiler as hoon expression
::
~& %metal-parsing
=+ compiler-twig=(ream compiler-source)
~& %metal-parsed
::
:: compiler-formula: compiler as nock formula
::
~& %metal-compiling
=+ compiler-formula=q:(~(mint ut %noun) %noun compiler-twig)
~& %metal-compiled
::
:: arvo-source: hoon source file producing arvo kernel, `sys/arvo`
::
=+ arvo-source=.^(@t %cx (welp sys /arvo/hoon))
::
:: main-moves: installation actions
::
=+ ^= main-moves
|^ ^- (list ovum)
:~ ::
:: configure identity
::
[[%name (scot %p who) ~] [%veal who]]
::
:: sys/zuse: standard library
::
(vent %$ /zuse)
::
:: sys/vane/ames: network
::
(vent %a /vane/ames)
::
:: sys/vane/behn: timer
::
(vent %b /vane/behn)
::
:: sys/vane/clay: revision control
::
(vent %c /vane/clay)
::
:: sys/vane/dill: console
::
(vent %d /vane/dill)
::
:: sys/vane/eyre: web
::
(vent %e /vane/eyre)
::
:: sys/vane/ford: build
::
(vent %f /vane/ford)
::
:: sys/vane/gall: applications
::
(vent %g /vane/gall)
::
:: sys/vane/jael: security
::
(vent %j /vane/jael)
::
:: legacy boot event
::
[[%$ %term '1' ~] [%boot %sith who `@uw`who &]]
::
:: userspace:
::
:: /app %gall applications
:: /gen :dojo generators
:: /lib %ford libraries
:: /mar %ford marks
:: /sur %ford structures
:: /ren %ford renderers
:: /web %eyre web content
:: /sys system files
::
(user /app /gen /lib /mar /ren /sec /sur /sys /web ~)
==
:: ::
++ user :: userspace loading
|= :: sal: all spurs to load from
::
sal/(list spur)
^- ovum
::
:: hav: all user files
::
=; hav ~& user-files+(lent hav)
[[%$ %sync ~] [%into %$ & hav]]
=| hav/mode:clay
|- ^+ hav
?~ sal ~
=. hav $(sal t.sal)
::
:: tyl: spur
::
=/ tyl i.sal
|- ^+ hav
::
:: pax: full path at `tyl`
:: lon: directory at `tyl`
::
=/ pax (en-beam:format bec tyl)
=/ lon .^(arch %cy pax)
=? hav ?=(^ fil.lon)
?. ?=({$hoon *} tyl)
::
:: install only hoon files for now
::
hav
::
:: cot: file as plain-text octet-stream
::
=; cot [[(flop `path`tyl) `[/text/plain cot]] hav]
^- octs
?- tyl
{$hoon *}
=/ dat .^(@t %cx pax)
[(met 3 dat) dat]
==
=/ all ~(tap by dir.lon)
|- ^- mode:clay
?~ all hav
$(all t.all, hav ^$(tyl [p.i.all tyl]))
::
++ vent
|= {abr/term den/path}
=+ pax=(weld sys den)
=+ txt=.^(@ %cx (welp pax /hoon))
`ovum`[[%vane den] [%veer abr pax txt]]
--
::
:: main-events: full events with advancing times
::
=. now ~2017.3.1
=+ ^= main-events
|- ^- (list (pair @da ovum))
?~ main-moves ~
:- [now i.main-moves]
$(main-moves t.main-moves, now (add now (bex 48)))
::
~? try
~& %metal-testing
=+ ^= yop
^- @p
%- mug
.* :* boot-one
boot-two
compiler-formula
compiler-source
arvo-source
main-events
==
[2 [0 3] [0 2]]
[%metal-tested yop]
::
:* boot-one
boot-two
compiler-formula
compiler-source
arvo-source
main-events
==