Compiler fixes for auxiliary constant generation#473

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
johnchandlerburnham merged 5 commits into from
Jul 7, 2026
Merged

Compiler fixes for auxiliary constant generation #473

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
62eb9c6
Ixon: drop recr/refl/nested flags from Inductive
johnchandlerburnham Jul 4, 2026
2fc6dda
Compile: evaporated-aux canonicalization and byte-exact aux roundtrip
johnchandlerburnham Jul 4, 2026
fb00cf5
chore: fix clippy warnings and fmt drift
johnchandlerburnham Jul 4, 2026
d8b11c0
IxVM Aiur kernel: fix Lean.Syntax.rec (shard 53) aux-recursor gen
arthurpaulino Jul 1, 2026
2f2a86f
IxVM: port Inductive flag-drop + evaporated-aux aliasing to Aiur kernel
arthurpaulino Jul 4, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -7,3 +7,7 @@
# Nix
result*
.direnv/

#Ix
*.ixe
plans
1 change: 1 addition & 0 deletions Benchmarks/Compile/CompileMutualFixtures.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
import Tests.Ix.Compile.Mutual
29 changes: 28 additions & 1 deletion Benchmarks/Compile/lake-manifest.json
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -21,6 +21,13 @@
"inputRev": "v4.29.0",
"inherited": false,
"configFile": "lakefile.toml"},
{"type": "path",
"scope": "",
"name": "ix",
"manifestFile": "lake-manifest.json",
"inherited": false,
"dir": "../..",
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/plausible",
"type": "git",
"subDir": null,
Expand DownExpand Up@@ -110,6 +117,26 @@
"manifestFile": "lake-manifest.json",
"inputRev": null,
"inherited": true,
"configFile": "lakefile.lean"}],
"configFile": "lakefile.lean"},
{"url": "https://github.com/argumentcomputer/Blake3.lean",
"type": "git",
"subDir": null,
"scope": "",
"rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
"name": "Blake3",
"manifestFile": "lake-manifest.json",
"inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/argumentcomputer/LSpec",
"type": "git",
"subDir": null,
"scope": "",
"rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
"name": "LSpec",
"manifestFile": "lake-manifest.json",
"inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
"inherited": true,
"configFile": "lakefile.toml"}],
"name": "Compile",
"lakeDir": ".lake"}
7 changes: 7 additions & 0 deletions Benchmarks/Compile/lakefile.toml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -17,6 +17,13 @@ name = "CompileMathlib"
[[lean_lib]]
name = "CompileFLT"

[[lean_lib]]
name = "CompileMutualFixtures"

[[require]]
name = "ix"
path = "../.."

[[require]]
name = "flt"
git = "https://github.com/ImperialCollegeLondon/FLT"
Expand Down
34 changes: 13 additions & 21 deletions Ix/Claim.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -94,10 +94,9 @@ structure RevealRecursorRule where
inductive RevealMutConstInfo where
| defn (kind : Option DefKind) (safety : Option DefinitionSafety)
(lvls : Option UInt64) (typ : Option Address) (value : Option Address)
| indc (isRecr : Option Bool) (refl : Option Bool) (isUnsafe : Option Bool)
(lvls : Option UInt64) (params : Option UInt64)
(indices : Option UInt64) (nested : Option UInt64)
(typ : Option Address) (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
| indc (isUnsafe : Option Bool) (lvls : Option UInt64) (params : Option UInt64)
(indices : Option UInt64) (typ : Option Address)
(ctors : Option (Array (UInt64 × RevealConstructorInfo)))
| recr (k : Option Bool) (isUnsafe : Option Bool) (lvls : Option UInt64)
(params : Option UInt64) (indices : Option UInt64)
(motives : Option UInt64) (minors : Option UInt64)
Expand DownExpand Up@@ -240,19 +239,15 @@ def put : RevealMutConstInfo → PutM Unit
match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
match typ with | some a => Serialize.put a | none => pure ()
match value with | some a => Serialize.put a | none => pure ()
| .indc isRecr refl isUnsafe lvls params indices nested typ ctors => do
| .indc isUnsafe lvls params indices typ ctors => do
putU8 1
let mask := computeMask [isRecr.isSome, refl.isSome, isUnsafe.isSome,
lvls.isSome, params.isSome, indices.isSome,
nested.isSome, typ.isSome, ctors.isSome]
let mask := computeMask [isUnsafe.isSome, lvls.isSome, params.isSome,
indices.isSome, typ.isSome, ctors.isSome]
putTag0 ⟨mask⟩
match isRecr with | some b => putBoolField b | none => pure ()
match refl with | some b => putBoolField b | none => pure ()
match isUnsafe with | some b => putBoolField b | none => pure ()
match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
match params with | some n => putTag0 ⟨n⟩ | none => pure ()
match indices with | some n => putTag0 ⟨n⟩ | none => pure ()
match nested with | some n => putTag0 ⟨n⟩ | none => pure ()
match typ with | some a => Serialize.put a | none => pure ()
match ctors with | some c => putCtors c | none => pure ()
| .recr k isUnsafe lvls params indices motives minors typ rules => do
Expand DownExpand Up@@ -283,16 +278,13 @@ def get : GetM RevealMutConstInfo := do
let value ← getOpt mask 16 Serialize.get
return .defn kind safety lvls typ value
| 1 => do -- Indc
let isRecr ← getOpt mask 1 getBoolField
let refl ← getOpt mask 2 getBoolField
let isUnsafe ← getOpt mask 4 getBoolField
let lvls ← getOpt mask 8 getTag0Size
let params ← getOpt mask 16 getTag0Size
let indices ← getOpt mask 32 getTag0Size
let nested ← getOpt mask 64 getTag0Size
let typ ← getOpt mask 128 Serialize.get
let ctors ← getOpt mask 256 getCtors
return .indc isRecr refl isUnsafe lvls params indices nested typ ctors
let isUnsafe ← getOpt mask 1 getBoolField
let lvls ← getOpt mask 2 getTag0Size
let params ← getOpt mask 4 getTag0Size
let indices ← getOpt mask 8 getTag0Size
let typ ← getOpt mask 16 Serialize.get
let ctors ← getOpt mask 32 getCtors
return .indc isUnsafe lvls params indices typ ctors
| 2 => do -- Recr
let k ← getOpt mask 1 getBoolField
let isUnsafe ← getOpt mask 2 getBoolField
Expand Down
3 changes: 1 addition & 2 deletions Ix/Commit.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -208,8 +208,7 @@ def openMutConst (mc : Ixon.MutConst) : RevealMutConstInfo :=
for j in [:i.ctors.size] do
arr := arr.push (j.toUInt64, openConstructor i.ctors[j]!)
return arr
.indc (some i.recr) (some i.refl) (some i.isUnsafe)
(some i.lvls) (some i.params) (some i.indices) (some i.nested)
.indc (some i.isUnsafe) (some i.lvls) (some i.params) (some i.indices)
(some (exprAddr i.typ)) (some ctors)
| .recr r =>
let rules := Id.run do
Expand Down
34 changes: 34 additions & 0 deletions Ix/Common.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -328,6 +328,40 @@ private partial def collectDependenciesAux (const : Lean.ConstantInfo)
goExpr consts acc val.value
| .recInfo val =>
let acc ← collectNames val.all acc
-- The compiler processes a declaration's recursors as one block, and
-- they cross-reference in rule RHSs (`A.rec`'s rule calls `A.rec_1`,
-- `A.rec_2`'s calls `C.rec`), so the closure needs every sibling:
-- `<ind>.rec` per block inductive plus the nested-aux `<all0>.rec_N`.
let siblings := val.all.filterMap fun ind =>
let n := Lean.mkRecName ind
if consts.contains n then some n else none
let auxSiblings : List Lean.Name := Id.run do
let mut out := []
let mut i := 1
repeat
match val.all.head? with
| none => break
| some base =>
let n := Lean.Name.mkStr base s!"rec_{i}"
if consts.contains n then
out := n :: out
i := i + 1
else break
return out
let acc ← collectNames (siblings ++ auxSiblings) acc
-- A nested-aux recursor's rules recurse via the external container's
-- ctors; its evaporated form aliases that container's recursor
-- (`List.rec`), which no collected expr mentions — pull it via each
-- rule ctor's owning inductive.
let extRecs := val.rules.filterMap fun rule =>
match consts.find? rule.ctor with
| some (.ctorInfo cv) =>
if val.all.contains cv.induct then none
else
let n := Lean.mkRecName cv.induct
if consts.contains n then some n else none
| _ => none
let acc ← collectNames extRecs acc
let acc ← goExpr consts acc val.type
val.rules.foldlM (init := acc) fun acc rule => goExpr consts acc rule.rhs
where
Expand Down
6 changes: 0 additions & 6 deletions Ix/CompileM.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -1112,13 +1112,10 @@ def compileInductive (i : InductiveVal) (ctorVals : Array ConstructorVal)
let ctxAddrs ← getMutCtxAddrs

let ind : Ixon.Inductive := {
recr := i.isRec
refl := i.isReflexive
isUnsafe := i.isUnsafe
lvls := i.cnst.levelParams.size.toUInt64
params := i.numParams.toUInt64
indices := i.numIndices.toUInt64
nested := i.numNested.toUInt64
typ := typeExpr
ctors := ctors
}
Expand DownExpand Up@@ -1194,13 +1191,10 @@ def compileInductiveData (i : Ind)
let ctxAddrs ← getMutCtxAddrs

let ind : Ixon.Inductive := {
recr := i.isRec
refl := i.isReflexive
isUnsafe := i.isUnsafe
lvls := i.levelParams.size.toUInt64
params := i.numParams.toUInt64
indices := i.numIndices.toUInt64
nested := i.numNested.toUInt64
typ := typeExpr
ctors := ctors
}
Expand Down
5 changes: 3 additions & 2 deletions Ix/DecompileM.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -670,8 +670,9 @@ def decompileInductive (ind : Ixon.Inductive) (cnst : Constant) (cMeta : Constan
cnst := { name, levelParams := univParams, type := typeExpr },
numParams := ind.params.toNat, numIndices := ind.indices.toNat,
all := allNames, ctors := ctorNames,
numNested := ind.nested.toNat, isRec := ind.recr,
isUnsafe := ind.isUnsafe, isReflexive := ind.refl }
-- temporary stub until we update the Lean compiler and decompiler semantics
numNested := 0, isRec := false
isUnsafe := ind.isUnsafe, isReflexive := false }
pure (indVal, ctors)

/-! ## Projection Handling -/
Expand Down
4 changes: 2 additions & 2 deletions Ix/IxVM/Convert.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -314,11 +314,11 @@ def convert := ⟦
match ctx {
ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
match ind {
Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, typ, _) =>
Inductive.Mk(is_unsafe, lvls, params, indices, typ, _) =>
let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
KConstantInfo.Induct(
flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
ctor_idxs, is_rec, is_refl, is_unsafe, flatten_u64(nested), block_addr),
ctor_idxs, is_unsafe, block_addr),
},
}
}
Expand Down
10 changes: 5 additions & 5 deletions Ix/IxVM/Ingress.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -175,7 +175,7 @@ def ingress := ⟦
match mc {
MutConst.Indc(ind) =>
match ind {
Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
Inductive.Mk(_, _, _, _, _, ctors) =>
list_length(ctors) + 1,
},
MutConst.Recr(_) => 1,
Expand DownExpand Up@@ -850,7 +850,7 @@ def ingress := ⟦
match mc {
MutConst.Indc(ind) =>
match ind {
Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
Inductive.Mk(_, _, _, _, _, ctors) =>
let num_ctors = list_length(ctors);
let this_ctors = build_ctor_idxs(num_ctors, cur_pos, 0);
let rest_ctors = build_rule_ctor_idxs_walk(rest,
Expand DownExpand Up@@ -998,7 +998,7 @@ def ingress := ⟦
match mc {
MutConst.Indc(ind) =>
match ind {
Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
Inductive.Mk(_, _, _, _, _, ctors) =>
build_ctor_idxs(list_length(ctors), cur_pos, 0),
},
_ => store(ListNode.Nil),
Expand DownExpand Up@@ -1027,7 +1027,7 @@ def ingress := ⟦
match mc {
MutConst.Indc(ind) =>
match ind {
Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
Inductive.Mk(_, _, _, _, _, ctors) =>
let num_ctors = list_length(ctors);
let induct_pos = block_start + member_offset(members, member_idx);
let ctor_idxs = build_ctor_idxs(num_ctors, induct_pos, 0);
Expand DownExpand Up@@ -1546,7 +1546,7 @@ def ingress := ⟦
match mc {
MutConst.Indc(ind) =>
match ind {
Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
Inductive.Mk(_, _, _, _, _, ctors) =>
list_length(ctors),
},
_ => 0,
Expand Down
4 changes: 2 additions & 2 deletions Ix/IxVM/Ixon.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -83,9 +83,9 @@ def ixon := ⟦
Mk(G, U64, U64, U64, U64, &Expr)
}

-- Inductive: (recr, refl, is_unsafe, lvls, params, indices, nested, typ, ctors)
-- Inductive: (is_unsafe, lvls, params, indices, typ, ctors)
enum Inductive {
Mk(G, G, G, U64, U64, U64, U64, &Expr, List‹Constructor›)
Mk(G, U64, U64, U64, &Expr, List‹Constructor›)
}

-- InductiveProj: (idx, block_address)
Expand Down
15 changes: 6 additions & 9 deletions Ix/IxVM/IxonDeserialize.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -479,21 +479,18 @@ def ixonDeserialize := ⟦
}

-- Inductive: byte(bools) + Tag0(lvls) + Tag0(params) + Tag0(indices) +
-- Tag0(nested) + expr(typ) + Tag0(ctors_len) + ctors...
-- expr(typ) + Tag0(ctors_len) + ctors...
fn get_inductive(stream: ByteStream) -> (Inductive, ByteStream) {
let (bools_byte, s) = read_byte(stream);
let bits = u8_bit_decomposition(bools_byte);
let recr = bits[0];
let refl = bits[1];
let is_unsafe = bits[2];
let is_unsafe = bits[0];
let (lvls, s2) = get_tag0(s);
let (params, s3) = get_tag0(s2);
let (indices, s4) = get_tag0(s3);
let (nested, s5) = get_tag0(s4);
let (typ, s6) = get_expr(s5);
let (ctors_len, s7) = get_tag0(s6);
let (ctors, s8) = get_constructor_list(s7, ctors_len);
(Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, store(typ), ctors), s8)
let (typ, s5) = get_expr(s4);
let (ctors_len, s6) = get_tag0(s5);
let (ctors, s7) = get_constructor_list(s6, ctors_len);
(Inductive.Mk(is_unsafe, lvls, params, indices, store(typ), ctors), s7)
}

-- ============================================================================
Expand Down
12 changes: 5 additions & 7 deletions Ix/IxVM/IxonSerialize.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -387,17 +387,15 @@ def ixonSerialize := ⟦

fn put_inductive(indc: Inductive, rest: ByteStream) -> ByteStream {
match indc {
Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, &typ, ctors) =>
let bools = recr + 2 * refl + 4 * is_unsafe;
Inductive.Mk(is_unsafe, lvls, params, indices, &typ, ctors) =>
let ctors_len = list_length_u64(ctors);
store(ListNode.Cons(u8_from_field_unsafe(bools),
store(ListNode.Cons(u8_from_field_unsafe(is_unsafe),
put_tag0(lvls,
put_tag0(params,
put_tag0(indices,
put_tag0(nested,
put_expr(typ,
put_tag0(ctors_len,
put_constructor_list(ctors, rest))))))))),
put_expr(typ,
put_tag0(ctors_len,
put_constructor_list(ctors, rest)))))))),
}
}

Expand Down
Loading
, 'i'); if (__m === '*' || __re.test(location.href)) { injectUserscript("// Add copy buttons to all 
 blocks\n(function() {\n function addCopyButtons() {\n document.querySelectorAll('pre code').forEach(function(codeBlock) {\n if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;\n codeBlock.parentElement.setAttribute('data-copy-added', 'true');\n \n var btn = document.createElement('button');\n btn.textContent = 'Copy';\n btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';\n btn.onmouseover = function() { this.style.opacity = '1'; };\n btn.onmouseout = function() { this.style.opacity = '0.7'; };\n btn.onclick = function() {\n navigator.clipboard.writeText(codeBlock.textContent).then(function() {\n btn.textContent = 'Copied!';\n setTimeout(function() { btn.textContent = 'Copy'; }, 1500);\n });\n };\n codeBlock.parentElement.style.position = 'relative';\n codeBlock.parentElement.appendChild(btn);\n });\n }\n \n addCopyButtons();\n \n // Re-run on dynamic content\n var observer = new MutationObserver(addCopyButtons);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Add Copy Buttons to Code Blocks");
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '

Skip to content
Compiler fixes for auxiliary constant generation#473

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

johnchandlerburnham
merged 5 commits into

from

Jul 7, 2026
 Merged


Compiler fixes for auxiliary constant generation
#473
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


5 commits


Select commit
Hold shift + click to select a range
62eb9c6

Ixon: drop recr/refl/nested flags from Inductive


johnchandlerburnham Jul 4, 2026
2fc6dda

Compile: evaporated-aux canonicalization and byte-exact aux roundtrip


johnchandlerburnham Jul 4, 2026
fb00cf5

chore: fix clippy warnings and fmt drift


johnchandlerburnham Jul 4, 2026
d8b11c0

IxVM Aiur kernel: fix Lean.Syntax.rec (shard 53) aux-recursor gen


arthurpaulino Jul 1, 2026
2f2a86f

IxVM: port Inductive flag-drop + evaporated-aux aliasing to Aiur kernel


arthurpaulino Jul 4, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


4 changes: 4 additions & 0 deletions
.gitignore

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -7,3 +7,7 @@
# Nix
result*
.direnv/

#Ix
*.ixe
plans

1 change: 1 addition & 0 deletions
Benchmarks/Compile/CompileMutualFixtures.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
import Tests.Ix.Compile.Mutual

29 changes: 28 additions & 1 deletion
Benchmarks/Compile/lake-manifest.json

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -21,6 +21,13 @@
 "inputRev": "v4.29.0",
 "inherited": false,
 "configFile": "lakefile.toml"},
 {"type": "path",
 "scope": "",
 "name": "ix",
 "manifestFile": "lake-manifest.json",
 "inherited": false,
 "dir": "../..",
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/leanprover-community/plausible",
 "type": "git",
 "subDir": null,
Expand DownExpand Up@@ -110,6 +117,26 @@
 "manifestFile": "lake-manifest.json",
 "inputRev": null,
 "inherited": true,
 "configFile": "lakefile.lean"}],
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/argumentcomputer/Blake3.lean",
 "type": "git",
 "subDir": null,
 "scope": "",
 "rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
 "name": "Blake3",
 "manifestFile": "lake-manifest.json",
 "inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
 "inherited": true,
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/argumentcomputer/LSpec",
 "type": "git",
 "subDir": null,
 "scope": "",
 "rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
 "name": "LSpec",
 "manifestFile": "lake-manifest.json",
 "inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
 "inherited": true,
 "configFile": "lakefile.toml"}],
 "name": "Compile",
 "lakeDir": ".lake"}

7 changes: 7 additions & 0 deletions
Benchmarks/Compile/lakefile.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -17,6 +17,13 @@ name = "CompileMathlib"
[[lean_lib]]
name = "CompileFLT"

[[lean_lib]]
name = "CompileMutualFixtures"

[[require]]
name = "ix"
path = "../.."

[[require]]
name = "flt"
git = "https://github.com/ImperialCollegeLondon/FLT"
Expand Down

34 changes: 13 additions & 21 deletions
Ix/Claim.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -94,10 +94,9 @@ structure RevealRecursorRule where
inductive RevealMutConstInfo where
 | defn (kind : Option DefKind) (safety : Option DefinitionSafety)
 (lvls : Option UInt64) (typ : Option Address) (value : Option Address)
 | indc (isRecr : Option Bool) (refl : Option Bool) (isUnsafe : Option Bool)
 (lvls : Option UInt64) (params : Option UInt64)
 (indices : Option UInt64) (nested : Option UInt64)
 (typ : Option Address) (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
 | indc (isUnsafe : Option Bool) (lvls : Option UInt64) (params : Option UInt64)
 (indices : Option UInt64) (typ : Option Address)
 (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
 | recr (k : Option Bool) (isUnsafe : Option Bool) (lvls : Option UInt64)
 (params : Option UInt64) (indices : Option UInt64)
 (motives : Option UInt64) (minors : Option UInt64)
Expand DownExpand Up@@ -240,19 +239,15 @@ def put : RevealMutConstInfo → PutM Unit
 match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
 match typ with | some a => Serialize.put a | none => pure ()
 match value with | some a => Serialize.put a | none => pure ()
 | .indc isRecr refl isUnsafe lvls params indices nested typ ctors => do
 | .indc isUnsafe lvls params indices typ ctors => do
 putU8 1
 let mask := computeMask [isRecr.isSome, refl.isSome, isUnsafe.isSome,
 lvls.isSome, params.isSome, indices.isSome,
 nested.isSome, typ.isSome, ctors.isSome]
 let mask := computeMask [isUnsafe.isSome, lvls.isSome, params.isSome, 
 indices.isSome, typ.isSome, ctors.isSome]
 putTag0 ⟨mask⟩
 match isRecr with | some b => putBoolField b | none => pure ()
 match refl with | some b => putBoolField b | none => pure ()
 match isUnsafe with | some b => putBoolField b | none => pure ()
 match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
 match params with | some n => putTag0 ⟨n⟩ | none => pure ()
 match indices with | some n => putTag0 ⟨n⟩ | none => pure ()
 match nested with | some n => putTag0 ⟨n⟩ | none => pure ()
 match typ with | some a => Serialize.put a | none => pure ()
 match ctors with | some c => putCtors c | none => pure ()
 | .recr k isUnsafe lvls params indices motives minors typ rules => do
Expand DownExpand Up@@ -283,16 +278,13 @@ def get : GetM RevealMutConstInfo := do
 let value ← getOpt mask 16 Serialize.get
 return .defn kind safety lvls typ value
 | 1 => do -- Indc
 let isRecr ← getOpt mask 1 getBoolField
 let refl ← getOpt mask 2 getBoolField
 let isUnsafe ← getOpt mask 4 getBoolField
 let lvls ← getOpt mask 8 getTag0Size
 let params ← getOpt mask 16 getTag0Size
 let indices ← getOpt mask 32 getTag0Size
 let nested ← getOpt mask 64 getTag0Size
 let typ ← getOpt mask 128 Serialize.get
 let ctors ← getOpt mask 256 getCtors
 return .indc isRecr refl isUnsafe lvls params indices nested typ ctors
 let isUnsafe ← getOpt mask 1 getBoolField
 let lvls ← getOpt mask 2 getTag0Size
 let params ← getOpt mask 4 getTag0Size
 let indices ← getOpt mask 8 getTag0Size
 let typ ← getOpt mask 16 Serialize.get
 let ctors ← getOpt mask 32 getCtors
 return .indc isUnsafe lvls params indices typ ctors
 | 2 => do -- Recr
 let k ← getOpt mask 1 getBoolField
 let isUnsafe ← getOpt mask 2 getBoolField
Expand Down

3 changes: 1 addition & 2 deletions
Ix/Commit.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -208,8 +208,7 @@ def openMutConst (mc : Ixon.MutConst) : RevealMutConstInfo :=
 for j in [:i.ctors.size] do
 arr := arr.push (j.toUInt64, openConstructor i.ctors[j]!)
 return arr
 .indc (some i.recr) (some i.refl) (some i.isUnsafe)
 (some i.lvls) (some i.params) (some i.indices) (some i.nested)
 .indc (some i.isUnsafe) (some i.lvls) (some i.params) (some i.indices)
 (some (exprAddr i.typ)) (some ctors)
 | .recr r =>
 let rules := Id.run do
Expand Down

34 changes: 34 additions & 0 deletions
Ix/Common.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -328,6 +328,40 @@ private partial def collectDependenciesAux (const : Lean.ConstantInfo)
 goExpr consts acc val.value
 | .recInfo val =>
 let acc ← collectNames val.all acc
 -- The compiler processes a declaration's recursors as one block, and
 -- they cross-reference in rule RHSs (`A.rec`'s rule calls `A.rec_1`,
 -- `A.rec_2`'s calls `C.rec`), so the closure needs every sibling:
 -- `<ind>.rec` per block inductive plus the nested-aux `<all0>.rec_N`.
 let siblings := val.all.filterMap fun ind =>
 let n := Lean.mkRecName ind
 if consts.contains n then some n else none
 let auxSiblings : List Lean.Name := Id.run do
 let mut out := []
 let mut i := 1
 repeat
 match val.all.head? with
 | none => break
 | some base =>
 let n := Lean.Name.mkStr base s!"rec_{i}"
 if consts.contains n then
 out := n :: out
 i := i + 1
 else break
 return out
 let acc ← collectNames (siblings ++ auxSiblings) acc
 -- A nested-aux recursor's rules recurse via the external container's
 -- ctors; its evaporated form aliases that container's recursor
 -- (`List.rec`), which no collected expr mentions — pull it via each
 -- rule ctor's owning inductive.
 let extRecs := val.rules.filterMap fun rule =>
 match consts.find? rule.ctor with
 | some (.ctorInfo cv) =>
 if val.all.contains cv.induct then none
 else
 let n := Lean.mkRecName cv.induct
 if consts.contains n then some n else none
 | _ => none
 let acc ← collectNames extRecs acc
 let acc ← goExpr consts acc val.type
 val.rules.foldlM (init := acc) fun acc rule => goExpr consts acc rule.rhs
where
Expand Down

6 changes: 0 additions & 6 deletions
Ix/CompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -1112,13 +1112,10 @@ def compileInductive (i : InductiveVal) (ctorVals : Array ConstructorVal)
 let ctxAddrs ← getMutCtxAddrs

 let ind : Ixon.Inductive := {
 recr := i.isRec
 refl := i.isReflexive
 isUnsafe := i.isUnsafe
 lvls := i.cnst.levelParams.size.toUInt64
 params := i.numParams.toUInt64
 indices := i.numIndices.toUInt64
 nested := i.numNested.toUInt64
 typ := typeExpr
 ctors := ctors
 }
Expand DownExpand Up@@ -1194,13 +1191,10 @@ def compileInductiveData (i : Ind)
 let ctxAddrs ← getMutCtxAddrs

 let ind : Ixon.Inductive := {
 recr := i.isRec
 refl := i.isReflexive
 isUnsafe := i.isUnsafe
 lvls := i.levelParams.size.toUInt64
 params := i.numParams.toUInt64
 indices := i.numIndices.toUInt64
 nested := i.numNested.toUInt64
 typ := typeExpr
 ctors := ctors
 }
Expand Down

5 changes: 3 additions & 2 deletions
Ix/DecompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -670,8 +670,9 @@ def decompileInductive (ind : Ixon.Inductive) (cnst : Constant) (cMeta : Constan
 cnst := { name, levelParams := univParams, type := typeExpr },
 numParams := ind.params.toNat, numIndices := ind.indices.toNat,
 all := allNames, ctors := ctorNames,
 numNested := ind.nested.toNat, isRec := ind.recr,
 isUnsafe := ind.isUnsafe, isReflexive := ind.refl }
 -- temporary stub until we update the Lean compiler and decompiler semantics
 numNested := 0, isRec := false
 isUnsafe := ind.isUnsafe, isReflexive := false }
 pure (indVal, ctors)

/-! ## Projection Handling -/
Expand Down

4 changes: 2 additions & 2 deletions
Ix/IxVM/Convert.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -314,11 +314,11 @@ def convert := ⟦
 match ctx {
 ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
 match ind {
 Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, typ, _) =>
 Inductive.Mk(is_unsafe, lvls, params, indices, typ, _) =>
 let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
 KConstantInfo.Induct(
 flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
 ctor_idxs, is_rec, is_refl, is_unsafe, flatten_u64(nested), block_addr),
 ctor_idxs, is_unsafe, block_addr),
 },
 }
 }
Expand Down

10 changes: 5 additions & 5 deletions
Ix/IxVM/Ingress.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -175,7 +175,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 list_length(ctors) + 1,
 },
 MutConst.Recr(_) => 1,
