You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
* feat(types): add Echo types (structured loss) across the pipeline
Introduce `Echo<A, B>` — the fibre of a function A → B (a retained
witness `x : A` with `f x ≡ y : B`) — and its residue `EchoR<A, B>`,
porting the echo-types (Agda) / EchoTypes.jl lineage into Error-Lang as
a runnable, stability-aware model of non-total erasure.
Pipeline:
- Types/Lexer: `Echo`/`EchoR` keywords; `TyEcho`/`TyEchoResidue`
typeExpr with sugar (`Echo<A,B>`, `Echo<A>`, bare `Echo`).
- Parser: real `parseTypeExpr` (primitives, `Array<T>`, Echo/EchoR,
nested `>>` splitting) wired into let annotations, struct fields and
function params/return — annotations were previously dropped.
- TypeChecker: internal `TyEcho`/`TyEchoR` with conversion, display and
unification. Echo and EchoR unify only with their own kind and never
with each other, so erasure is irreversible at the type level.
Builtins mirror EchoTypes.jl: echo, echo_to_residue,
residue_strictly_loses, echo_input (illegal on a residue), echo_output.
- Runtime (Bytecode/VM/Codegen): `VEcho{input,output}` single-witness
value and `VResidue{output}`; dedicated opcodes. Erasing an Echo to its
residue debits stability (a Landauer-style cost; cf. fiber_erasure_bound).
- Pretty/LayerNavigator: render the new type forms.
- spec/type-system.md: new §7 (Echo Types) plus the [Stab-Erase] rule.
- Tests: type-checker, parser and lexer coverage for Echo/EchoR.
The core conversion/display/unification logic was compile-verified and
behaviourally checked in isolation (the wider compiler/ tree does not
build against mainstream ReScript for reasons predating this change).
* ci: add timeout-minutes to standalone workflow jobs
Addresses the Hypatia workflow-audit `missing_timeout_minutes` findings on
the jobs that can carry a job-level timeout:
- casket-pages.yml: build (15m), deploy (10m)
- codeql.yml: analyze (30m)
- hypatia-scan.yml: scan (20m)
The reusable-workflow callers (governance.yml, mirror.yml, scorecard.yml)
are intentionally left untouched: GitHub does not permit `timeout-minutes`
on a job that uses `uses:`. governance.yml's `@main` reference is also left
as-is — mirror/scorecard are SHA-pinned but governance is deliberately kept
on main by the maintainer.
---------
Co-authored-by: Claude <noreply@anthropic.com>
# The submission script's location in gitbot-fleet has drifted
262
+
# before (it was absent from the default branch, which exit-127'd
263
+
# every consuming repo's scan). Probe known locations rather than
264
+
# hard-coding one path, and skip gracefully if none is present.
265
+
SUBMIT_SCRIPT=""
266
+
for cand in \
267
+
"$FLEET_DIR/scripts/submit-finding.sh" \
268
+
"$FLEET_DIR/scripts/submit_finding.sh" \
269
+
"$FLEET_DIR/bin/submit-finding.sh" \
270
+
"$FLEET_DIR/submit-finding.sh"; do
271
+
if [ -f "$cand" ]; then
272
+
SUBMIT_SCRIPT="$cand"
273
+
break
274
+
fi
275
+
done
276
+
277
+
if [ -z "$SUBMIT_SCRIPT" ]; then
278
+
echo "::warning::gitbot-fleet submit-finding script not found at any known path — skipping Phase 2 learning submission (non-fatal). Findings are still uploaded as an artifact and gated below."
279
+
rm -rf "$FLEET_DIR"
280
+
exit 0
281
+
fi
282
+
283
+
# Run submission script. Pass the findings path as ABSOLUTE —
284
+
# the script cd's into its own working dir before reading the
285
+
# file, so a relative path would resolve to the wrong place.
286
+
# A submission-script failure is logged but non-fatal.
287
+
if bash "$SUBMIT_SCRIPT" "$GITHUB_WORKSPACE/hypatia-findings.json"; then
0 commit comments