chore: update stage0
This commit is contained in:
parent
9f76cb9aa5
commit
3a588e7547
8 changed files with 9673 additions and 5777 deletions
|
|
@ -8,7 +8,7 @@ options get_default_options() {
|
|||
// switch to `true` for ABI-breaking changes affecting meta code
|
||||
opts = opts.update({"interpreter", "prefer_native"}, false);
|
||||
// switch to `true` for changing built-in parsers used in quotations
|
||||
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
|
||||
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
|
||||
// toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
|
||||
// with custom precheck hooks were affected
|
||||
opts = opts.update({"quotPrecheck"}, true);
|
||||
|
|
|
|||
1218
stage0/stdlib/Lean/Elab/BuiltinCommand.c
generated
1218
stage0/stdlib/Lean/Elab/BuiltinCommand.c
generated
File diff suppressed because it is too large
Load diff
955
stage0/stdlib/Lean/Elab/Command.c
generated
955
stage0/stdlib/Lean/Elab/Command.c
generated
File diff suppressed because it is too large
Load diff
39
stage0/stdlib/Lean/Elab/Inductive.c
generated
39
stage0/stdlib/Lean/Elab/Inductive.c
generated
|
|
@ -33991,7 +33991,7 @@ return x_1;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17; lean_object* x_18; uint8_t x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; lean_object* x_24;
|
||||
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19; uint8_t x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; lean_object* x_24; lean_object* x_25;
|
||||
x_10 = lean_ctor_get(x_1, 0);
|
||||
x_11 = lean_ctor_get(x_1, 1);
|
||||
x_12 = lean_ctor_get(x_1, 2);
|
||||
|
|
@ -33999,7 +33999,9 @@ x_13 = lean_ctor_get(x_1, 3);
|
|||
x_14 = lean_ctor_get(x_1, 4);
|
||||
x_15 = lean_ctor_get(x_1, 5);
|
||||
x_16 = lean_ctor_get(x_1, 6);
|
||||
x_17 = lean_ctor_get_uint8(x_1, sizeof(void*)*7);
|
||||
x_17 = lean_ctor_get(x_1, 7);
|
||||
x_18 = lean_ctor_get_uint8(x_1, sizeof(void*)*8);
|
||||
lean_inc(x_17);
|
||||
lean_inc(x_16);
|
||||
lean_inc(x_15);
|
||||
lean_inc(x_14);
|
||||
|
|
@ -34008,22 +34010,23 @@ lean_inc(x_12);
|
|||
lean_inc(x_11);
|
||||
lean_inc(x_10);
|
||||
lean_dec(x_1);
|
||||
x_18 = l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_applyComputedFields___lambda__1___closed__2;
|
||||
x_19 = 0;
|
||||
x_20 = l_Lean_KVMap_setBool(x_11, x_18, x_19);
|
||||
x_21 = l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_applyComputedFields___lambda__1___closed__4;
|
||||
x_22 = 1;
|
||||
x_23 = l_Lean_KVMap_setBool(x_20, x_21, x_22);
|
||||
x_24 = lean_alloc_ctor(0, 7, 1);
|
||||
lean_ctor_set(x_24, 0, x_10);
|
||||
lean_ctor_set(x_24, 1, x_23);
|
||||
lean_ctor_set(x_24, 2, x_12);
|
||||
lean_ctor_set(x_24, 3, x_13);
|
||||
lean_ctor_set(x_24, 4, x_14);
|
||||
lean_ctor_set(x_24, 5, x_15);
|
||||
lean_ctor_set(x_24, 6, x_16);
|
||||
lean_ctor_set_uint8(x_24, sizeof(void*)*7, x_17);
|
||||
return x_24;
|
||||
x_19 = l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_applyComputedFields___lambda__1___closed__2;
|
||||
x_20 = 0;
|
||||
x_21 = l_Lean_KVMap_setBool(x_11, x_19, x_20);
|
||||
x_22 = l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_applyComputedFields___lambda__1___closed__4;
|
||||
x_23 = 1;
|
||||
x_24 = l_Lean_KVMap_setBool(x_21, x_22, x_23);
|
||||
x_25 = lean_alloc_ctor(0, 8, 1);
|
||||
lean_ctor_set(x_25, 0, x_10);
|
||||
lean_ctor_set(x_25, 1, x_24);
|
||||
lean_ctor_set(x_25, 2, x_12);
|
||||
lean_ctor_set(x_25, 3, x_13);
|
||||
lean_ctor_set(x_25, 4, x_14);
|
||||
lean_ctor_set(x_25, 5, x_15);
|
||||
lean_ctor_set(x_25, 6, x_16);
|
||||
lean_ctor_set(x_25, 7, x_17);
|
||||
lean_ctor_set_uint8(x_25, sizeof(void*)*8, x_18);
|
||||
return x_25;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
12550
stage0/stdlib/Lean/Elab/MutualDef.c
generated
12550
stage0/stdlib/Lean/Elab/MutualDef.c
generated
File diff suppressed because it is too large
Load diff
7
stage0/stdlib/Lean/Language/Lean.c
generated
7
stage0/stdlib/Lean/Language/Lean.c
generated
|
|
@ -4346,15 +4346,16 @@ x_2 = l_Lean_Language_Lean_initFn____x40_Lean_Language_Lean___hyg_444____closed_
|
|||
x_3 = lean_box(0);
|
||||
x_4 = l_Lean_Language_Lean_process_parseCmd___lambda__2___closed__9;
|
||||
x_5 = 0;
|
||||
x_6 = lean_alloc_ctor(0, 7, 1);
|
||||
x_6 = lean_alloc_ctor(0, 8, 1);
|
||||
lean_ctor_set(x_6, 0, x_2);
|
||||
lean_ctor_set(x_6, 1, x_1);
|
||||
lean_ctor_set(x_6, 2, x_3);
|
||||
lean_ctor_set(x_6, 3, x_1);
|
||||
lean_ctor_set(x_6, 4, x_1);
|
||||
lean_ctor_set(x_6, 5, x_4);
|
||||
lean_ctor_set(x_6, 6, x_4);
|
||||
lean_ctor_set_uint8(x_6, sizeof(void*)*7, x_5);
|
||||
lean_ctor_set(x_6, 6, x_1);
|
||||
lean_ctor_set(x_6, 7, x_4);
|
||||
lean_ctor_set_uint8(x_6, sizeof(void*)*8, x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
27
stage0/stdlib/Lean/Linter/MissingDocs.c
generated
27
stage0/stdlib/Lean/Linter/MissingDocs.c
generated
|
|
@ -8328,14 +8328,16 @@ return x_2;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12;
|
||||
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; lean_object* x_13;
|
||||
x_5 = lean_ctor_get(x_2, 0);
|
||||
x_6 = lean_ctor_get(x_2, 2);
|
||||
x_7 = lean_ctor_get(x_2, 3);
|
||||
x_8 = lean_ctor_get(x_2, 4);
|
||||
x_9 = lean_ctor_get(x_2, 5);
|
||||
x_10 = lean_ctor_get(x_2, 6);
|
||||
x_11 = lean_ctor_get_uint8(x_2, sizeof(void*)*7);
|
||||
x_11 = lean_ctor_get(x_2, 7);
|
||||
x_12 = lean_ctor_get_uint8(x_2, sizeof(void*)*8);
|
||||
lean_inc(x_11);
|
||||
lean_inc(x_10);
|
||||
lean_inc(x_9);
|
||||
lean_inc(x_8);
|
||||
|
|
@ -8343,16 +8345,17 @@ lean_inc(x_7);
|
|||
lean_inc(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_dec(x_2);
|
||||
x_12 = lean_alloc_ctor(0, 7, 1);
|
||||
lean_ctor_set(x_12, 0, x_5);
|
||||
lean_ctor_set(x_12, 1, x_1);
|
||||
lean_ctor_set(x_12, 2, x_6);
|
||||
lean_ctor_set(x_12, 3, x_7);
|
||||
lean_ctor_set(x_12, 4, x_8);
|
||||
lean_ctor_set(x_12, 5, x_9);
|
||||
lean_ctor_set(x_12, 6, x_10);
|
||||
lean_ctor_set_uint8(x_12, sizeof(void*)*7, x_11);
|
||||
return x_12;
|
||||
x_13 = lean_alloc_ctor(0, 8, 1);
|
||||
lean_ctor_set(x_13, 0, x_5);
|
||||
lean_ctor_set(x_13, 1, x_1);
|
||||
lean_ctor_set(x_13, 2, x_6);
|
||||
lean_ctor_set(x_13, 3, x_7);
|
||||
lean_ctor_set(x_13, 4, x_8);
|
||||
lean_ctor_set(x_13, 5, x_9);
|
||||
lean_ctor_set(x_13, 6, x_10);
|
||||
lean_ctor_set(x_13, 7, x_11);
|
||||
lean_ctor_set_uint8(x_13, sizeof(void*)*8, x_12);
|
||||
return x_13;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
652
stage0/stdlib/Lean/Parser/Command.c
generated
652
stage0/stdlib/Lean/Parser/Command.c
generated
File diff suppressed because it is too large
Load diff
Loading…
Add table
Reference in a new issue