Expand DownExpand Up@@ -850,7 +850,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 let num_ctors = list_length(ctors);
 let this_ctors = build_ctor_idxs(num_ctors, cur_pos, 0);
 let rest_ctors = build_rule_ctor_idxs_walk(rest,
Expand DownExpand Up@@ -998,7 +998,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 build_ctor_idxs(list_length(ctors), cur_pos, 0),
 },
 _ => store(ListNode.Nil),
Expand DownExpand Up@@ -1027,7 +1027,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 let num_ctors = list_length(ctors);
 let induct_pos = block_start + member_offset(members, member_idx);
 let ctor_idxs = build_ctor_idxs(num_ctors, induct_pos, 0);
Expand DownExpand Up@@ -1546,7 +1546,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 list_length(ctors),
 },
 _ => 0,
Expand Down

4 changes: 2 additions & 2 deletions
Ix/IxVM/Ixon.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -83,9 +83,9 @@ def ixon := ⟦
 Mk(G, U64, U64, U64, U64, &Expr)
 }

 -- Inductive: (recr, refl, is_unsafe, lvls, params, indices, nested, typ, ctors)
 -- Inductive: (is_unsafe, lvls, params, indices, typ, ctors)
 enum Inductive {
 Mk(G, G, G, U64, U64, U64, U64, &Expr, List‹Constructor›)
 Mk(G, U64, U64, U64, &Expr, List‹Constructor›)
 }

 -- InductiveProj: (idx, block_address)
Expand Down

15 changes: 6 additions & 9 deletions
Ix/IxVM/IxonDeserialize.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -479,21 +479,18 @@ def ixonDeserialize := ⟦
 }

 -- Inductive: byte(bools) + Tag0(lvls) + Tag0(params) + Tag0(indices) +
 -- Tag0(nested) + expr(typ) + Tag0(ctors_len) + ctors...
 -- expr(typ) + Tag0(ctors_len) + ctors...
 fn get_inductive(stream: ByteStream) -> (Inductive, ByteStream) {
 let (bools_byte, s) = read_byte(stream);
 let bits = u8_bit_decomposition(bools_byte);
 let recr = bits[0];
 let refl = bits[1];
 let is_unsafe = bits[2];
 let is_unsafe = bits[0];
 let (lvls, s2) = get_tag0(s);
 let (params, s3) = get_tag0(s2);
 let (indices, s4) = get_tag0(s3);
 let (nested, s5) = get_tag0(s4);
 let (typ, s6) = get_expr(s5);
 let (ctors_len, s7) = get_tag0(s6);
 let (ctors, s8) = get_constructor_list(s7, ctors_len);
 (Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, store(typ), ctors), s8)
 let (typ, s5) = get_expr(s4);
 let (ctors_len, s6) = get_tag0(s5);
 let (ctors, s7) = get_constructor_list(s6, ctors_len);
 (Inductive.Mk(is_unsafe, lvls, params, indices, store(typ), ctors), s7)
 }

 -- ============================================================================
Expand Down

12 changes: 5 additions & 7 deletions
Ix/IxVM/IxonSerialize.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -387,17 +387,15 @@ def ixonSerialize := ⟦

 fn put_inductive(indc: Inductive, rest: ByteStream) -> ByteStream {
 match indc {
 Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, &typ, ctors) =>
 let bools = recr + 2 * refl + 4 * is_unsafe;
 Inductive.Mk(is_unsafe, lvls, params, indices, &typ, ctors) =>
 let ctors_len = list_length_u64(ctors);
 store(ListNode.Cons(u8_from_field_unsafe(bools),
 store(ListNode.Cons(u8_from_field_unsafe(is_unsafe),
 put_tag0(lvls,
 put_tag0(params,
 put_tag0(indices,
 put_tag0(nested,
 put_expr(typ,
 put_tag0(ctors_len,
 put_constructor_list(ctors, rest))))))))),
 put_expr(typ,
 put_tag0(ctors_len,
 put_constructor_list(ctors, rest)))))))),
 }
 }

Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Force GitHub README to respect dark mode\n(function() {\n var style = document.createElement('style');\n style.textContent = '\n .markdown-body {\n color-scheme: dark light;\n }\n .markdown-body pre { background: #161b22 !important; }\n .markdown-body code { background: rgba(110, 118, 129, 0.4) !important; }\n .markdown-body table th, .markdown-body table td { border-color: #30363d !important; }\n .markdown-body img { background: #0d1117; }\n .markdown-body blockquote { border-left-color: #8b949e; }\n .markdown-body hr { border-color: #30363d; }\n ';\n document.head.appendChild(style);\n})();", "GitHub Dark Mode README Fix");
}
} catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
Compiler fixes for auxiliary constant generation#473

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

johnchandlerburnham
merged 5 commits into

from

Jul 7, 2026
 Merged


Compiler fixes for auxiliary constant generation
#473
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


5 commits


