-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathnitpick.toml
More file actions
217 lines (197 loc) · 9.22 KB
/
Copy pathnitpick.toml
File metadata and controls
217 lines (197 loc) · 9.22 KB
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
[project]
name = "npkc"
version = "0.0.0"
description = "The Nitpick compiler — self-hosted, zero-dependency, formally verifiable"
authors = ["Randy"]
target = "executable"
[build]
entry = "src/main.npk"
output = "build/npkc"
# 0 during the bootstrap: `opt` is not invoked at all (BUILD_REFERENCE §4), which
# keeps the pipeline short and the output easy to read while the backend is being
# built. Raised once there is something worth optimising.
opt-level = 0
# THE TOOLCHAIN IS A BUILD INPUT (D-204), so it is pinned here as DATA rather
# than described in prose somewhere. "The same inputs produce a byte-identical
# output" is only a claim you can check if the tools count as inputs.
#
# EXACT PATCH RELEASE, not a minor version. The R-4 reproducibility research is
# blunt about it: pinning to a minor version is insufficient for strict
# byte-identity, because a patch release may change instruction selection or
# section ordering. Any update — patch included — is a breaking change that
# regenerates every expected hash, and the harness refuses a mismatch loudly
# rather than producing output nobody can reproduce.
#
# THE FLAGS ARE PINNED TOO, AND THE HARNESS READS THEM FROM HERE. A table
# stating flags that nothing checks is the next stale document; these are the
# lists every `llc`/`opt`/`ld.lld` invocation is actually built from, so the
# manifest and the pipeline cannot drift. `llc-opt-flags` is the 1.3.8
# instrument's leg (every program re-run through `opt -O2` + `llc -O2`), kept
# separate because it is a CHECK, not the build.
#
# NOT PINNED, deliberately:
# -mcpu — the emitted .ll carries `target triple` and we pass no `-mcpu`, so
# llc uses the triple's generic CPU. R-4 recommends an explicit `-mcpu`
# when build hosts vary; pinning a specific microarchitecture would change
# today's byte-identical output, so it is a recorded question rather than a
# change. If cross-machine divergence is ever observed, `-mcpu=x86-64` (the
# generic tune) is the fix, applied everywhere at once with hashes
# regenerated.
# --build-id — we pass none. The `uuid` form injects entropy by design and is
# the one spelling never to use here.
[toolchain]
llvm = "20.1.2"
llc-flags = ["-O0", "-filetype=obj", "-relocation-model=static"]
llc-opt-flags = ["-O2", "-filetype=obj", "-relocation-model=static"]
opt-flags = ["-O2", "-S"]
lld-flags = ["-static"]
# Empty, and empty for a long while. The compiler depends on nothing until
# `nlibc` exists in cycle 0.8. Anything added here is a zero-dependency decision
# and needs to be argued as one.
[dependencies]
# TEST TARGETS (BUILD_REFERENCE §7.1; D-238). EVERY suite `npkg test` and the
# harness run is declared here, in run order, and both runners read this one
# table -- a manifest that declared four of fourteen suites was a document a
# reader could not trust to say what ran, the stale-document shape the
# [toolchain] block refused for flags. Both runners refuse an entry they
# cannot honour BY NAME before anything runs: a stage they do not know, a
# `kind` on a stage that has none, no paths. Keys:
#
# name the suite's label, in every verdict line and stage line
# stage the tool that judges the suite and what it must say:
# compile the compiler under test, held to `kind`:
# positive compiles, links, runs, exits with the expected code
# negative FAILS to compile, emitting exactly the expected diagnostics
# diagnostic compiles, emitting exactly the expected warnings
# parse tools/parse_check: accepted with no diagnostic (D-085's sweep)
# resolve tools/resolve_check: refused with exactly the expected codes (the LOADER)
# check tools/check: refused with exactly the expected codes (the frontend)
# accept tools/check: accepted in silence
# fixture built like a program and never run; its uppercased stem is an `// argv:` token
# program emitted, scanned, assembled, linked, run at -O0 and again through opt -O2
# runtime a hand-written .ll assembled, linked against the floor, run
# (`compile` is the default; it is the only stage with a `kind`)
# paths the directories swept, an array; `path` is its one-element shorthand
# recursive sweep subdirectories too (default false)
#
# Membership stays with the stage: a `resolve`/`check` file with no
# `expect-error` is a fixture another file imports and is skipped; a
# `compile`/`program` file some other file in its suite imports is skipped.
# Expectations live in the test file itself, next to the code, so a test and
# its expectation cannot drift apart -- and they assert on stable CODES and
# spans, never on message text (§7.1 has the marker grammar).
[[test]]
name = "conformance"
stage = "compile"
kind = "positive"
path = "tests/conformance"
[[test]]
name = "frontend"
stage = "compile"
kind = "positive"
path = "tests/frontend"
[[test]]
name = "rejection"
stage = "compile"
kind = "negative"
path = "tests/rejection"
# The BACKEND's own unit tests (cycle 0.7). Positive, like `frontend`: they link the
# emitter, run it, and assert on what it produced. A backend test cannot be a
# rejection case -- the thing it is checking is the IR, and IR that is wrong in a way
# that still assembles produces no diagnostic at all.
[[test]]
name = "backend"
stage = "compile"
kind = "positive"
path = "tests/backend"
# The REAL parser over every source in the tree, each file once. A rejection
# test the real parser cannot read is testing the wrong stage (D-085);
# tests/grammar/ is parse-only by design and exists to be swept here; the
# prelude is real source; and the compiler's own tree is the file set that
# matters most -- stage 1 must parse it to build stage 2, so a source the real
# parser cannot read is a source that never self-hosts. `npkg/` is built by
# the compiler under test, so it is here for the same reason.
[[test]]
name = "grammar"
stage = "parse"
recursive = true
paths = ["tests", "src", "tools", "lib", "npkg"]
# FIVE REJECTION SUITES, ONE PER STAGE THAT REFUSES, and the split is the
# point: a file that stops earlier would satisfy a test written about a later
# stage. `modules` is refused by the LOADER and never reaches a checker; the
# other four load and resolve and are refused by the type checker, a static
# analysis, macro expansion, or the `#[derive]` reader (whose codes carry
# their own prefix because a reader filtering for one is asking a different
# question). A file here with no `expect-error:` is a fixture another one
# imports, not a test. (The BACKEND's rejections -- correct programs at a rung
# that cannot lower them yet -- are the `rejection` compile target above.)
[[test]]
name = "modules"
stage = "resolve"
recursive = true
path = "tests/modules/rejection"
[[test]]
name = "types"
stage = "check"
recursive = true
path = "tests/types/rejection"
[[test]]
name = "analysis"
stage = "check"
recursive = true
path = "tests/analysis/rejection"
[[test]]
name = "expansion"
stage = "check"
recursive = true
path = "tests/expansion/rejection"
[[test]]
name = "derive"
stage = "check"
recursive = true
path = "tests/derive/rejection"
# Helper binaries a test spawns (1.1.13a): built by the real-backend pipeline
# and held to its checks, never run by the runner; a program names one in
# `// argv:` by its uppercased stem. A `.c` here is a reference DRIVER
# (1.1.13c) built with the system C compiler -- test tooling outside the
# TCB, never in the artifact (D-149). Declared BEFORE `programs`, which
# consumes the map this stage fills.
[[test]]
name = "fixtures"
stage = "fixture"
path = "tests/backend/fixtures"
# Whole programs COMPILED BY THE REAL BACKEND, linked against the runtime and
# RUN -- at -O0 and again through opt -O2 with the same exit required (1.3.8:
# the optimiser once removed a load-bearing guarantee, so it is tested, not
# trusted). The conformance suite is here too: subset 1 compiles and runs
# under THIS compiler, the self-hosting goal sentence made a test.
[[test]]
name = "programs"
stage = "program"
paths = ["tests/backend/programs", "tests/conformance"]
# The runtime floor's own tests (0.10.3): hand-written .ll for families with
# no surface syntax, assembled, linked against npkrt.o, run, exit asserted.
[[test]]
name = "runtime"
stage = "runtime"
path = "runtime/tests"
# Whole programs the frontend must ACCEPT in full silence -- the counterweight
# to the rejection suites, since a checker that refused every program would
# pass every one of them. One suite, not one per stage: silence has no stage.
[[test]]
name = "accept"
stage = "accept"
recursive = true
path = "tests/accept"
# Verification configuration belongs to the project, not to whoever typed the
# command (D-077). These are the settings this project must be verified under.
#
# ⚠️ The tooling that honours them arrives in cycle 1.5 (verification); `npkg`
# itself landed at 1.4.8 and refuses `npkg verify` BY NAME until then. They
# are written now, switched on, so that enabling verification is never a step
# someone has to remember — a safety property must not depend on a flag being
# flipped later (D-068).
[verify]
z3 = true
[verify.nikos]
domain = "interval"