Commits

Breadcrumbs

History for

onmain

User selector

All users

Datepicker

All time

Commit history

Commits on Aug 14, 2026

• fix(formal): restore the orphaned top-level soundness formalization to the build; revert unverified proof claims

  Show description for d0cd746
  dporkka

  committed
  d0cd746View commit details

  Copy full SHA for d0cd746

  View code at this pointBrowse repository at this point

• proof(semantics): complete the type-soundness chain — zero sorries in types.lean

  Show description for dd3aafa
  dporkka

  committed
  dd3aafaView commit details

  Copy full SHA for dd3aafa

  View code at this pointBrowse repository at this point

• proof(semantics): prove weakening (corrected), progress, closed-type theorems

  Show description for fe610d8
  dporkka

  committed
  fe610d8View commit details

  Copy full SHA for fe610d8

  View code at this pointBrowse repository at this point

Commits on Aug 10, 2026

• fix(formal): complete de Bruijn proofs with non-nested Expr

  Show description for eb7c381
  dporkka

  committed
  eb7c381View commit details

  Copy full SHA for eb7c381

  View code at this pointBrowse repository at this point

• feat(formal): context_exchange_at — 7/10 cases proved

  Show description for d75e5d2
  dporkka

  committed
  d75e5d2View commit details

  Copy full SHA for d75e5d2

  View code at this pointBrowse repository at this point

• feat(formal): generalized context exchange at arbitrary depth

  Show description for 3962da8
  dporkka

  committed
  3962da8View commit details

  Copy full SHA for 3962da8

  View code at this pointBrowse repository at this point

• feat(formal): context exchange var case proved

  Show description for 36a7e40
  dporkka

  committed
  36a7e40View commit details

  Copy full SHA for 36a7e40

  View code at this pointBrowse repository at this point

• feat(formal): context exchange lemma (var + binder cases WIP)

  dporkka

  committed
  6bc10acView commit details

  Copy full SHA for 6bc10ac

  View code at this pointBrowse repository at this point

• feat(formal): weakening proof with de Bruijn indices (12/14 cases)

  Show description for f63f9e0
  dporkka

  committed
  f63f9e0View commit details

  Copy full SHA for f63f9e0

  View code at this pointBrowse repository at this point

• feat(formal): de Bruijn syntax with complete shift_compose lemma (13/13 proved)

  Show description for 2af780d
  dporkka

  committed
  2af780dView commit details

  Copy full SHA for 2af780d

  View code at this pointBrowse repository at this point

Commits on Aug 9, 2026

• feat(jit): SIMD tier-2 compilation for loop regions

  Show description for 079a733
  dporkka

  committed
  079a733View commit details

  Copy full SHA for 079a733

  View code at this pointBrowse repository at this point

• Update formal spec docs and add AOT debug test

  dporkka

  committed
  89bd0d6View commit details

  Copy full SHA for 89bd0d6

  View code at this pointBrowse repository at this point

Commits on Aug 2, 2026

• feat(effects): enforce LinearIso/Linear exactly-once for let-bindings

  Show description for 4f1b511
  dporkka

  committed
  4f1b511View commit details

  Copy full SHA for 4f1b511

  View code at this pointBrowse repository at this point

• docs(formal): correct false '0 sorries' claim, add CI sorry ratchet

  Show description for 2368853
  dporkka

  committed
  2368853View commit details

  Copy full SHA for 2368853

  View code at this pointBrowse repository at this point

Commits on Aug 1, 2026

• feat(lsp): replace regex-based inlay hints with typechecker-backed inference

  Show description for 7934c75
  dporkka

  committed
  7934c75View commit details

  Copy full SHA for 7934c75

  View code at this pointBrowse repository at this point

Commits on Jul 26, 2026

• fix(formal): Lean 4.16.0 compatibility, restore theorem stmts

  Show description for ac9ef5d
  dporkka

  committed
  ac9ef5dView commit details

  Copy full SHA for ac9ef5d

  View code at this pointBrowse repository at this point

Commits on Jul 25, 2026

• style: apply rustfmt to entire codebase

  Show description for c4a3fd5
  dporkka

  committed
  c4a3fd5View commit details

  Copy full SHA for c4a3fd5

  View code at this pointBrowse repository at this point

• chore: gitignore Lean build artifacts, remove accidental commits

  dporkka

  committed
  8e0a3b2View commit details

  Copy full SHA for 8e0a3b2

  View code at this pointBrowse repository at this point

• fix: lexer block comment panic, LSP diagnostic range, arity errors

  Show description for 94ccf3a
  dporkka

  committed
  94ccf3aView commit details

  Copy full SHA for 94ccf3a

  View code at this pointBrowse repository at this point

• docs: narrow formal spec scope, add Lean CI, document divergences

  Show description for e4d6bab
  dporkka

  committed
  e4d6babView commit details

  Copy full SHA for e4d6bab

  View code at this pointBrowse repository at this point

• feat(types.lean): add HasType.rec_on_ctx, fix tStrConcat/tUnit, update induction

  Show description for 2740cfc
  dporkka

  committed
  2740cfcView commit details

  Copy full SHA for 2740cfc

  View code at this pointBrowse repository at this point

• feat(types.lean): eliminate 3 sorries, add h_fv/h_closed to lemmas

  Show description for 829e57e
  dporkka

  committed
  829e57eView commit details

  Copy full SHA for 829e57e

  View code at this pointBrowse repository at this point

Commits on Jul 24, 2026

• feat: formal HM soundness proofs, break-with-value, ArrLen VM fix

  Show description for c44642a
  dporkka

  committed
  c44642aView commit details

  Copy full SHA for c44642a

  View code at this pointBrowse repository at this point

• feat(formal): add combined.lean — unified HM+cap+effect typing judgment

  Show description for 29f03a3
  dporkka

  committed
  29f03a3View commit details

  Copy full SHA for 29f03a3

  View code at this pointBrowse repository at this point

• feat: add CryptoProvider/ForeignInterop traits, extend formal semantics

  Show description for 1cbe06c
  dporkka

  committed
  1cbe06cView commit details

  Copy full SHA for 1cbe06c

  View code at this pointBrowse repository at this point

Commits on Jul 23, 2026

• chore: fix compiler warnings and extend formal semantics

  Show description for 14b5a74
  dporkka

  committed
  14b5a74View commit details

  Copy full SHA for 14b5a74

  View code at this pointBrowse repository at this point

Commits on Jul 19, 2026

• feat: formal semantics scaffold + bootstrap compiler skeleton

  Show description for e1f358b
  dporkka

  committed
  e1f358bView commit details

  Copy full SHA for e1f358b

  View code at this pointBrowse repository at this point

• feat: 200-year longevity roadmap — format versioning, governance, .nbc, Provider effect, backend traits, content-addressed modules, grammar

  Show description for be0ef48
  dporkka

  committed
  be0ef48View commit details

  Copy full SHA for be0ef48

  View code at this pointBrowse repository at this point

Loading