Select commit
Hold shift + click to select a range
62eb9c6

Ixon: drop recr/refl/nested flags from Inductive


johnchandlerburnham Jul 4, 2026
2fc6dda

Compile: evaporated-aux canonicalization and byte-exact aux roundtrip


johnchandlerburnham Jul 4, 2026
fb00cf5

chore: fix clippy warnings and fmt drift


johnchandlerburnham Jul 4, 2026
d8b11c0

IxVM Aiur kernel: fix Lean.Syntax.rec (shard 53) aux-recursor gen


arthurpaulino Jul 1, 2026
2f2a86f

IxVM: port Inductive flag-drop + evaporated-aux aliasing to Aiur kernel


arthurpaulino Jul 4, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


4 changes: 4 additions & 0 deletions
.gitignore

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -7,3 +7,7 @@
# Nix
result*
.direnv/

#Ix
*.ixe
plans

1 change: 1 addition & 0 deletions
Benchmarks/Compile/CompileMutualFixtures.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
import Tests.Ix.Compile.Mutual

29 changes: 28 additions & 1 deletion
Benchmarks/Compile/lake-manifest.json

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -21,6 +21,13 @@
 "inputRev": "v4.29.0",
 "inherited": false,
 "configFile": "lakefile.toml"},
 {"type": "path",
 "scope": "",
 "name": "ix",
 "manifestFile": "lake-manifest.json",
 "inherited": false,
 "dir": "../..",
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/leanprover-community/plausible",
 "type": "git",
 "subDir": null,
Expand DownExpand Up@@ -110,6 +117,26 @@
 "manifestFile": "lake-manifest.json",
 "inputRev": null,
 "inherited": true,
 "configFile": "lakefile.lean"}],
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/argumentcomputer/Blake3.lean",
 "type": "git",
 "subDir": null,
 "scope": "",
 "rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
 "name": "Blake3",
 "manifestFile": "lake-manifest.json",
 "inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
 "inherited": true,
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/argumentcomputer/LSpec",
 "type": "git",
 "subDir": null,
 "scope": "",
 "rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
 "name": "LSpec",
 "manifestFile": "lake-manifest.json",
 "inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
 "inherited": true,
 "configFile": "lakefile.toml"}],
 "name": "Compile",
 "lakeDir": ".lake"}

7 changes: 7 additions & 0 deletions
Benchmarks/Compile/lakefile.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -17,6 +17,13 @@ name = "CompileMathlib"
[[lean_lib]]
name = "CompileFLT"

[[lean_lib]]
name = "CompileMutualFixtures"

[[require]]
name = "ix"
path = "../.."

[[require]]
name = "flt"
git = "https://github.com/ImperialCollegeLondon/FLT"
Expand Down

34 changes: 13 additions & 21 deletions
Ix/Claim.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -94,10 +94,9 @@ structure RevealRecursorRule where
inductive RevealMutConstInfo where
 | defn (kind : Option DefKind) (safety : Option DefinitionSafety)
 (lvls : Option UInt64) (typ : Option Address) (value : Option Address)
 | indc (isRecr : Option Bool) (refl : Option Bool) (isUnsafe : Option Bool)
 (lvls : Option UInt64) (params : Option UInt64)
 (indices : Option UInt64) (nested : Option UInt64)
 (typ : Option Address) (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
 | indc (isUnsafe : Option Bool) (lvls : Option UInt64) (params : Option UInt64)
 (indices : Option UInt64) (typ : Option Address)
 (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
 | recr (k : Option Bool) (isUnsafe : Option Bool) (lvls : Option UInt64)
 (params : Option UInt64) (indices : Option UInt64)
 (motives : Option UInt64) (minors : Option UInt64)
Expand DownExpand Up@@ -240,19 +239,15 @@ def put : RevealMutConstInfo → PutM Unit
 match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
 match typ with | some a => Serialize.put a | none => pure ()
 match value with | some a => Serialize.put a | none => pure ()
 | .indc isRecr refl isUnsafe lvls params indices nested typ ctors => do
 | .indc isUnsafe lvls params indices typ ctors => do
 putU8 1
 let mask := computeMask [isRecr.isSome, refl.isSome, isUnsafe.isSome,
 lvls.isSome, params.isSome, indices.isSome,
 nested.isSome, typ.isSome, ctors.isSome]
 let mask := computeMask [isUnsafe.isSome, lvls.isSome, params.isSome, 
 indices.isSome, typ.isSome, ctors.isSome]
 putTag0 ⟨mask⟩
 match isRecr with | some b => putBoolField b | none => pure ()
 match refl with | some b => putBoolField b | none => pure ()
 match isUnsafe with | some b => putBoolField b | none => pure ()
 match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
 match params with | some n => putTag0 ⟨n⟩ | none => pure ()
 match indices with | some n => putTag0 ⟨n⟩ | none => pure ()
 match nested with | some n => putTag0 ⟨n⟩ | none => pure ()
 match typ with | some a => Serialize.put a | none => pure ()
 match ctors with | some c => putCtors c | none => pure ()
 | .recr k isUnsafe lvls params indices motives minors typ rules => do
Expand DownExpand Up@@ -283,16 +278,13 @@ def get : GetM RevealMutConstInfo := do
 let value ← getOpt mask 16 Serialize.get
 return .defn kind safety lvls typ value
 | 1 => do -- Indc
 let isRecr ← getOpt mask 1 getBoolField
 let refl ← getOpt mask 2 getBoolField
 let isUnsafe ← getOpt mask 4 getBoolField
 let lvls ← getOpt mask 8 getTag0Size
 let params ← getOpt mask 16 getTag0Size
 let indices ← getOpt mask 32 getTag0Size
 let nested ← getOpt mask 64 getTag0Size
 let typ ← getOpt mask 128 Serialize.get
 let ctors ← getOpt mask 256 getCtors
 return .indc isRecr refl isUnsafe lvls params indices nested typ ctors
 let isUnsafe ← getOpt mask 1 getBoolField
 let lvls ← getOpt mask 2 getTag0Size
 let params ← getOpt mask 4 getTag0Size
 let indices ← getOpt mask 8 getTag0Size
 let typ ← getOpt mask 16 Serialize.get
 let ctors ← getOpt mask 32 getCtors
 return .indc isUnsafe lvls params indices typ ctors
 | 2 => do -- Recr
 let k ← getOpt mask 1 getBoolField
 let isUnsafe ← getOpt mask 2 getBoolField
Expand Down

3 changes: 1 addition & 2 deletions
Ix/Commit.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -208,8 +208,7 @@ def openMutConst (mc : Ixon.MutConst) : RevealMutConstInfo :=
 for j in [:i.ctors.size] do
 arr := arr.push (j.toUInt64, openConstructor i.ctors[j]!)
 return arr
 .indc (some i.recr) (some i.refl) (some i.isUnsafe)
 (some i.lvls) (some i.params) (some i.indices) (some i.nested)
 .indc (some i.isUnsafe) (some i.lvls) (some i.params) (some i.indices)
 (some (exprAddr i.typ)) (some ctors)
 | .recr r =>
 let rules := Id.run do
Expand Down

34 changes: 34 additions & 0 deletions
Ix/Common.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -328,6 +328,40 @@ private partial def collectDependenciesAux (const : Lean.ConstantInfo)
 goExpr consts acc val.value
 | .recInfo val =>
 let acc ← collectNames val.all acc
 -- The compiler processes a declaration's recursors as one block, and
 -- they cross-reference in rule RHSs (`A.rec`'s rule calls `A.rec_1`,
 -- `A.rec_2`'s calls `C.rec`), so the closure needs every sibling:
 -- `<ind>.rec` per block inductive plus the nested-aux `<all0>.rec_N`.
 let siblings := val.all.filterMap fun ind =>
 let n := Lean.mkRecName ind
 if consts.contains n then some n else none
 let auxSiblings : List Lean.Name := Id.run do
 let mut out := []
 let mut i := 1
 repeat
 match val.all.head? with
 | none => break
 | some base =>
 let n := Lean.Name.mkStr base s!"rec_{i}"
 if consts.contains n then
 out := n :: out
 i := i + 1
 else break
 return out
 let acc ← collectNames (siblings ++ auxSiblings) acc
 -- A nested-aux recursor's rules recurse via the external container's
 -- ctors; its evaporated form aliases that container's recursor
 -- (`List.rec`), which no collected expr mentions — pull it via each
 -- rule ctor's owning inductive.
 let extRecs := val.rules.filterMap fun rule =>
 match consts.find? rule.ctor with
 | some (.ctorInfo cv) =>
 if val.all.contains cv.induct then none
 else
 let n := Lean.mkRecName cv.induct
 if consts.contains n then some n else none
 | _ => none
 let acc ← collectNames extRecs acc
 let acc ← goExpr consts acc val.type
 val.rules.foldlM (init := acc) fun acc rule => goExpr consts acc rule.rhs
where
Expand Down

6 changes: 0 additions & 6 deletions
Ix/CompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -1112,13 +1112,10 @@ def compileInductive (i : InductiveVal) (ctorVals : Array ConstructorVal)
 let ctxAddrs ← getMutCtxAddrs

 let ind : Ixon.Inductive := {
 recr := i.isRec
 refl := i.isReflexive
 isUnsafe := i.isUnsafe
 lvls := i.cnst.levelParams.size.toUInt64
 params := i.numParams.toUInt64
 indices := i.numIndices.toUInt64
 nested := i.numNested.toUInt64
 typ := typeExpr
 ctors := ctors
 }
Expand DownExpand Up@@ -1194,13 +1191,10 @@ def compileInductiveData (i : Ind)
 let ctxAddrs ← getMutCtxAddrs

 let ind : Ixon.Inductive := {
 recr := i.isRec
 refl := i.isReflexive
 isUnsafe := i.isUnsafe
 lvls := i.levelParams.size.toUInt64
 params := i.numParams.toUInt64
 indices := i.numIndices.toUInt64
 nested := i.numNested.toUInt64
 typ := typeExpr
 ctors := ctors
 }
Expand Down

5 changes: 3 additions & 2 deletions
Ix/DecompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -670,8 +670,9 @@ def decompileInductive (ind : Ixon.Inductive) (cnst : Constant) (cMeta : Constan
 cnst := { name, levelParams := univParams, type := typeExpr },
 numParams := ind.params.toNat, numIndices := ind.indices.toNat,
 all := allNames, ctors := ctorNames,
 numNested := ind.nested.toNat, isRec := ind.recr,
 isUnsafe := ind.isUnsafe, isReflexive := ind.refl }
 -- temporary stub until we update the Lean compiler and decompiler semantics
 numNested := 0, isRec := false
 isUnsafe := ind.isUnsafe, isReflexive := false }
 pure (indVal, ctors)

/-! ## Projection Handling -/
Expand Down

4 changes: 2 additions & 2 deletions
Ix/IxVM/Convert.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -314,11 +314,11 @@ def convert := ⟦
 match ctx {
 ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
 match ind {
 Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, typ, _) =>
 Inductive.Mk(is_unsafe, lvls, params, indices, typ, _) =>
 let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
 KConstantInfo.Induct(
 flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
 ctor_idxs, is_rec, is_refl, is_unsafe, flatten_u64(nested), block_addr),
 ctor_idxs, is_unsafe, block_addr),
 },
 }
 }
Expand Down

10 changes: 5 additions & 5 deletions
Ix/IxVM/Ingress.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -175,7 +175,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 list_length(ctors) + 1,
 },
 MutConst.Recr(_) => 1,
Expand DownExpand Up@@ -850,7 +850,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 let num_ctors = list_length(ctors);
 let this_ctors = build_ctor_idxs(num_ctors, cur_pos, 0);
 let rest_ctors = build_rule_ctor_idxs_walk(rest,
Expand DownExpand Up@@ -998,7 +998,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 build_ctor_idxs(list_length(ctors), cur_pos, 0),
 },
 _ => store(ListNode.Nil),
Expand DownExpand Up@@ -1027,7 +1027,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 let num_ctors = list_length(ctors);
 let induct_pos = block_start + member_offset(members, member_idx);
 let ctor_idxs = build_ctor_idxs(num_ctors, induct_pos, 0);
Expand DownExpand Up@@ -1546,7 +1546,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 list_length(ctors),
 },
 _ => 0,
Expand Down

4 changes: 2 additions & 2 deletions
Ix/IxVM/Ixon.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -83,9 +83,9 @@ def ixon := ⟦
 Mk(G, U64, U64, U64, U64, &Expr)
 }

 -- Inductive: (recr, refl, is_unsafe, lvls, params, indices, nested, typ, ctors)
 -- Inductive: (is_unsafe, lvls, params, indices, typ, ctors)
 enum Inductive {
 Mk(G, G, G, U64, U64, U64, U64, &Expr, List‹Constructor›)
 Mk(G, U64, U64, U64, &Expr, List‹Constructor›)
 }

 -- InductiveProj: (idx, block_address)
Expand Down

15 changes: 6 additions & 9 deletions
Ix/IxVM/IxonDeserialize.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -479,21 +479,18 @@ def ixonDeserialize := ⟦
 }

 -- Inductive: byte(bools) + Tag0(lvls) + Tag0(params) + Tag0(indices) +
 -- Tag0(nested) + expr(typ) + Tag0(ctors_len) + ctors...
 -- expr(typ) + Tag0(ctors_len) + ctors...
 fn get_inductive(stream: ByteStream) -> (Inductive, ByteStream) {
 let (bools_byte, s) = read_byte(stream);
 let bits = u8_bit_decomposition(bools_byte);
 let recr = bits[0];
 let refl = bits[1];
 let is_unsafe = bits[2];
 let is_unsafe = bits[0];
 let (lvls, s2) = get_tag0(s);
 let (params, s3) = get_tag0(s2);
 let (indices, s4) = get_tag0(s3);
 let (nested, s5) = get_tag0(s4);
 let (typ, s6) = get_expr(s5);
 let (ctors_len, s7) = get_tag0(s6);
 let (ctors, s8) = get_constructor_list(s7, ctors_len);
 (Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, store(typ), ctors), s8)
 let (typ, s5) = get_expr(s4);
 let (ctors_len, s6) = get_tag0(s5);
 let (ctors, s7) = get_constructor_list(s6, ctors_len);
 (Inductive.Mk(is_unsafe, lvls, params, indices, store(typ), ctors), s7)
 }

 -- ============================================================================
Expand Down

12 changes: 5 additions & 7 deletions
Ix/IxVM/IxonSerialize.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -387,17 +387,15 @@ def ixonSerialize := ⟦

 fn put_inductive(indc: Inductive, rest: ByteStream) -> ByteStream {
 match indc {
 Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, &typ, ctors) =>
 let bools = recr + 2 * refl + 4 * is_unsafe;
 Inductive.Mk(is_unsafe, lvls, params, indices, &typ, ctors) =>
 let ctors_len = list_length_u64(ctors);
 store(ListNode.Cons(u8_from_field_unsafe(bools),
 store(ListNode.Cons(u8_from_field_unsafe(is_unsafe),
 put_tag0(lvls,
 put_tag0(params,
 put_tag0(indices,
 put_tag0(nested,
 put_expr(typ,
 put_tag0(ctors_len,
 put_constructor_list(ctors, rest))))))))),
 put_expr(typ,
 put_tag0(ctors_len,
 put_constructor_list(ctors, rest)))))))),
 }
 }

Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Highlight search terms from Google/DuckDuckGo/Bing referrer\n(function() {\n var ref = document.referrer;\n var terms = [];\n \n if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) {\n var url = new URL(ref);\n var q = url.searchParams.get('q') || url.searchParams.get('p');\n if (q) {\n terms = q.split(/\\s+/).filter(function(t) { return t.length > 2; });\n }\n }\n \n if (terms.length === 0) return;\n \n var style = document.createElement('style');\n style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';\n document.head.appendChild(style);\n \n function highlight(node) {\n if (node.nodeType === 3) { // text node\n var text = node.textContent;\n var found = false;\n terms.forEach(function(term) {\n var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\\]\\\\]/g, '\\\\') + ')', 'gi');\n if (regex.test(text)) {\n found = true;\n var frag = document.createDocumentFragment();\n var parts = text.split(regex);\n parts.forEach(function(part, i) {\n if (i % 2 === 0) {\n frag.appendChild(document.createTextNode(part));\n } else {\n var span = document.createElement('span');\n span.className = 'userscript-highlight';\n span.textContent = part;\n frag.appendChild(span);\n }\n });\n node.parentNode.replaceChild(frag, node);\n }\n });\n } else if (node.nodeType === 1 && node.childNodes) { // element\n var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];\n if (!skipTags.includes(node.tagName)) {\n Array.from(node.childNodes).forEach(highlight);\n }\n }\n }\n \n highlight(document.body);\n \n // Re-highlight on dynamic content\n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1 || node.nodeType === 3) highlight(node);\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Highlight Search Terms");
}
} catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
Compiler fixes for auxiliary constant generation#473

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

johnchandlerburnham
merged 5 commits into

from

Jul 7, 2026
 Merged


Compiler fixes for auxiliary constant generation
#473
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


5 commits


Select commit
Hold shift + click to select a range
62eb9c6

Ixon: drop recr/refl/nested flags from Inductive


johnchandlerburnham Jul 4, 2026
2fc6dda

Compile: evaporated-aux canonicalization and byte-exact aux roundtrip


johnchandlerburnham Jul 4, 2026
fb00cf5

chore: fix clippy warnings and fmt drift


johnchandlerburnham Jul 4, 2026
d8b11c0

IxVM Aiur kernel: fix Lean.Syntax.rec (shard 53) aux-recursor gen


arthurpaulino Jul 1, 2026
2f2a86f

IxVM: port Inductive flag-drop + evaporated-aux aliasing to Aiur kernel


arthurpaulino Jul 4, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


4 changes: 4 additions & 0 deletions
.gitignore

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -7,3 +7,7 @@
# Nix
result*
.direnv/

#Ix
*.ixe
plans

1 change: 1 addition & 0 deletions
Benchmarks/Compile/CompileMutualFixtures.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
import Tests.Ix.Compile.Mutual

29 changes: 28 additions & 1 deletion
Benchmarks/Compile/lake-manifest.json

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -21,6 +21,13 @@
 "inputRev": "v4.29.0",
 "inherited": false,
 "configFile": "lakefile.toml"},
 {"type": "path",
 "scope": "",
 "name": "ix",
 "manifestFile": "lake-manifest.json",
 "inherited": false,
 "dir": "../..",
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/leanprover-community/plausible",
 "type": "git",
 "subDir": null,
Expand DownExpand Up@@ -110,6 +117,26 @@
 "manifestFile": "lake-manifest.json",
 "inputRev": null,
 "inherited": true,
 "configFile": "lakefile.lean"}],
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/argumentcomputer/Blake3.lean",
 "type": "git",
 "subDir": null,
 "scope": "",
 "rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
 "name": "Blake3",
 "manifestFile": "lake-manifest.json",
 "inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
 "inherited": true,
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/argumentcomputer/LSpec",
 "type": "git",
 "subDir": null,
 "scope": "",
 "rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
 "name": "LSpec",
 "manifestFile": "lake-manifest.json",
 "inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
 "inherited": true,
 "configFile": "lakefile.toml"}],
 "name": "Compile",
 "lakeDir": ".lake"}

7 changes: 7 additions & 0 deletions
Benchmarks/Compile/lakefile.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -17,6 +17,13 @@ name = "CompileMathlib"
[[lean_lib]]
name = "CompileFLT"

[[lean_lib]]
name = "CompileMutualFixtures"

[[require]]
name = "ix"
path = "../.."

[[require]]
name = "flt"
git = "https://github.com/ImperialCollegeLondon/FLT"
Expand Down

34 changes: 13 additions & 21 deletions
Ix/Claim.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -94,10 +94,9 @@ structure RevealRecursorRule where
inductive RevealMutConstInfo where
 | defn (kind : Option DefKind) (safety : Option DefinitionSafety)
 (lvls : Option UInt64) (typ : Option Address) (value : Option Address)
 | indc (isRecr : Option Bool) (refl : Option Bool) (isUnsafe : Option Bool)
 (lvls : Option UInt64) (params : Option UInt64)
 (indices : Option UInt64) (nested : Option UInt64)
 (typ : Option Address) (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
 | indc (isUnsafe : Option Bool) (lvls : Option UInt64) (params : Option UInt64)
 (indices : Option UInt64) (typ : Option Address)
 (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
 | recr (k : Option Bool) (isUnsafe : Option Bool) (lvls : Option UInt64)
 (params : Option UInt64) (indices : Option UInt64)
 (motives : Option UInt64) (minors : Option UInt64)
Expand DownExpand Up@@ -240,19 +239,15 @@ def put : RevealMutConstInfo → PutM Unit
 match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
 match typ with | some a => Serialize.put a | none => pure ()
 match value with | some a => Serialize.put a | none => pure ()
 | .indc isRecr refl isUnsafe lvls params indices nested typ ctors => do
 | .indc isUnsafe lvls params indices typ ctors => do
 putU8 1
 let mask := computeMask [isRecr.isSome, refl.isSome, isUnsafe.isSome,
 lvls.isSome, params.isSome, indices.isSome,
 nested.isSome, typ.isSome, ctors.isSome]
 let mask := computeMask [isUnsafe.isSome, lvls.isSome, params.isSome, 
 indices.isSome, typ.isSome, ctors.isSome]
 putTag0 ⟨mask⟩
 match isRecr with | some b => putBoolField b | none => pure ()
 match refl with | some b => putBoolField b | none => pure ()
 match isUnsafe with | some b => putBoolField b | none => pure ()
 match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
 match params with | some n => putTag0 ⟨n⟩ | none => pure ()
 match indices with | some n => putTag0 ⟨n⟩ | none => pure ()
 match nested with | some n => putTag0 ⟨n⟩ | none => pure ()
 match typ with | some a => Serialize.put a | none => pure ()
 match ctors with | some c => putCtors c | none => pure ()
 | .recr k isUnsafe lvls params indices motives minors typ rules => do
Expand DownExpand Up@@ -283,16 +278,13 @@ def get : GetM RevealMutConstInfo := do
 let value ← getOpt mask 16 Serialize.get
 return .defn kind safety lvls typ value
 | 1 => do -- Indc
 let isRecr ← getOpt mask 1 getBoolField
 let refl ← getOpt mask 2 getBoolField
 let isUnsafe ← getOpt mask 4 getBoolField
 let lvls ← getOpt mask 8 getTag0Size
 let params ← getOpt mask 16 getTag0Size
 let indices ← getOpt mask 32 getTag0Size
 let nested ← getOpt mask 64 getTag0Size
 let typ ← getOpt mask 128 Serialize.get
 let ctors ← getOpt mask 256 getCtors
 return .indc isRecr refl isUnsafe lvls params indices nested typ ctors
 let isUnsafe ← getOpt mask 1 getBoolField
 let lvls ← getOpt mask 2 getTag0Size
 let params ← getOpt mask 4 getTag0Size
 let indices ← getOpt mask 8 getTag0Size
 let typ ← getOpt mask 16 Serialize.get
 let ctors ← getOpt mask 32 getCtors
 return .indc isUnsafe lvls params indices typ ctors
 | 2 => do -- Recr
 let k ← getOpt mask 1 getBoolField
 let isUnsafe ← getOpt mask 2 getBoolField
Expand Down

3 changes: 1 addition & 2 deletions
Ix/Commit.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -208,8 +208,7 @@ def openMutConst (mc : Ixon.MutConst) : RevealMutConstInfo :=
 for j in [:i.ctors.size] do
 arr := arr.push (j.toUInt64, openConstructor i.ctors[j]!)
 return arr
 .indc (some i.recr) (some i.refl) (some i.isUnsafe)
 (some i.lvls) (some i.params) (some i.indices) (some i.nested)
 .indc (some i.isUnsafe) (some i.lvls) (some i.params) (some i.indices)
 (some (exprAddr i.typ)) (some ctors)
 | .recr r =>
 let rules := Id.run do
Expand Down

34 changes: 34 additions & 0 deletions
Ix/Common.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -328,6 +328,40 @@ private partial def collectDependenciesAux (const : Lean.ConstantInfo)
 goExpr consts acc val.value
 | .recInfo val =>
 let acc ← collectNames val.all acc
 -- The compiler processes a declaration's recursors as one block, and
 -- they cross-reference in rule RHSs (`A.rec`'s rule calls `A.rec_1`,
 -- `A.rec_2`'s calls `C.rec`), so the closure needs every sibling:
 -- `<ind>.rec` per block inductive plus the nested-aux `<all0>.rec_N`.
 let siblings := val.all.filterMap fun ind =>
 let n := Lean.mkRecName ind
 if consts.contains n then some n else none
 let auxSiblings : List Lean.Name := Id.run do
 let mut out := []
 let mut i := 1
 repeat
 match val.all.head? with
 | none => break
 | some base =>
 let n := Lean.Name.mkStr base s!"rec_{i}"
 if consts.contains n then
 out := n :: out
 i := i + 1
 else break
 return out
 let acc ← collectNames (siblings ++ auxSiblings) acc
 -- A nested-aux recursor's rules recurse via the external container's
 -- ctors; its evaporated form aliases that container's recursor
 -- (`List.rec`), which no collected expr mentions — pull it via each
 -- rule ctor's owning inductive.
 let extRecs := val.rules.filterMap fun rule =>
 match consts.find? rule.ctor with
 | some (.ctorInfo cv) =>
 if val.all.contains cv.induct then none
 else
 let n := Lean.mkRecName cv.induct
 if consts.contains n then some n else none
 | _ => none
 let acc ← collectNames extRecs acc
 let acc ← goExpr consts acc val.type
 val.rules.foldlM (init := acc) fun acc rule => goExpr consts acc rule.rhs
where
Expand Down

6 changes: 0 additions & 6 deletions
Ix/CompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -1112,13 +1112,10 @@ def compileInductive (i : InductiveVal) (ctorVals : Array ConstructorVal)
 let ctxAddrs ← getMutCtxAddrs

 let ind : Ixon.Inductive := {
 recr := i.isRec
 refl := i.isReflexive
 isUnsafe := i.isUnsafe
 lvls := i.cnst.levelParams.size.toUInt64
 params := i.numParams.toUInt64
 indices := i.numIndices.toUInt64
 nested := i.numNested.toUInt64
 typ := typeExpr
 ctors := ctors
 }
Expand DownExpand Up@@ -1194,13 +1191,10 @@ def compileInductiveData (i : Ind)
 let ctxAddrs ← getMutCtxAddrs

 let ind : Ixon.Inductive := {
 recr := i.isRec
 refl := i.isReflexive
 isUnsafe := i.isUnsafe
 lvls := i.levelParams.size.toUInt64
 params := i.numParams.toUInt64
 indices := i.numIndices.toUInt64
 nested := i.numNested.toUInt64
 typ := typeExpr
 ctors := ctors
 }
Expand Down

5 changes: 3 additions & 2 deletions
Ix/DecompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -670,8 +670,9 @@ def decompileInductive (ind : Ixon.Inductive) (cnst : Constant) (cMeta : Constan
 cnst := { name, levelParams := univParams, type := typeExpr },
 numParams := ind.params.toNat, numIndices := ind.indices.toNat,
 all := allNames, ctors := ctorNames,
 numNested := ind.nested.toNat, isRec := ind.recr,
 isUnsafe := ind.isUnsafe, isReflexive := ind.refl }
 -- temporary stub until we update the Lean compiler and decompiler semantics
 numNested := 0, isRec := false
 isUnsafe := ind.isUnsafe, isReflexive := false }
 pure (indVal, ctors)

/-! ## Projection Handling -/
Expand Down

4 changes: 2 additions & 2 deletions
Ix/IxVM/Convert.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -314,11 +314,11 @@ def convert := ⟦
 match ctx {
 ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
 match ind {
 Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, typ, _) =>
 Inductive.Mk(is_unsafe, lvls, params, indices, typ, _) =>
 let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
 KConstantInfo.Induct(
 flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
 ctor_idxs, is_rec, is_refl, is_unsafe, flatten_u64(nested), block_addr),
 ctor_idxs, is_unsafe, block_addr),
 },
 }
 }
Expand Down

10 changes: 5 additions & 5 deletions
Ix/IxVM/Ingress.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -175,7 +175,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 list_length(ctors) + 1,
 },
 MutConst.Recr(_) => 1,
Expand DownExpand Up@@ -850,7 +850,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 let num_ctors = list_length(ctors);
 let this_ctors = build_ctor_idxs(num_ctors, cur_pos, 0);
 let rest_ctors = build_rule_ctor_idxs_walk(rest,
Expand DownExpand Up@@ -998,7 +998,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 build_ctor_idxs(list_length(ctors), cur_pos, 0),
 },
 _ => store(ListNode.Nil),
Expand DownExpand Up@@ -1027,7 +1027,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 let num_ctors = list_length(ctors);
 let induct_pos = block_start + member_offset(members, member_idx);
 let ctor_idxs = build_ctor_idxs(num_ctors, induct_pos, 0);
Expand DownExpand Up@@ -1546,7 +1546,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 list_length(ctors),
 },
 _ => 0,
Expand Down

4 changes: 2 additions & 2 deletions
Ix/IxVM/Ixon.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -83,9 +83,9 @@ def ixon := ⟦
 Mk(G, U64, U64, U64, U64, &Expr)
 }

 -- Inductive: (recr, refl, is_unsafe, lvls, params, indices, nested, typ, ctors)
 -- Inductive: (is_unsafe, lvls, params, indices, typ, ctors)
 enum Inductive {
 Mk(G, G, G, U64, U64, U64, U64, &Expr, List‹Constructor›)
 Mk(G, U64, U64, U64, &Expr, List‹Constructor›)
 }

 -- InductiveProj: (idx, block_address)
Expand Down

15 changes: 6 additions & 9 deletions
Ix/IxVM/IxonDeserialize.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -479,21 +479,18 @@ def ixonDeserialize := ⟦
 }

 -- Inductive: byte(bools) + Tag0(lvls) + Tag0(params) + Tag0(indices) +
 -- Tag0(nested) + expr(typ) + Tag0(ctors_len) + ctors...
 -- expr(typ) + Tag0(ctors_len) + ctors...
 fn get_inductive(stream: ByteStream) -> (Inductive, ByteStream) {
 let (bools_byte, s) = read_byte(stream);
 let bits = u8_bit_decomposition(bools_byte);
 let recr = bits[0];
 let refl = bits[1];
 let is_unsafe = bits[2];
 let is_unsafe = bits[0];
 let (lvls, s2) = get_tag0(s);
 let (params, s3) = get_tag0(s2);
 let (indices, s4) = get_tag0(s3);
 let (nested, s5) = get_tag0(s4);
 let (typ, s6) = get_expr(s5);
 let (ctors_len, s7) = get_tag0(s6);
 let (ctors, s8) = get_constructor_list(s7, ctors_len);
 (Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, store(typ), ctors), s8)
 let (typ, s5) = get_expr(s4);
 let (ctors_len, s6) = get_tag0(s5);
 let (ctors, s7) = get_constructor_list(s6, ctors_len);
 (Inductive.Mk(is_unsafe, lvls, params, indices, store(typ), ctors), s7)
 }

 -- ============================================================================
Expand Down

12 changes: 5 additions & 7 deletions
Ix/IxVM/IxonSerialize.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -387,17 +387,15 @@ def ixonSerialize := ⟦

 fn put_inductive(indc: Inductive, rest: ByteStream) -> ByteStream {
 match indc {
 Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, &typ, ctors) =>
 let bools = recr + 2 * refl + 4 * is_unsafe;
 Inductive.Mk(is_unsafe, lvls, params, indices, &typ, ctors) =>
 let ctors_len = list_length_u64(ctors);
 store(ListNode.Cons(u8_from_field_unsafe(bools),
 store(ListNode.Cons(u8_from_field_unsafe(is_unsafe),
 put_tag0(lvls,
 put_tag0(params,
 put_tag0(indices,
 put_tag0(nested,
 put_expr(typ,
 put_tag0(ctors_len,
 put_constructor_list(ctors, rest))))))))),
 put_expr(typ,
 put_tag0(ctors_len,
 put_constructor_list(ctors, rest)))))))),
 }
 }

Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Strip utm_, fbclid, gclid, etc. from all links on page\n(function() {\n var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content',\n 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid',\n 'ref', 'ref_src', 'source', 'medium', 'campaign'];\n \n function cleanUrl(url) {\n try {\n var u = new URL(url, window.location.origin);\n var changed = false;\n trackingParams.forEach(function(p) {\n if (u.searchParams.has(p)) {\n u.searchParams.delete(p);\n changed = true;\n }\n });\n return changed ? u.toString() : url;\n } catch (e) {\n return url;\n }\n }\n \n function cleanLinks() {\n document.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n \n cleanLinks();\n \n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1) {\n if (node.tagName === 'A') cleanLinks();\n node.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Remove Tracking Parameters from Links");
}
} catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); }
})();
(function(){
try {
var __m = "youtube.com";
var __re = new RegExp('^' + "youtube\\.com" + '

Skip to content
Compiler fixes for auxiliary constant generation#473

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

johnchandlerburnham
merged 5 commits into

from

Jul 7, 2026
 Merged


Compiler fixes for auxiliary constant generation
#473
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


5 commits


Select commit
Hold shift + click to select a range
62eb9c6

Ixon: drop recr/refl/nested flags from Inductive


johnchandlerburnham Jul 4, 2026
2fc6dda

Compile: evaporated-aux canonicalization and byte-exact aux roundtrip


johnchandlerburnham Jul 4, 2026
fb00cf5

chore: fix clippy warnings and fmt drift


johnchandlerburnham Jul 4, 2026
d8b11c0

IxVM Aiur kernel: fix Lean.Syntax.rec (shard 53) aux-recursor gen


arthurpaulino Jul 1, 2026
2f2a86f

IxVM: port Inductive flag-drop + evaporated-aux aliasing to Aiur kernel


arthurpaulino Jul 4, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


4 changes: 4 additions & 0 deletions
.gitignore

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -7,3 +7,7 @@
# Nix
result*
.direnv/

#Ix
*.ixe
plans

1 change: 1 addition & 0 deletions
Benchmarks/Compile/CompileMutualFixtures.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
import Tests.Ix.Compile.Mutual

29 changes: 28 additions & 1 deletion
Benchmarks/Compile/lake-manifest.json

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -21,6 +21,13 @@
 "inputRev": "v4.29.0",
 "inherited": false,
 "configFile": "lakefile.toml"},
 {"type": "path",
 "scope": "",
 "name": "ix",
 "manifestFile": "lake-manifest.json",
 "inherited": false,
 "dir": "../..",
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/leanprover-community/plausible",
 "type": "git",
 "subDir": null,
Expand DownExpand Up@@ -110,6 +117,26 @@
 "manifestFile": "lake-manifest.json",
 "inputRev": null,
 "inherited": true,
 "configFile": "lakefile.lean"}],
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/argumentcomputer/Blake3.lean",
 "type": "git",
 "subDir": null,
 "scope": "",
 "rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
 "name": "Blake3",
 "manifestFile": "lake-manifest.json",
 "inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
 "inherited": true,
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/argumentcomputer/LSpec",
 "type": "git",
 "subDir": null,
 "scope": "",
 "rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
 "name": "LSpec",
 "manifestFile": "lake-manifest.json",
 "inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
 "inherited": true,
 "configFile": "lakefile.toml"}],
 "name": "Compile",
 "lakeDir": ".lake"}

7 changes: 7 additions & 0 deletions
Benchmarks/Compile/lakefile.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -17,6 +17,13 @@ name = "CompileMathlib"
[[lean_lib]]
name = "CompileFLT"

[[lean_lib]]
name = "CompileMutualFixtures"

[[require]]
name = "ix"
path = "../.."

[[require]]
name = "flt"
git = "https://github.com/ImperialCollegeLondon/FLT"
Expand Down

34 changes: 13 additions & 21 deletions
Ix/Claim.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -94,10 +94,9 @@ structure RevealRecursorRule where
inductive RevealMutConstInfo where
 | defn (kind : Option DefKind) (safety : Option DefinitionSafety)
 (lvls : Option UInt64) (typ : Option Address) (value : Option Address)
 | indc (isRecr : Option Bool) (refl : Option Bool) (isUnsafe : Option Bool)
 (lvls : Option UInt64) (params : Option UInt64)
 (indices : Option UInt64) (nested : Option UInt64)
 (typ : Option Address) (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
 | indc (isUnsafe : Option Bool) (lvls : Option UInt64) (params : Option UInt64)
 (indices : Option UInt64) (typ : Option Address)
 (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
 | recr (k : Option Bool) (isUnsafe : Option Bool) (lvls : Option UInt64)
 (params : Option UInt64) (indices : Option UInt64)
 (motives : Option UInt64) (minors : Option UInt64)
Expand DownExpand Up@@ -240,19 +239,15 @@ def put : RevealMutConstInfo → PutM Unit
 match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
 match typ with | some a => Serialize.put a | none => pure ()
 match value with | some a => Serialize.put a | none => pure ()
 | .indc isRecr refl isUnsafe lvls params indices nested typ ctors => do
 | .indc isUnsafe lvls params indices typ ctors => do
 putU8 1
 let mask := computeMask [isRecr.isSome, refl.isSome, isUnsafe.isSome,
 lvls.isSome, params.isSome, indices.isSome,
 nested.isSome, typ.isSome, ctors.isSome]
 let mask := computeMask [isUnsafe.isSome, lvls.isSome, params.isSome, 
 indices.isSome, typ.isSome, ctors.isSome]
 putTag0 ⟨mask⟩
 match isRecr with | some b => putBoolField b | none => pure ()
 match refl with | some b => putBoolField b | none => pure ()
 match isUnsafe with | some b => putBoolField b | none => pure ()
 match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
 match params with | some n => putTag0 ⟨n⟩ | none => pure ()
 match indices with | some n => putTag0 ⟨n⟩ | none => pure ()
 match nested with | some n => putTag0 ⟨n⟩ | none => pure ()
 match typ with | some a => Serialize.put a | none => pure ()
 match ctors with | some c => putCtors c | none => pure ()
 | .recr k isUnsafe lvls params indices motives minors typ rules => do
Expand DownExpand Up@@ -283,16 +278,13 @@ def get : GetM RevealMutConstInfo := do
 let value ← getOpt mask 16 Serialize.get
 return .defn kind safety lvls typ value
 | 1 => do -- Indc
 let isRecr ← getOpt mask 1 getBoolField
 let refl ← getOpt mask 2 getBoolField
 let isUnsafe ← getOpt mask 4 getBoolField
 let lvls ← getOpt mask 8 getTag0Size
 let params ← getOpt mask 16 getTag0Size
 let indices ← getOpt mask 32 getTag0Size
 let nested ← getOpt mask 64 getTag0Size
 let typ ← getOpt mask 128 Serialize.get
 let ctors ← getOpt mask 256 getCtors
 return .indc isRecr refl isUnsafe lvls params indices nested typ ctors
 let isUnsafe ← getOpt mask 1 getBoolField
 let lvls ← getOpt mask 2 getTag0Size
 let params ← getOpt mask 4 getTag0Size
 let indices ← getOpt mask 8 getTag0Size
 let typ ← getOpt mask 16 Serialize.get
 let ctors ← getOpt mask 32 getCtors
 return .indc isUnsafe lvls params indices typ ctors
 | 2 => do -- Recr
 let k ← getOpt mask 1 getBoolField
 let isUnsafe ← getOpt mask 2 getBoolField
Expand Down

3 changes: 1 addition & 2 deletions
Ix/Commit.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -208,8 +208,7 @@ def openMutConst (mc : Ixon.MutConst) : RevealMutConstInfo :=
 for j in [:i.ctors.size] do
 arr := arr.push (j.toUInt64, openConstructor i.ctors[j]!)
 return arr
 .indc (some i.recr) (some i.refl) (some i.isUnsafe)
 (some i.lvls) (some i.params) (some i.indices) (some i.nested)
 .indc (some i.isUnsafe) (some i.lvls) (some i.params) (some i.indices)
 (some (exprAddr i.typ)) (some ctors)
 | .recr r =>
 let rules := Id.run do
Expand Down

34 changes: 34 additions & 0 deletions
Ix/Common.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -328,6 +328,40 @@ private partial def collectDependenciesAux (const : Lean.ConstantInfo)
 goExpr consts acc val.value
 | .recInfo val =>
 let acc ← collectNames val.all acc
 -- The compiler processes a declaration's recursors as one block, and
 -- they cross-reference in rule RHSs (`A.rec`'s rule calls `A.rec_1`,
 -- `A.rec_2`'s calls `C.rec`), so the closure needs every sibling:
 -- `<ind>.rec` per block inductive plus the nested-aux `<all0>.rec_N`.
 let siblings := val.all.filterMap fun ind =>
 let n := Lean.mkRecName ind
 if consts.contains n then some n else none
 let auxSiblings : List Lean.Name := Id.run do
 let mut out := []
 let mut i := 1
 repeat
 match val.all.head? with
 | none => break
 | some base =>
 let n := Lean.Name.mkStr base s!"rec_{i}"
 if consts.contains n then
 out := n :: out
 i := i + 1
 else break
 return out
 let acc ← collectNames (siblings ++ auxSiblings) acc
 -- A nested-aux recursor's rules recurse via the external container's
 -- ctors; its evaporated form aliases that container's recursor
 -- (`List.rec`), which no collected expr mentions — pull it via each
 -- rule ctor's owning inductive.
 let extRecs := val.rules.filterMap fun rule =>
 match consts.find? rule.ctor with
 | some (.ctorInfo cv) =>
 if val.all.contains cv.induct then none
 else
 let n := Lean.mkRecName cv.induct
 if consts.contains n then some n else none
 | _ => none
 let acc ← collectNames extRecs acc
 let acc ← goExpr consts acc val.type
 val.rules.foldlM (init := acc) fun acc rule => goExpr consts acc rule.rhs
where
Expand Down

6 changes: 0 additions & 6 deletions
Ix/CompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -1112,13 +1112,10 @@ def compileInductive (i : InductiveVal) (ctorVals : Array ConstructorVal)
 let ctxAddrs ← getMutCtxAddrs

 let ind : Ixon.Inductive := {
 recr := i.isRec
 refl := i.isReflexive
 isUnsafe := i.isUnsafe
 lvls := i.cnst.levelParams.size.toUInt64
 params := i.numParams.toUInt64
 indices := i.numIndices.toUInt64
 nested := i.numNested.toUInt64
 typ := typeExpr
 ctors := ctors
 }
Expand DownExpand Up@@ -1194,13 +1191,10 @@ def compileInductiveData (i : Ind)
 let ctxAddrs ← getMutCtxAddrs

 let ind : Ixon.Inductive := {
 recr := i.isRec
 refl := i.isReflexive
 isUnsafe := i.isUnsafe
 lvls := i.levelParams.size.toUInt64
 params := i.numParams.toUInt64
 indices := i.numIndices.toUInt64
 nested := i.numNested.toUInt64
 typ := typeExpr
 ctors := ctors
 }
Expand Down

5 changes: 3 additions & 2 deletions
Ix/DecompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -670,8 +670,9 @@ def decompileInductive (ind : Ixon.Inductive) (cnst : Constant) (cMeta : Constan
 cnst := { name, levelParams := univParams, type := typeExpr },
 numParams := ind.params.toNat, numIndices := ind.indices.toNat,
 all := allNames, ctors := ctorNames,
 numNested := ind.nested.toNat, isRec := ind.recr,
 isUnsafe := ind.isUnsafe, isReflexive := ind.refl }
 -- temporary stub until we update the Lean compiler and decompiler semantics
 numNested := 0, isRec := false
 isUnsafe := ind.isUnsafe, isReflexive := false }
 pure (indVal, ctors)

/-! ## Projection Handling -/
Expand Down

4 changes: 2 additions & 2 deletions
Ix/IxVM/Convert.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -314,11 +314,11 @@ def convert := ⟦
 match ctx {
 ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
 match ind {
 Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, typ, _) =>
 Inductive.Mk(is_unsafe, lvls, params, indices, typ, _) =>
 let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
 KConstantInfo.Induct(
 flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
 ctor_idxs, is_rec, is_refl, is_unsafe, flatten_u64(nested), block_addr),
 ctor_idxs, is_unsafe, block_addr),
 },
 }
 }
Expand Down

10 changes: 5 additions & 5 deletions
Ix/IxVM/Ingress.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -175,7 +175,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 list_length(ctors) + 1,
 },
 MutConst.Recr(_) => 1,
Expand DownExpand Up@@ -850,7 +850,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 let num_ctors = list_length(ctors);
 let this_ctors = build_ctor_idxs(num_ctors, cur_pos, 0);
 let rest_ctors = build_rule_ctor_idxs_walk(rest,
Expand DownExpand Up@@ -998,7 +998,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 build_ctor_idxs(list_length(ctors), cur_pos, 0),
 },
 _ => store(ListNode.Nil),
Expand DownExpand Up@@ -1027,7 +1027,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 let num_ctors = list_length(ctors);
 let induct_pos = block_start + member_offset(members, member_idx);
 let ctor_idxs = build_ctor_idxs(num_ctors, induct_pos, 0);
Expand DownExpand Up@@ -1546,7 +1546,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 list_length(ctors),
 },
 _ => 0,
Expand Down

4 changes: 2 additions & 2 deletions
Ix/IxVM/Ixon.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -83,9 +83,9 @@ def ixon := ⟦
 Mk(G, U64, U64, U64, U64, &Expr)
 }

 -- Inductive: (recr, refl, is_unsafe, lvls, params, indices, nested, typ, ctors)
 -- Inductive: (is_unsafe, lvls, params, indices, typ, ctors)
 enum Inductive {
 Mk(G, G, G, U64, U64, U64, U64, &Expr, List‹Constructor›)
 Mk(G, U64, U64, U64, &Expr, List‹Constructor›)
 }

 -- InductiveProj: (idx, block_address)
Expand Down

15 changes: 6 additions & 9 deletions
Ix/IxVM/IxonDeserialize.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -479,21 +479,18 @@ def ixonDeserialize := ⟦
 }

 -- Inductive: byte(bools) + Tag0(lvls) + Tag0(params) + Tag0(indices) +
 -- Tag0(nested) + expr(typ) + Tag0(ctors_len) + ctors...
 -- expr(typ) + Tag0(ctors_len) + ctors...
 fn get_inductive(stream: ByteStream) -> (Inductive, ByteStream) {
 let (bools_byte, s) = read_byte(stream);
 let bits = u8_bit_decomposition(bools_byte);
 let recr = bits[0];
 let refl = bits[1];
 let is_unsafe = bits[2];
 let is_unsafe = bits[0];
 let (lvls, s2) = get_tag0(s);
 let (params, s3) = get_tag0(s2);
 let (indices, s4) = get_tag0(s3);
 let (nested, s5) = get_tag0(s4);
 let (typ, s6) = get_expr(s5);
 let (ctors_len, s7) = get_tag0(s6);
 let (ctors, s8) = get_constructor_list(s7, ctors_len);
 (Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, store(typ), ctors), s8)
 let (typ, s5) = get_expr(s4);
 let (ctors_len, s6) = get_tag0(s5);
 let (ctors, s7) = get_constructor_list(s6, ctors_len);
 (Inductive.Mk(is_unsafe, lvls, params, indices, store(typ), ctors), s7)
 }

 -- ============================================================================
Expand Down

12 changes: 5 additions & 7 deletions
Ix/IxVM/IxonSerialize.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -387,17 +387,15 @@ def ixonSerialize := ⟦

 fn put_inductive(indc: Inductive, rest: ByteStream) -> ByteStream {
 match indc {
 Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, &typ, ctors) =>
 let bools = recr + 2 * refl + 4 * is_unsafe;
 Inductive.Mk(is_unsafe, lvls, params, indices, &typ, ctors) =>
 let ctors_len = list_length_u64(ctors);
 store(ListNode.Cons(u8_from_field_unsafe(bools),
 store(ListNode.Cons(u8_from_field_unsafe(is_unsafe),
 put_tag0(lvls,
 put_tag0(params,
 put_tag0(indices,
 put_tag0(nested,
 put_expr(typ,
 put_tag0(ctors_len,
 put_constructor_list(ctors, rest))))))))),
 put_expr(typ,
 put_tag0(ctors_len,
 put_constructor_list(ctors, rest)))))))),
 }
 }

Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Auto-enable theater mode on YouTube\n(function() {\n function tryTheater() {\n var btn = document.querySelector('button[aria-label=\"Theater mode\"], ytd-player #player button[title=\"Theater mode\"]');\n if (btn && !btn.classList.contains('activated')) {\n btn.click();\n }\n }\n \n // Try immediately\n tryTheater();\n \n // Try after navigation (SPA)\n var lastUrl = location.href;\n setInterval(function() {\n if (location.href !== lastUrl) {\n lastUrl = location.href;\n setTimeout(tryTheater, 500);\n }\n }, 1000);\n \n // Also try on player load\n var observer = new MutationObserver(tryTheater);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "YouTube Theater Mode Default");
}
} catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
Compiler fixes for auxiliary constant generation#473

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

johnchandlerburnham
merged 5 commits into

from

Jul 7, 2026
 Merged


Compiler fixes for auxiliary constant generation
#473
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


5 commits


Select commit
Hold shift + click to select a range
62eb9c6

Ixon: drop recr/refl/nested flags from Inductive


johnchandlerburnham Jul 4, 2026
2fc6dda

Compile: evaporated-aux canonicalization and byte-exact aux roundtrip


johnchandlerburnham Jul 4, 2026
fb00cf5

chore: fix clippy warnings and fmt drift


johnchandlerburnham Jul 4, 2026
d8b11c0

IxVM Aiur kernel: fix Lean.Syntax.rec (shard 53) aux-recursor gen


arthurpaulino Jul 1, 2026
2f2a86f

IxVM: port Inductive flag-drop + evaporated-aux aliasing to Aiur kernel


arthurpaulino Jul 4, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


4 changes: 4 additions & 0 deletions
.gitignore

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -7,3 +7,7 @@
# Nix
result*
.direnv/

#Ix
*.ixe
plans

1 change: 1 addition & 0 deletions
Benchmarks/Compile/CompileMutualFixtures.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
import Tests.Ix.Compile.Mutual

29 changes: 28 additions & 1 deletion
Benchmarks/Compile/lake-manifest.json

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -21,6 +21,13 @@
 "inputRev": "v4.29.0",
 "inherited": false,
 "configFile": "lakefile.toml"},
 {"type": "path",
 "scope": "",
 "name": "ix",
 "manifestFile": "lake-manifest.json",
 "inherited": false,
 "dir": "../..",
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/leanprover-community/plausible",
 "type": "git",
 "subDir": null,
Expand DownExpand Up@@ -110,6 +117,26 @@
 "manifestFile": "lake-manifest.json",
 "inputRev": null,
 "inherited": true,
 "configFile": "lakefile.lean"}],
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/argumentcomputer/Blake3.lean",
 "type": "git",
 "subDir": null,
 "scope": "",
 "rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
 "name": "Blake3",
 "manifestFile": "lake-manifest.json",
 "inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
 "inherited": true,
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/argumentcomputer/LSpec",
 "type": "git",
 "subDir": null,
 "scope": "",
 "rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
 "name": "LSpec",
 "manifestFile": "lake-manifest.json",
 "inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
 "inherited": true,
 "configFile": "lakefile.toml"}],
 "name": "Compile",
 "lakeDir": ".lake"}

7 changes: 7 additions & 0 deletions
Benchmarks/Compile/lakefile.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -17,6 +17,13 @@ name = "CompileMathlib"
[[lean_lib]]
name = "CompileFLT"

[[lean_lib]]
name = "CompileMutualFixtures"

[[require]]
name = "ix"
path = "../.."

[[require]]
name = "flt"
git = "https://github.com/ImperialCollegeLondon/FLT"
Expand Down

34 changes: 13 additions & 21 deletions
Ix/Claim.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -94,10 +94,9 @@ structure RevealRecursorRule where
inductive RevealMutConstInfo where
 | defn (kind : Option DefKind) (safety : Option DefinitionSafety)
 (lvls : Option UInt64) (typ : Option Address) (value : Option Address)
 | indc (isRecr : Option Bool) (refl : Option Bool) (isUnsafe : Option Bool)
 (lvls : Option UInt64) (params : Option UInt64)
 (indices : Option UInt64) (nested : Option UInt64)
 (typ : Option Address) (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
 | indc (isUnsafe : Option Bool) (lvls : Option UInt64) (params : Option UInt64)
 (indices : Option UInt64) (typ : Option Address)
 (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
 | recr (k : Option Bool) (isUnsafe : Option Bool) (lvls : Option UInt64)
 (params : Option UInt64) (indices : Option UInt64)
 (motives : Option UInt64) (minors : Option UInt64)
Expand DownExpand Up@@ -240,19 +239,15 @@ def put : RevealMutConstInfo → PutM Unit
 match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
 match typ with | some a => Serialize.put a | none => pure ()
 match value with | some a => Serialize.put a | none => pure ()
 | .indc isRecr refl isUnsafe lvls params indices nested typ ctors => do
 | .indc isUnsafe lvls params indices typ ctors => do
 putU8 1
 let mask := computeMask [isRecr.isSome, refl.isSome, isUnsafe.isSome,
 lvls.isSome, params.isSome, indices.isSome,
 nested.isSome, typ.isSome, ctors.isSome]
 let mask := computeMask [isUnsafe.isSome, lvls.isSome, params.isSome, 
 indices.isSome, typ.isSome, ctors.isSome]
 putTag0 ⟨mask⟩
 match isRecr with | some b => putBoolField b | none => pure ()
 match refl with | some b => putBoolField b | none => pure ()
 match isUnsafe with | some b => putBoolField b | none => pure ()
 match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
 match params with | some n => putTag0 ⟨n⟩ | none => pure ()
 match indices with | some n => putTag0 ⟨n⟩ | none => pure ()
 match nested with | some n => putTag0 ⟨n⟩ | none => pure ()
 match typ with | some a => Serialize.put a | none => pure ()
 match ctors with | some c => putCtors c | none => pure ()
 | .recr k isUnsafe lvls params indices motives minors typ rules => do
Expand DownExpand Up@@ -283,16 +278,13 @@ def get : GetM RevealMutConstInfo := do
 let value ← getOpt mask 16 Serialize.get
 return .defn kind safety lvls typ value
 | 1 => do -- Indc
 let isRecr ← getOpt mask 1 getBoolField
 let refl ← getOpt mask 2 getBoolField
 let isUnsafe ← getOpt mask 4 getBoolField
 let lvls ← getOpt mask 8 getTag0Size
 let params ← getOpt mask 16 getTag0Size
 let indices ← getOpt mask 32 getTag0Size
 let nested ← getOpt mask 64 getTag0Size
 let typ ← getOpt mask 128 Serialize.get
 let ctors ← getOpt mask 256 getCtors
 return .indc isRecr refl isUnsafe lvls params indices nested typ ctors
 let isUnsafe ← getOpt mask 1 getBoolField
 let lvls ← getOpt mask 2 getTag0Size
 let params ← getOpt mask 4 getTag0Size
 let indices ← getOpt mask 8 getTag0Size
 let typ ← getOpt mask 16 Serialize.get
 let ctors ← getOpt mask 32 getCtors
 return .indc isUnsafe lvls params indices typ ctors
 | 2 => do -- Recr
 let k ← getOpt mask 1 getBoolField
 let isUnsafe ← getOpt mask 2 getBoolField
Expand Down

3 changes: 1 addition & 2 deletions
Ix/Commit.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -208,8 +208,7 @@ def openMutConst (mc : Ixon.MutConst) : RevealMutConstInfo :=
 for j in [:i.ctors.size] do
 arr := arr.push (j.toUInt64, openConstructor i.ctors[j]!)
 return arr
 .indc (some i.recr) (some i.refl) (some i.isUnsafe)
 (some i.lvls) (some i.params) (some i.indices) (some i.nested)
 .indc (some i.isUnsafe) (some i.lvls) (some i.params) (some i.indices)
 (some (exprAddr i.typ)) (some ctors)
 | .recr r =>
 let rules := Id.run do
Expand Down

34 changes: 34 additions & 0 deletions
Ix/Common.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -328,6 +328,40 @@ private partial def collectDependenciesAux (const : Lean.ConstantInfo)
 goExpr consts acc val.value
 | .recInfo val =>
 let acc ← collectNames val.all acc
 -- The compiler processes a declaration's recursors as one block, and
 -- they cross-reference in rule RHSs (`A.rec`'s rule calls `A.rec_1`,
 -- `A.rec_2`'s calls `C.rec`), so the closure needs every sibling:
 -- `<ind>.rec` per block inductive plus the nested-aux `<all0>.rec_N`.
 let siblings := val.all.filterMap fun ind =>
 let n := Lean.mkRecName ind
 if consts.contains n then some n else none
 let auxSiblings : List Lean.Name := Id.run do
 let mut out := []
 let mut i := 1
 repeat
 match val.all.head? with
 | none => break
 | some base =>
 let n := Lean.Name.mkStr base s!"rec_{i}"
 if consts.contains n then
 out := n :: out
 i := i + 1
 else break
 return out
 let acc ← collectNames (siblings ++ auxSiblings) acc
 -- A nested-aux recursor's rules recurse via the external container's
 -- ctors; its evaporated form aliases that container's recursor
 -- (`List.rec`), which no collected expr mentions — pull it via each
 -- rule ctor's owning inductive.
 let extRecs := val.rules.filterMap fun rule =>
 match consts.find? rule.ctor with
 | some (.ctorInfo cv) =>
 if val.all.contains cv.induct then none
 else
 let n := Lean.mkRecName cv.induct
 if consts.contains n then some n else none
 | _ => none
 let acc ← collectNames extRecs acc
 let acc ← goExpr consts acc val.type
 val.rules.foldlM (init := acc) fun acc rule => goExpr consts acc rule.rhs
where
Expand Down

6 changes: 0 additions & 6 deletions
Ix/CompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -1112,13 +1112,10 @@ def compileInductive (i : InductiveVal) (ctorVals : Array ConstructorVal)
 let ctxAddrs ← getMutCtxAddrs

 let ind : Ixon.Inductive := {
 recr := i.isRec
 refl := i.isReflexive
 isUnsafe := i.isUnsafe
 lvls := i.cnst.levelParams.size.toUInt64
 params := i.numParams.toUInt64
 indices := i.numIndices.toUInt64
 nested := i.numNested.toUInt64
 typ := typeExpr
 ctors := ctors
 }
Expand DownExpand Up@@ -1194,13 +1191,10 @@ def compileInductiveData (i : Ind)
 let ctxAddrs ← getMutCtxAddrs

 let ind : Ixon.Inductive := {
 recr := i.isRec
 refl := i.isReflexive
 isUnsafe := i.isUnsafe
 lvls := i.levelParams.size.toUInt64
 params := i.numParams.toUInt64
 indices := i.numIndices.toUInt64
 nested := i.numNested.toUInt64
 typ := typeExpr
 ctors := ctors
 }
Expand Down

5 changes: 3 additions & 2 deletions
Ix/DecompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -670,8 +670,9 @@ def decompileInductive (ind : Ixon.Inductive) (cnst : Constant) (cMeta : Constan
 cnst := { name, levelParams := univParams, type := typeExpr },
 numParams := ind.params.toNat, numIndices := ind.indices.toNat,
 all := allNames, ctors := ctorNames,
 numNested := ind.nested.toNat, isRec := ind.recr,
 isUnsafe := ind.isUnsafe, isReflexive := ind.refl }
 -- temporary stub until we update the Lean compiler and decompiler semantics
 numNested := 0, isRec := false
 isUnsafe := ind.isUnsafe, isReflexive := false }
 pure (indVal, ctors)

/-! ## Projection Handling -/
Expand Down

4 changes: 2 additions & 2 deletions
Ix/IxVM/Convert.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -314,11 +314,11 @@ def convert := ⟦
 match ctx {
 ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
 match ind {
 Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, typ, _) =>
 Inductive.Mk(is_unsafe, lvls, params, indices, typ, _) =>
 let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
 KConstantInfo.Induct(
 flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
 ctor_idxs, is_rec, is_refl, is_unsafe, flatten_u64(nested), block_addr),
 ctor_idxs, is_unsafe, block_addr),
 },
 }
 }
Expand Down

10 changes: 5 additions & 5 deletions
Ix/IxVM/Ingress.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -175,7 +175,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 list_length(ctors) + 1,
 },
 MutConst.Recr(_) => 1,
Expand DownExpand Up@@ -850,7 +850,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 let num_ctors = list_length(ctors);
 let this_ctors = build_ctor_idxs(num_ctors, cur_pos, 0);
 let rest_ctors = build_rule_ctor_idxs_walk(rest,
Expand DownExpand Up@@ -998,7 +998,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 build_ctor_idxs(list_length(ctors), cur_pos, 0),
 },
 _ => store(ListNode.Nil),
Expand DownExpand Up@@ -1027,7 +1027,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 let num_ctors = list_length(ctors);
 let induct_pos = block_start + member_offset(members, member_idx);
 let ctor_idxs = build_ctor_idxs(num_ctors, induct_pos, 0);
Expand DownExpand Up@@ -1546,7 +1546,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 list_length(ctors),
 },
 _ => 0,
Expand Down

4 changes: 2 additions & 2 deletions
Ix/IxVM/Ixon.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -83,9 +83,9 @@ def ixon := ⟦
 Mk(G, U64, U64, U64, U64, &Expr)
 }

 -- Inductive: (recr, refl, is_unsafe, lvls, params, indices, nested, typ, ctors)
 -- Inductive: (is_unsafe, lvls, params, indices, typ, ctors)
 enum Inductive {
 Mk(G, G, G, U64, U64, U64, U64, &Expr, List‹Constructor›)
 Mk(G, U64, U64, U64, &Expr, List‹Constructor›)
 }

 -- InductiveProj: (idx, block_address)
Expand Down

15 changes: 6 additions & 9 deletions
Ix/IxVM/IxonDeserialize.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -479,21 +479,18 @@ def ixonDeserialize := ⟦
 }

 -- Inductive: byte(bools) + Tag0(lvls) + Tag0(params) + Tag0(indices) +
 -- Tag0(nested) + expr(typ) + Tag0(ctors_len) + ctors...
 -- expr(typ) + Tag0(ctors_len) + ctors...
 fn get_inductive(stream: ByteStream) -> (Inductive, ByteStream) {
 let (bools_byte, s) = read_byte(stream);
 let bits = u8_bit_decomposition(bools_byte);
 let recr = bits[0];
 let refl = bits[1];
 let is_unsafe = bits[2];
 let is_unsafe = bits[0];
 let (lvls, s2) = get_tag0(s);
 let (params, s3) = get_tag0(s2);
 let (indices, s4) = get_tag0(s3);
 let (nested, s5) = get_tag0(s4);
 let (typ, s6) = get_expr(s5);
 let (ctors_len, s7) = get_tag0(s6);
 let (ctors, s8) = get_constructor_list(s7, ctors_len);
 (Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, store(typ), ctors), s8)
 let (typ, s5) = get_expr(s4);
 let (ctors_len, s6) = get_tag0(s5);
 let (ctors, s7) = get_constructor_list(s6, ctors_len);
 (Inductive.Mk(is_unsafe, lvls, params, indices, store(typ), ctors), s7)
 }

 -- ============================================================================
Expand Down

12 changes: 5 additions & 7 deletions
Ix/IxVM/IxonSerialize.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -387,17 +387,15 @@ def ixonSerialize := ⟦

 fn put_inductive(indc: Inductive, rest: ByteStream) -> ByteStream {
 match indc {
 Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, &typ, ctors) =>
 let bools = recr + 2 * refl + 4 * is_unsafe;
 Inductive.Mk(is_unsafe, lvls, params, indices, &typ, ctors) =>
 let ctors_len = list_length_u64(ctors);
 store(ListNode.Cons(u8_from_field_unsafe(bools),
 store(ListNode.Cons(u8_from_field_unsafe(is_unsafe),
 put_tag0(lvls,
 put_tag0(params,
 put_tag0(indices,
 put_tag0(nested,
 put_expr(typ,
 put_tag0(ctors_len,
 put_constructor_list(ctors, rest))))))))),
 put_expr(typ,
 put_tag0(ctors_len,
 put_constructor_list(ctors, rest)))))))),
 }
 }

Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Remove or un-stick sticky/fixed headers that block content\n(function() {\n function unstick() {\n document.querySelectorAll('header, nav, [role=\"banner\"], .header, .navbar, .sticky, .fixed-top, [style*=\"position: fixed\"], [style*=\"position:sticky\"]').forEach(function(el) {\n if (el.style.position === 'fixed' || el.style.position === 'sticky' || \n getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') {\n el.style.position = 'static';\n el.style.top = 'auto';\n el.style.zIndex = 'auto';\n }\n });\n }\n \n unstick();\n \n var observer = new MutationObserver(unstick);\n observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] });\n})();", "Kill Sticky Headers");
}
} catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
Compiler fixes for auxiliary constant generation#473

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

johnchandlerburnham
merged 5 commits into

from

Jul 7, 2026
 Merged


Compiler fixes for auxiliary constant generation
#473
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


5 commits


Select commit
Hold shift + click to select a range
62eb9c6

Ixon: drop recr/refl/nested flags from Inductive


johnchandlerburnham Jul 4, 2026
2fc6dda

Compile: evaporated-aux canonicalization and byte-exact aux roundtrip


johnchandlerburnham Jul 4, 2026
fb00cf5

chore: fix clippy warnings and fmt drift


johnchandlerburnham Jul 4, 2026
d8b11c0

IxVM Aiur kernel: fix Lean.Syntax.rec (shard 53) aux-recursor gen


arthurpaulino Jul 1, 2026
2f2a86f

IxVM: port Inductive flag-drop + evaporated-aux aliasing to Aiur kernel


arthurpaulino Jul 4, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


4 changes: 4 additions & 0 deletions
.gitignore

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -7,3 +7,7 @@
# Nix
result*
.direnv/

#Ix
*.ixe
plans

1 change: 1 addition & 0 deletions
Benchmarks/Compile/CompileMutualFixtures.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
import Tests.Ix.Compile.Mutual

29 changes: 28 additions & 1 deletion
Benchmarks/Compile/lake-manifest.json

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -21,6 +21,13 @@
 "inputRev": "v4.29.0",
 "inherited": false,
 "configFile": "lakefile.toml"},
 {"type": "path",
 "scope": "",
 "name": "ix",
 "manifestFile": "lake-manifest.json",
 "inherited": false,
 "dir": "../..",
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/leanprover-community/plausible",
 "type": "git",
 "subDir": null,
Expand DownExpand Up@@ -110,6 +117,26 @@
 "manifestFile": "lake-manifest.json",
 "inputRev": null,
 "inherited": true,
 "configFile": "lakefile.lean"}],
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/argumentcomputer/Blake3.lean",
 "type": "git",
 "subDir": null,
 "scope": "",
 "rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
 "name": "Blake3",
 "manifestFile": "lake-manifest.json",
 "inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
 "inherited": true,
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/argumentcomputer/LSpec",
 "type": "git",
 "subDir": null,
 "scope": "",
 "rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
 "name": "LSpec",
 "manifestFile": "lake-manifest.json",
 "inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
 "inherited": true,
 "configFile": "lakefile.toml"}],
 "name": "Compile",
 "lakeDir": ".lake"}

7 changes: 7 additions & 0 deletions
Benchmarks/Compile/lakefile.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -17,6 +17,13 @@ name = "CompileMathlib"
[[lean_lib]]
name = "CompileFLT"

[[lean_lib]]
name = "CompileMutualFixtures"

[[require]]
name = "ix"
path = "../.."

[[require]]
name = "flt"
git = "https://github.com/ImperialCollegeLondon/FLT"
Expand Down

34 changes: 13 additions & 21 deletions
Ix/Claim.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -94,10 +94,9 @@ structure RevealRecursorRule where
inductive RevealMutConstInfo where
 | defn (kind : Option DefKind) (safety : Option DefinitionSafety)
 (lvls : Option UInt64) (typ : Option Address) (value : Option Address)
 | indc (isRecr : Option Bool) (refl : Option Bool) (isUnsafe : Option Bool)
 (lvls : Option UInt64) (params : Option UInt64)
 (indices : Option UInt64) (nested : Option UInt64)
 (typ : Option Address) (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
 | indc (isUnsafe : Option Bool) (lvls : Option UInt64) (params : Option UInt64)
 (indices : Option UInt64) (typ : Option Address)
 (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
 | recr (k : Option Bool) (isUnsafe : Option Bool) (lvls : Option UInt64)
 (params : Option UInt64) (indices : Option UInt64)
 (motives : Option UInt64) (minors : Option UInt64)
Expand DownExpand Up@@ -240,19 +239,15 @@ def put : RevealMutConstInfo → PutM Unit
 match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
 match typ with | some a => Serialize.put a | none => pure ()
 match value with | some a => Serialize.put a | none => pure ()
 | .indc isRecr refl isUnsafe lvls params indices nested typ ctors => do
 | .indc isUnsafe lvls params indices typ ctors => do
 putU8 1
 let mask := computeMask [isRecr.isSome, refl.isSome, isUnsafe.isSome,
 lvls.isSome, params.isSome, indices.isSome,
 nested.isSome, typ.isSome, ctors.isSome]
 let mask := computeMask [isUnsafe.isSome, lvls.isSome, params.isSome, 
 indices.isSome, typ.isSome, ctors.isSome]
 putTag0 ⟨mask⟩
 match isRecr with | some b => putBoolField b | none => pure ()
 match refl with | some b => putBoolField b | none => pure ()
 match isUnsafe with | some b => putBoolField b | none => pure ()
 match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
 match params with | some n => putTag0 ⟨n⟩ | none => pure ()
 match indices with | some n => putTag0 ⟨n⟩ | none => pure ()
 match nested with | some n => putTag0 ⟨n⟩ | none => pure ()
 match typ with | some a => Serialize.put a | none => pure ()
 match ctors with | some c => putCtors c | none => pure ()
 | .recr k isUnsafe lvls params indices motives minors typ rules => do
Expand DownExpand Up@@ -283,16 +278,13 @@ def get : GetM RevealMutConstInfo := do
 let value ← getOpt mask 16 Serialize.get
 return .defn kind safety lvls typ value
 | 1 => do -- Indc
 let isRecr ← getOpt mask 1 getBoolField
 let refl ← getOpt mask 2 getBoolField
 let isUnsafe ← getOpt mask 4 getBoolField
 let lvls ← getOpt mask 8 getTag0Size
 let params ← getOpt mask 16 getTag0Size
 let indices ← getOpt mask 32 getTag0Size
 let nested ← getOpt mask 64 getTag0Size
 let typ ← getOpt mask 128 Serialize.get
 let ctors ← getOpt mask 256 getCtors
 return .indc isRecr refl isUnsafe lvls params indices nested typ ctors
 let isUnsafe ← getOpt mask 1 getBoolField
 let lvls ← getOpt mask 2 getTag0Size
 let params ← getOpt mask 4 getTag0Size
 let indices ← getOpt mask 8 getTag0Size
 let typ ← getOpt mask 16 Serialize.get
 let ctors ← getOpt mask 32 getCtors
 return .indc isUnsafe lvls params indices typ ctors
 | 2 => do -- Recr
 let k ← getOpt mask 1 getBoolField
 let isUnsafe ← getOpt mask 2 getBoolField
Expand Down

3 changes: 1 addition & 2 deletions
Ix/Commit.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -208,8 +208,7 @@ def openMutConst (mc : Ixon.MutConst) : RevealMutConstInfo :=
 for j in [:i.ctors.size] do
 arr := arr.push (j.toUInt64, openConstructor i.ctors[j]!)
 return arr
 .indc (some i.recr) (some i.refl) (some i.isUnsafe)
 (some i.lvls) (some i.params) (some i.indices) (some i.nested)
 .indc (some i.isUnsafe) (some i.lvls) (some i.params) (some i.indices)
 (some (exprAddr i.typ)) (some ctors)
 | .recr r =>
 let rules := Id.run do
Expand Down

34 changes: 34 additions & 0 deletions
Ix/Common.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -328,6 +328,40 @@ private partial def collectDependenciesAux (const : Lean.ConstantInfo)
 goExpr consts acc val.value
 | .recInfo val =>
 let acc ← collectNames val.all acc
 -- The compiler processes a declaration's recursors as one block, and
 -- they cross-reference in rule RHSs (`A.rec`'s rule calls `A.rec_1`,
 -- `A.rec_2`'s calls `C.rec`), so the closure needs every sibling:
 -- `<ind>.rec` per block inductive plus the nested-aux `<all0>.rec_N`.
 let siblings := val.all.filterMap fun ind =>
 let n := Lean.mkRecName ind
 if consts.contains n then some n else none
 let auxSiblings : List Lean.Name := Id.run do
 let mut out := []
 let mut i := 1
 repeat
 match val.all.head? with
 | none => break
 | some base =>
 let n := Lean.Name.mkStr base s!"rec_{i}"
 if consts.contains n then
 out := n :: out
 i := i + 1
 else break
 return out
 let acc ← collectNames (siblings ++ auxSiblings) acc
 -- A nested-aux recursor's rules recurse via the external container's
 -- ctors; its evaporated form aliases that container's recursor
 -- (`List.rec`), which no collected expr mentions — pull it via each
 -- rule ctor's owning inductive.
 let extRecs := val.rules.filterMap fun rule =>
 match consts.find? rule.ctor with
 | some (.ctorInfo cv) =>
 if val.all.contains cv.induct then none
 else
 let n := Lean.mkRecName cv.induct
 if consts.contains n then some n else none
 | _ => none
 let acc ← collectNames extRecs acc
 let acc ← goExpr consts acc val.type
 val.rules.foldlM (init := acc) fun acc rule => goExpr consts acc rule.rhs
where
Expand Down

6 changes: 0 additions & 6 deletions
Ix/CompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -1112,13 +1112,10 @@ def compileInductive (i : InductiveVal) (ctorVals : Array ConstructorVal)
 let ctxAddrs ← getMutCtxAddrs

 let ind : Ixon.Inductive := {
 recr := i.isRec
 refl := i.isReflexive
 isUnsafe := i.isUnsafe
 lvls := i.cnst.levelParams.size.toUInt64
 params := i.numParams.toUInt64
 indices := i.numIndices.toUInt64
 nested := i.numNested.toUInt64
 typ := typeExpr
 ctors := ctors
 }
Expand DownExpand Up@@ -1194,13 +1191,10 @@ def compileInductiveData (i : Ind)
 let ctxAddrs ← getMutCtxAddrs

 let ind : Ixon.Inductive := {
 recr := i.isRec
 refl := i.isReflexive
 isUnsafe := i.isUnsafe
 lvls := i.levelParams.size.toUInt64
 params := i.numParams.toUInt64
 indices := i.numIndices.toUInt64
 nested := i.numNested.toUInt64
 typ := typeExpr
 ctors := ctors
 }
Expand Down

5 changes: 3 additions & 2 deletions
Ix/DecompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -670,8 +670,9 @@ def decompileInductive (ind : Ixon.Inductive) (cnst : Constant) (cMeta : Constan
 cnst := { name, levelParams := univParams, type := typeExpr },
 numParams := ind.params.toNat, numIndices := ind.indices.toNat,
 all := allNames, ctors := ctorNames,
 numNested := ind.nested.toNat, isRec := ind.recr,
 isUnsafe := ind.isUnsafe, isReflexive := ind.refl }
 -- temporary stub until we update the Lean compiler and decompiler semantics
 numNested := 0, isRec := false
 isUnsafe := ind.isUnsafe, isReflexive := false }
 pure (indVal, ctors)

/-! ## Projection Handling -/
Expand Down

4 changes: 2 additions & 2 deletions
Ix/IxVM/Convert.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -314,11 +314,11 @@ def convert := ⟦
 match ctx {
 ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
 match ind {
 Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, typ, _) =>
 Inductive.Mk(is_unsafe, lvls, params, indices, typ, _) =>
 let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
 KConstantInfo.Induct(
 flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
 ctor_idxs, is_rec, is_refl, is_unsafe, flatten_u64(nested), block_addr),
 ctor_idxs, is_unsafe, block_addr),
 },
 }
 }
Expand Down

10 changes: 5 additions & 5 deletions
Ix/IxVM/Ingress.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -175,7 +175,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 list_length(ctors) + 1,
 },
 MutConst.Recr(_) => 1,
Expand DownExpand Up@@ -850,7 +850,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 let num_ctors = list_length(ctors);
 let this_ctors = build_ctor_idxs(num_ctors, cur_pos, 0);
 let rest_ctors = build_rule_ctor_idxs_walk(rest,
Expand DownExpand Up@@ -998,7 +998,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 build_ctor_idxs(list_length(ctors), cur_pos, 0),
 },
 _ => store(ListNode.Nil),
Expand DownExpand Up@@ -1027,7 +1027,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 let num_ctors = list_length(ctors);
 let induct_pos = block_start + member_offset(members, member_idx);
 let ctor_idxs = build_ctor_idxs(num_ctors, induct_pos, 0);
Expand DownExpand Up@@ -1546,7 +1546,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 list_length(ctors),
 },
 _ => 0,
Expand Down

4 changes: 2 additions & 2 deletions
Ix/IxVM/Ixon.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -83,9 +83,9 @@ def ixon := ⟦
 Mk(G, U64, U64, U64, U64, &Expr)
 }

 -- Inductive: (recr, refl, is_unsafe, lvls, params, indices, nested, typ, ctors)
 -- Inductive: (is_unsafe, lvls, params, indices, typ, ctors)
 enum Inductive {
 Mk(G, G, G, U64, U64, U64, U64, &Expr, List‹Constructor›)
 Mk(G, U64, U64, U64, &Expr, List‹Constructor›)
 }

 -- InductiveProj: (idx, block_address)
Expand Down

15 changes: 6 additions & 9 deletions
Ix/IxVM/IxonDeserialize.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -479,21 +479,18 @@ def ixonDeserialize := ⟦
 }

 -- Inductive: byte(bools) + Tag0(lvls) + Tag0(params) + Tag0(indices) +
 -- Tag0(nested) + expr(typ) + Tag0(ctors_len) + ctors...
 -- expr(typ) + Tag0(ctors_len) + ctors...
 fn get_inductive(stream: ByteStream) -> (Inductive, ByteStream) {
 let (bools_byte, s) = read_byte(stream);
 let bits = u8_bit_decomposition(bools_byte);
 let recr = bits[0];
 let refl = bits[1];
 let is_unsafe = bits[2];
 let is_unsafe = bits[0];
 let (lvls, s2) = get_tag0(s);
 let (params, s3) = get_tag0(s2);
 let (indices, s4) = get_tag0(s3);
 let (nested, s5) = get_tag0(s4);
 let (typ, s6) = get_expr(s5);
 let (ctors_len, s7) = get_tag0(s6);
 let (ctors, s8) = get_constructor_list(s7, ctors_len);
 (Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, store(typ), ctors), s8)
 let (typ, s5) = get_expr(s4);
 let (ctors_len, s6) = get_tag0(s5);
 let (ctors, s7) = get_constructor_list(s6, ctors_len);
 (Inductive.Mk(is_unsafe, lvls, params, indices, store(typ), ctors), s7)
 }

 -- ============================================================================
Expand Down

12 changes: 5 additions & 7 deletions
Ix/IxVM/IxonSerialize.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -387,17 +387,15 @@ def ixonSerialize := ⟦

 fn put_inductive(indc: Inductive, rest: ByteStream) -> ByteStream {
 match indc {
 Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, &typ, ctors) =>
 let bools = recr + 2 * refl + 4 * is_unsafe;
 Inductive.Mk(is_unsafe, lvls, params, indices, &typ, ctors) =>
 let ctors_len = list_length_u64(ctors);
 store(ListNode.Cons(u8_from_field_unsafe(bools),
 store(ListNode.Cons(u8_from_field_unsafe(is_unsafe),
 put_tag0(lvls,
 put_tag0(params,
 put_tag0(indices,
 put_tag0(nested,
 put_expr(typ,
 put_tag0(ctors_len,
 put_constructor_list(ctors, rest))))))))),
 put_expr(typ,
 put_tag0(ctors_len,
 put_constructor_list(ctors, rest)))))))),
 }
 }

Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Universal Dark Mode - works on any site\n(function() {\n var enabled = true;\n \n function applyDarkMode() {\n if (!enabled) return;\n \n // Create style element if it doesn't exist\n var style = document.getElementById('universal-dark-mode-style');\n if (!style) {\n style = document.createElement('style');\n style.id = 'universal-dark-mode-style';\n document.head.appendChild(style);\n }\n \n // Dark mode CSS - inverts colors but preserves images/video\n style.textContent = '\n /* Invert everything except media */\n html {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #1a1a2e !important;\n }\n \n /* Restore images, videos, iframes, canvas */\n img, video, iframe, canvas, svg, picture, [style*=\"background-image\"] {\n filter: invert(1) hue-rotate(180deg) !important;\n }\n \n /* Preserve specific elements that should not be inverted */\n .no-dark-mode, .no-dark-mode *,\n [data-theme=\"light\"], [data-theme=\"light\"],\n .ace_editor, .ace_editor *,\n .CodeMirror, .CodeMirror *,\n .monaco-editor, .monaco-editor *,\n .markdown-body pre, .markdown-body pre *,\n .highlight, .highlight *,\n pre code, pre code * {\n filter: none !important;\n }\n \n /* Fix common UI elements */\n .modal, .popup, .dropdown-menu, .tooltip, .popover {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #2d2d44 !important;\n border-color: #444 !important;\n }\n \n /* Scrollbars */\n ::-webkit-scrollbar { background: #1a1a2e !important; }\n ::-webkit-scrollbar-thumb { background: #444 !important; }\n ::-webkit-scrollbar-thumb:hover { background: #555 !important; }\n \n /* Selection */\n ::selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ';\n }\n \n function removeDarkMode() {\n var style = document.getElementById('universal-dark-mode-style');\n if (style) style.remove();\n }\n \n // Toggle with Alt+Shift+D\n document.addEventListener('keydown', function(e) {\n if (e.altKey && e.shiftKey && e.key === 'D') {\n e.preventDefault();\n enabled = !enabled;\n if (enabled) {\n applyDarkMode();\n console.log('[Universal Dark Mode] Enabled');\n } else {\n removeDarkMode();\n console.log('[Universal Dark Mode] Disabled');\n }\n }\n });\n \n // Apply on load\n applyDarkMode();\n \n // Re-apply on dynamic content\n var observer = new MutationObserver(function(mutations) {\n if (enabled && !document.getElementById('universal-dark-mode-style')) {\n applyDarkMode();\n }\n });\n observer.observe(document.head, { childList: true });\n \n console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle');\n})();", "Universal Dark Mode");
}
} catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); }
})();
})();

Skip to content
Compiler fixes for auxiliary constant generation#473

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

johnchandlerburnham
merged 5 commits into

from

Jul 7, 2026
 Merged


Compiler fixes for auxiliary constant generation
#473
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


5 commits


Select commit
Hold shift + click to select a range
62eb9c6

Ixon: drop recr/refl/nested flags from Inductive


johnchandlerburnham Jul 4, 2026
2fc6dda

Compile: evaporated-aux canonicalization and byte-exact aux roundtrip


johnchandlerburnham Jul 4, 2026
fb00cf5

chore: fix clippy warnings and fmt drift


johnchandlerburnham Jul 4, 2026
d8b11c0

IxVM Aiur kernel: fix Lean.Syntax.rec (shard 53) aux-recursor gen


arthurpaulino Jul 1, 2026
2f2a86f

IxVM: port Inductive flag-drop + evaporated-aux aliasing to Aiur kernel


arthurpaulino Jul 4, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


4 changes: 4 additions & 0 deletions
.gitignore

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -7,3 +7,7 @@
# Nix
result*
.direnv/

#Ix
*.ixe
plans

1 change: 1 addition & 0 deletions
Benchmarks/Compile/CompileMutualFixtures.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
import Tests.Ix.Compile.Mutual

29 changes: 28 additions & 1 deletion
Benchmarks/Compile/lake-manifest.json

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -21,6 +21,13 @@
 "inputRev": "v4.29.0",
 "inherited": false,
 "configFile": "lakefile.toml"},
 {"type": "path",
 "scope": "",
 "name": "ix",
 "manifestFile": "lake-manifest.json",
 "inherited": false,
 "dir": "../..",
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/leanprover-community/plausible",
 "type": "git",
 "subDir": null,
Expand DownExpand Up@@ -110,6 +117,26 @@
 "manifestFile": "lake-manifest.json",
 "inputRev": null,
 "inherited": true,
 "configFile": "lakefile.lean"}],
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/argumentcomputer/Blake3.lean",
 "type": "git",
 "subDir": null,
 "scope": "",
 "rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
 "name": "Blake3",
 "manifestFile": "lake-manifest.json",
 "inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
 "inherited": true,
 "configFile": "lakefile.lean"},
 {"url": "https://github.com/argumentcomputer/LSpec",
 "type": "git",
 "subDir": null,
 "scope": "",
 "rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
 "name": "LSpec",
 "manifestFile": "lake-manifest.json",
 "inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
 "inherited": true,
 "configFile": "lakefile.toml"}],
 "name": "Compile",
 "lakeDir": ".lake"}

7 changes: 7 additions & 0 deletions
Benchmarks/Compile/lakefile.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -17,6 +17,13 @@ name = "CompileMathlib"
[[lean_lib]]
name = "CompileFLT"

[[lean_lib]]
name = "CompileMutualFixtures"

[[require]]
name = "ix"
path = "../.."

[[require]]
name = "flt"
git = "https://github.com/ImperialCollegeLondon/FLT"
Expand Down

34 changes: 13 additions & 21 deletions
Ix/Claim.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -94,10 +94,9 @@ structure RevealRecursorRule where
inductive RevealMutConstInfo where
 | defn (kind : Option DefKind) (safety : Option DefinitionSafety)
 (lvls : Option UInt64) (typ : Option Address) (value : Option Address)
 | indc (isRecr : Option Bool) (refl : Option Bool) (isUnsafe : Option Bool)
 (lvls : Option UInt64) (params : Option UInt64)
 (indices : Option UInt64) (nested : Option UInt64)
 (typ : Option Address) (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
 | indc (isUnsafe : Option Bool) (lvls : Option UInt64) (params : Option UInt64)
 (indices : Option UInt64) (typ : Option Address)
 (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
 | recr (k : Option Bool) (isUnsafe : Option Bool) (lvls : Option UInt64)
 (params : Option UInt64) (indices : Option UInt64)
 (motives : Option UInt64) (minors : Option UInt64)
Expand DownExpand Up@@ -240,19 +239,15 @@ def put : RevealMutConstInfo → PutM Unit
 match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
 match typ with | some a => Serialize.put a | none => pure ()
 match value with | some a => Serialize.put a | none => pure ()
 | .indc isRecr refl isUnsafe lvls params indices nested typ ctors => do
 | .indc isUnsafe lvls params indices typ ctors => do
 putU8 1
 let mask := computeMask [isRecr.isSome, refl.isSome, isUnsafe.isSome,
 lvls.isSome, params.isSome, indices.isSome,
 nested.isSome, typ.isSome, ctors.isSome]
 let mask := computeMask [isUnsafe.isSome, lvls.isSome, params.isSome, 
 indices.isSome, typ.isSome, ctors.isSome]
 putTag0 ⟨mask⟩
 match isRecr with | some b => putBoolField b | none => pure ()
 match refl with | some b => putBoolField b | none => pure ()
 match isUnsafe with | some b => putBoolField b | none => pure ()
 match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
 match params with | some n => putTag0 ⟨n⟩ | none => pure ()
 match indices with | some n => putTag0 ⟨n⟩ | none => pure ()
 match nested with | some n => putTag0 ⟨n⟩ | none => pure ()
 match typ with | some a => Serialize.put a | none => pure ()
 match ctors with | some c => putCtors c | none => pure ()
 | .recr k isUnsafe lvls params indices motives minors typ rules => do
Expand DownExpand Up@@ -283,16 +278,13 @@ def get : GetM RevealMutConstInfo := do
 let value ← getOpt mask 16 Serialize.get
 return .defn kind safety lvls typ value
 | 1 => do -- Indc
 let isRecr ← getOpt mask 1 getBoolField
 let refl ← getOpt mask 2 getBoolField
 let isUnsafe ← getOpt mask 4 getBoolField
 let lvls ← getOpt mask 8 getTag0Size
 let params ← getOpt mask 16 getTag0Size
 let indices ← getOpt mask 32 getTag0Size
 let nested ← getOpt mask 64 getTag0Size
 let typ ← getOpt mask 128 Serialize.get
 let ctors ← getOpt mask 256 getCtors
 return .indc isRecr refl isUnsafe lvls params indices nested typ ctors
 let isUnsafe ← getOpt mask 1 getBoolField
 let lvls ← getOpt mask 2 getTag0Size
 let params ← getOpt mask 4 getTag0Size
 let indices ← getOpt mask 8 getTag0Size
 let typ ← getOpt mask 16 Serialize.get
 let ctors ← getOpt mask 32 getCtors
 return .indc isUnsafe lvls params indices typ ctors
 | 2 => do -- Recr
 let k ← getOpt mask 1 getBoolField
 let isUnsafe ← getOpt mask 2 getBoolField
Expand Down

3 changes: 1 addition & 2 deletions
Ix/Commit.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -208,8 +208,7 @@ def openMutConst (mc : Ixon.MutConst) : RevealMutConstInfo :=
 for j in [:i.ctors.size] do
 arr := arr.push (j.toUInt64, openConstructor i.ctors[j]!)
 return arr
 .indc (some i.recr) (some i.refl) (some i.isUnsafe)
 (some i.lvls) (some i.params) (some i.indices) (some i.nested)
 .indc (some i.isUnsafe) (some i.lvls) (some i.params) (some i.indices)
 (some (exprAddr i.typ)) (some ctors)
 | .recr r =>
 let rules := Id.run do
Expand Down

34 changes: 34 additions & 0 deletions
Ix/Common.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -328,6 +328,40 @@ private partial def collectDependenciesAux (const : Lean.ConstantInfo)
 goExpr consts acc val.value
 | .recInfo val =>
 let acc ← collectNames val.all acc
 -- The compiler processes a declaration's recursors as one block, and
 -- they cross-reference in rule RHSs (`A.rec`'s rule calls `A.rec_1`,
 -- `A.rec_2`'s calls `C.rec`), so the closure needs every sibling:
 -- `<ind>.rec` per block inductive plus the nested-aux `<all0>.rec_N`.
 let siblings := val.all.filterMap fun ind =>
 let n := Lean.mkRecName ind
 if consts.contains n then some n else none
 let auxSiblings : List Lean.Name := Id.run do
 let mut out := []
 let mut i := 1
 repeat
 match val.all.head? with
 | none => break
 | some base =>
 let n := Lean.Name.mkStr base s!"rec_{i}"
 if consts.contains n then
 out := n :: out
 i := i + 1
 else break
 return out
 let acc ← collectNames (siblings ++ auxSiblings) acc
 -- A nested-aux recursor's rules recurse via the external container's
 -- ctors; its evaporated form aliases that container's recursor
 -- (`List.rec`), which no collected expr mentions — pull it via each
 -- rule ctor's owning inductive.
 let extRecs := val.rules.filterMap fun rule =>
 match consts.find? rule.ctor with
 | some (.ctorInfo cv) =>
 if val.all.contains cv.induct then none
 else
 let n := Lean.mkRecName cv.induct
 if consts.contains n then some n else none
 | _ => none
 let acc ← collectNames extRecs acc
 let acc ← goExpr consts acc val.type
 val.rules.foldlM (init := acc) fun acc rule => goExpr consts acc rule.rhs
where
Expand Down

6 changes: 0 additions & 6 deletions
Ix/CompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -1112,13 +1112,10 @@ def compileInductive (i : InductiveVal) (ctorVals : Array ConstructorVal)
 let ctxAddrs ← getMutCtxAddrs

 let ind : Ixon.Inductive := {
 recr := i.isRec
 refl := i.isReflexive
 isUnsafe := i.isUnsafe
 lvls := i.cnst.levelParams.size.toUInt64
 params := i.numParams.toUInt64
 indices := i.numIndices.toUInt64
 nested := i.numNested.toUInt64
 typ := typeExpr
 ctors := ctors
 }
Expand DownExpand Up@@ -1194,13 +1191,10 @@ def compileInductiveData (i : Ind)
 let ctxAddrs ← getMutCtxAddrs

 let ind : Ixon.Inductive := {
 recr := i.isRec
 refl := i.isReflexive
 isUnsafe := i.isUnsafe
 lvls := i.levelParams.size.toUInt64
 params := i.numParams.toUInt64
 indices := i.numIndices.toUInt64
 nested := i.numNested.toUInt64
 typ := typeExpr
 ctors := ctors
 }
Expand Down

5 changes: 3 additions & 2 deletions
Ix/DecompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -670,8 +670,9 @@ def decompileInductive (ind : Ixon.Inductive) (cnst : Constant) (cMeta : Constan
 cnst := { name, levelParams := univParams, type := typeExpr },
 numParams := ind.params.toNat, numIndices := ind.indices.toNat,
 all := allNames, ctors := ctorNames,
 numNested := ind.nested.toNat, isRec := ind.recr,
 isUnsafe := ind.isUnsafe, isReflexive := ind.refl }
 -- temporary stub until we update the Lean compiler and decompiler semantics
 numNested := 0, isRec := false
 isUnsafe := ind.isUnsafe, isReflexive := false }
 pure (indVal, ctors)

/-! ## Projection Handling -/
Expand Down

4 changes: 2 additions & 2 deletions
Ix/IxVM/Convert.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -314,11 +314,11 @@ def convert := ⟦
 match ctx {
 ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
 match ind {
 Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, typ, _) =>
 Inductive.Mk(is_unsafe, lvls, params, indices, typ, _) =>
 let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
 KConstantInfo.Induct(
 flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
 ctor_idxs, is_rec, is_refl, is_unsafe, flatten_u64(nested), block_addr),
 ctor_idxs, is_unsafe, block_addr),
 },
 }
 }
Expand Down

10 changes: 5 additions & 5 deletions
Ix/IxVM/Ingress.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -175,7 +175,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 list_length(ctors) + 1,
 },
 MutConst.Recr(_) => 1,
Expand DownExpand Up@@ -850,7 +850,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 let num_ctors = list_length(ctors);
 let this_ctors = build_ctor_idxs(num_ctors, cur_pos, 0);
 let rest_ctors = build_rule_ctor_idxs_walk(rest,
Expand DownExpand Up@@ -998,7 +998,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 build_ctor_idxs(list_length(ctors), cur_pos, 0),
 },
 _ => store(ListNode.Nil),
Expand DownExpand Up@@ -1027,7 +1027,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 let num_ctors = list_length(ctors);
 let induct_pos = block_start + member_offset(members, member_idx);
 let ctor_idxs = build_ctor_idxs(num_ctors, induct_pos, 0);
Expand DownExpand Up@@ -1546,7 +1546,7 @@ def ingress := ⟦
 match mc {
 MutConst.Indc(ind) =>
 match ind {
 Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
 Inductive.Mk(_, _, _, _, _, ctors) =>
 list_length(ctors),
 },
 _ => 0,
Expand Down

4 changes: 2 additions & 2 deletions
Ix/IxVM/Ixon.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -83,9 +83,9 @@ def ixon := ⟦
 Mk(G, U64, U64, U64, U64, &Expr)
 }

 -- Inductive: (recr, refl, is_unsafe, lvls, params, indices, nested, typ, ctors)
 -- Inductive: (is_unsafe, lvls, params, indices, typ, ctors)
 enum Inductive {
 Mk(G, G, G, U64, U64, U64, U64, &Expr, List‹Constructor›)
 Mk(G, U64, U64, U64, &Expr, List‹Constructor›)
 }

 -- InductiveProj: (idx, block_address)
Expand Down

15 changes: 6 additions & 9 deletions
Ix/IxVM/IxonDeserialize.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -479,21 +479,18 @@ def ixonDeserialize := ⟦
 }

 -- Inductive: byte(bools) + Tag0(lvls) + Tag0(params) + Tag0(indices) +
 -- Tag0(nested) + expr(typ) + Tag0(ctors_len) + ctors...
 -- expr(typ) + Tag0(ctors_len) + ctors...
 fn get_inductive(stream: ByteStream) -> (Inductive, ByteStream) {
 let (bools_byte, s) = read_byte(stream);
 let bits = u8_bit_decomposition(bools_byte);
 let recr = bits[0];
 let refl = bits[1];
 let is_unsafe = bits[2];
 let is_unsafe = bits[0];
 let (lvls, s2) = get_tag0(s);
 let (params, s3) = get_tag0(s2);
 let (indices, s4) = get_tag0(s3);
 let (nested, s5) = get_tag0(s4);
 let (typ, s6) = get_expr(s5);
 let (ctors_len, s7) = get_tag0(s6);
 let (ctors, s8) = get_constructor_list(s7, ctors_len);
 (Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, store(typ), ctors), s8)
 let (typ, s5) = get_expr(s4);
 let (ctors_len, s6) = get_tag0(s5);
 let (ctors, s7) = get_constructor_list(s6, ctors_len);
 (Inductive.Mk(is_unsafe, lvls, params, indices, store(typ), ctors), s7)
 }

 -- ============================================================================
Expand Down

12 changes: 5 additions & 7 deletions
Ix/IxVM/IxonSerialize.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -387,17 +387,15 @@ def ixonSerialize := ⟦

 fn put_inductive(indc: Inductive, rest: ByteStream) -> ByteStream {
 match indc {
 Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, &typ, ctors) =>
 let bools = recr + 2 * refl + 4 * is_unsafe;
 Inductive.Mk(is_unsafe, lvls, params, indices, &typ, ctors) =>
 let ctors_len = list_length_u64(ctors);
 store(ListNode.Cons(u8_from_field_unsafe(bools),
 store(ListNode.Cons(u8_from_field_unsafe(is_unsafe),
 put_tag0(lvls,
 put_tag0(params,
 put_tag0(indices,
 put_tag0(nested,
 put_expr(typ,
 put_tag0(ctors_len,
 put_constructor_list(ctors, rest))))))))),
 put_expr(typ,
 put_tag0(ctors_len,
 put_constructor_list(ctors, rest)))))))),
 }
 }

Expand Down
Loading