max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Sebastian Ullrich 2022-07-06 09:52:51 +02:00
parent 775ed70a84
commit ec991f3761
6 changed files with 1455 additions and 470 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
stage0/src/Lean/Elab/Declaration.lean generated
View file

@ -94,12 +94,14 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
match sortDeclLevelParams scopeLevelNames allUserLevelNames usedParams with
| Except.error msg => throwErrorAt stx msg
| Except.ok levelParams =>
let type ← instantiateMVars type
let decl := Declaration.axiomDecl {
name := declName,
levelParams := levelParams,
type := type,
isUnsafe := modifiers.isUnsafe
}
trace[Elab.axiom] "{declName} : {type}"
Term.ensureNoUnassignedMVars decl
addDecl decl
withSaveInfoContext do -- save new env
@ -342,4 +344,7 @@ def expandInitCmd (builtin : Bool) : Macro := fun stx => do
@[builtinMacro Lean.Parser.Command.«builtin_initialize»] def expandBuiltinInitialize : Macro :=
expandInitCmd (builtin := true)
builtin_initialize
registerTraceClass `Elab.axiom
end Lean.Elab.Command

25
stage0/src/Lean/Elab/Import.lean generated
View file

@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
import Lean.Parser.Module
import Lean.Data.Json
namespace Lean.Elab
def headerToImports (header : Syntax) : List Import :=
@ -38,4 +40,27 @@ def printImports (input : String) (fileName : Option String) : IO Unit := do
let fname ← findOLean dep.module
IO.println fname
deriving instance ToJson for Import
structure PrintImportResult where
imports? : Option (Array Import) := none
errors : Array String := #[]
deriving ToJson
structure PrintImportsResult where
imports : Array PrintImportResult
deriving ToJson
@[export lean_print_imports_json]
def printImportsJson (fileNames : Array String) : IO Unit := do
let rs ← fileNames.mapM fun fn => do
try
let (deps, _, msgs) ← parseImports (← IO.FS.readFile ⟨fn⟩) fn
if msgs.hasErrors then
return { errors := (← msgs.toList.toArray.mapM (·.toString)) }
else
return { imports? := some deps.toArray }
catch e => return { errors := #[e.toString] }
IO.println (toJson { imports := rs : PrintImportsResult })
end Lean.Elab

8
stage0/src/Std/Data/PersistentArray.lean generated
View file

@ -71,7 +71,7 @@ partial def setAux : PersistentArrayNode α → USize → USize → α → Persi
let j := div2Shift i shift
let i := mod2Shift i shift
let shift := shift - initShift
node $ cs.modify j.toNat $ fun c => setAux c i shift a
node <| cs.modify j.toNat fun c => setAux c i shift a
| leaf cs, i, _, a => leaf (cs.set! i.toNat a)
def set (t : PersistentArray α) (i : Nat) (a : α) : PersistentArray α :=
@ -85,7 +85,7 @@ def set (t : PersistentArray α) (i : Nat) (a : α) : PersistentArray α :=
let j := div2Shift i shift
let i := mod2Shift i shift
let shift := shift - initShift
node $ cs.modify j.toNat $ fun c => modifyAux f c i shift
node <| cs.modify j.toNat fun c => modifyAux f c i shift
| leaf cs, i, _ => leaf (cs.modify i.toNat f)
@[specialize] def modify [Inhabited α] (t : PersistentArray α) (i : Nat) (f : α → α) : PersistentArray α :=
@ -109,9 +109,9 @@ partial def insertNewLeaf : PersistentArrayNode α → USize → USize → Array
let i := mod2Shift i shift
let shift := shift - initShift
if j.toNat < cs.size then
node $ cs.modify j.toNat fun c => insertNewLeaf c i shift a
node <| cs.modify j.toNat fun c => insertNewLeaf c i shift a
else
node $ cs.push $ mkNewPath shift a
node <| cs.push <| mkNewPath shift a
| n, _, _, _ => n -- unreachable
def mkNewTail (t : PersistentArray α) : PersistentArray α :=

22
stage0/src/util/shell.cpp generated
View file

@ -20,6 +20,7 @@ Author: Leonardo de Moura
#include "runtime/debug.h"
#include "runtime/sstream.h"
#include "runtime/load_dynlib.h"
#include "runtime/array_ref.h"
#include "util/timer.h"
#include "util/macros.h"
#include "util/io.h"
@ -233,6 +234,7 @@ static struct option g_long_options[] = {
{"stats", no_argument, 0, 'a'},
{"quiet", no_argument, 0, 'q'},
{"deps", no_argument, 0, 'd'},
{"deps-json", no_argument, 0, 'J'},
{"timeout", optional_argument, 0, 'T'},
{"c", optional_argument, 0, 'c'},
{"exitOnPanic", no_argument, 0, 'e'},
@ -392,6 +394,12 @@ void print_imports(std::string const & input, std::string const & fname) {
consume_io_result(lean_print_imports(mk_string(input), mk_option_some(mk_string(fname)), io_mk_world()));
}
/* def printImportsJson (fileNames : Array String) : IO Unit */
extern "C" object* lean_print_imports_json(object * file_names, object * w);
void print_imports_json(array_ref<string_ref> const & fnames) {
consume_io_result(lean_print_imports_json(fnames.to_obj_arg(), io_mk_world()));
}
extern "C" object* lean_environment_free_regions(object * env, object * w);
void environment_free_regions(environment && env) {
consume_io_result(lean_environment_free_regions(env.steal(), io_mk_world()));
@ -442,6 +450,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
bool use_stdin = false;
unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL + 1;
bool only_deps = false;
bool deps_json = false;
bool stats = false;
// 0 = don't run server, 1 = watchdog, 2 = worker
int run_server = 0;
@ -535,6 +544,10 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
case 'd':
only_deps = true;
break;
case 'J':
only_deps = true;
deps_json = true;
break;
case 'a':
stats = true;
break;
@ -622,6 +635,15 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
else if (run_server == 2)
return run_server_worker(opts);
if (only_deps && deps_json) {
buffer<string_ref> fns;
for (int i = optind; i < argc; i++) {
fns.push_back(string_ref(argv[i]));
}
print_imports_json(fns);
return 0;
}
if (use_stdin) {
if (argc - optind != 0) {
mod_fn = argv[optind++];

1135
stage0/stdlib/Lean/Elab/Declaration.c generated
View file

File diff suppressed because it is too large Load diff

730
stage0/stdlib/Lean/Elab/Import.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab.Import
// Imports: Init Lean.Parser.Module
// Imports: Init Lean.Parser.Module Lean.Data.Json
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -14,40 +14,88 @@
extern "C" {
#endif
lean_object* l_List_reverse___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_instToJsonImport;
lean_object* lean_string_push(lean_object*, uint32_t);
size_t lean_usize_add(size_t, size_t);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__1(size_t, size_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_517_(lean_object*);
static lean_object* l_Lean_Elab_headerToImports___closed__4;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Parser_parseHeader(lean_object*, lean_object*);
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* lean_io_error_to_string(lean_object*);
static lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401____closed__1;
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
static lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401____closed__2;
static lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_PrintImportResult_imports_x3f___default;
static lean_object* l_Lean_Elab_headerToImports___closed__2;
LEAN_EXPORT lean_object* l_Lean_Elab_headerToImports(lean_object*);
lean_object* l_Lean_Parser_mkInputContext(lean_object*, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_517____spec__1(size_t, size_t, lean_object*);
static lean_object* l_Lean_Elab_PrintImportResult_errors___default___closed__1;
lean_object* l_List_join___rarg(lean_object*);
uint8_t lean_usize_dec_lt(size_t, size_t);
static lean_object* l_Lean_Elab_headerToImports___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_headerToImports___boxed(lean_object*);
static lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___closed__1;
lean_object* l_Lean_findOLean(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_processHeader(lean_object*, lean_object*, lean_object*, lean_object*, uint32_t, lean_object*);
static lean_object* l_Lean_Elab_parseImports___closed__1;
lean_object* l_Lean_MessageLog_toList(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_headerToImports___closed__3;
static lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____closed__2;
lean_object* l_Lean_Name_toString(lean_object*, uint8_t);
lean_object* l_IO_print___at_IO_println___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Elab_printImports___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getId(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__3(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_processHeader___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_to_list(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_processHeader___closed__1;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_517____spec__1___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_PrintImportResult_errors___default;
lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
lean_object* l_Lean_FileMap_ofString(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472_(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401_(lean_object*);
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_Syntax_getPos_x3f(lean_object*, uint8_t);
lean_object* lean_mk_empty_environment(uint32_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_import_modules(lean_object*, lean_object*, uint32_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__2(size_t, size_t, lean_object*);
lean_object* l_List_redLength___rarg(lean_object*);
lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instToJsonPrintImportsResult___closed__1;
lean_object* l_Lean_Syntax_getArgs(lean_object*);
static lean_object* l_Lean_Elab_instToJsonPrintImportResult___closed__1;
lean_object* l_Lean_Json_mkObj(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_instToJsonPrintImportResult;
lean_object* l_Lean_Json_pretty(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instToJsonImport___closed__1;
lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNone(lean_object*);
LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_headerToImports___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_parseImports(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2(size_t, size_t, lean_object*, lean_object*);
lean_object* l_IO_FS_readFile(lean_object*, lean_object*);
LEAN_EXPORT lean_object* lean_print_imports(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_println___at_Lean_Elab_printImports___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_println___at_Lean_Elab_printImportsJson___spec__3(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Std_PersistentArray_anyM___at_Lean_MessageLog_hasErrors___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__3___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Message_toString(lean_object*, uint8_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_instToJsonPrintImportsResult;
lean_object* l_List_appendTR___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* lean_print_imports_json(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_headerToImports___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -1064,8 +1112,657 @@ return x_21;
}
}
}
static lean_object* _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("module", 6);
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401____closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("runtimeOnly", 11);
return x_1;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t 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; lean_object* x_18;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = 1;
x_4 = l_Lean_Name_toString(x_2, x_3);
x_5 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_5, 0, x_4);
x_6 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401____closed__1;
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_5);
x_8 = lean_box(0);
x_9 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_9, 0, x_7);
lean_ctor_set(x_9, 1, x_8);
x_10 = lean_ctor_get_uint8(x_1, sizeof(void*)*1);
lean_dec(x_1);
x_11 = lean_alloc_ctor(1, 0, 1);
lean_ctor_set_uint8(x_11, 0, x_10);
x_12 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401____closed__2;
x_13 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_11);
x_14 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_8);
x_15 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_8);
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_9);
lean_ctor_set(x_16, 1, x_15);
x_17 = l_List_join___rarg(x_16);
x_18 = l_Lean_Json_mkObj(x_17);
return x_18;
}
}
static lean_object* _init_l_Lean_Elab_instToJsonImport___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401_), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_instToJsonImport() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Elab_instToJsonImport___closed__1;
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_PrintImportResult_imports_x3f___default() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_PrintImportResult_errors___default___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_PrintImportResult_errors___default() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Elab_PrintImportResult_errors___default___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__2(size_t x_1, size_t x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
x_4 = lean_usize_dec_lt(x_2, x_1);
if (x_4 == 0)
{
return x_3;
}
else
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x_9; size_t x_10; lean_object* x_11;
x_5 = lean_array_uget(x_3, x_2);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_array_uset(x_3, x_2, x_6);
x_8 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401_(x_5);
x_9 = 1;
x_10 = lean_usize_add(x_2, x_9);
x_11 = lean_array_uset(x_7, x_2, x_8);
x_2 = x_10;
x_3 = x_11;
goto _start;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_3;
lean_dec(x_1);
x_3 = lean_box(0);
return x_3;
}
else
{
lean_object* x_4; lean_object* x_5; size_t x_6; size_t x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_4 = lean_ctor_get(x_2, 0);
lean_inc(x_4);
lean_dec(x_2);
x_5 = lean_array_get_size(x_4);
x_6 = lean_usize_of_nat(x_5);
lean_dec(x_5);
x_7 = 0;
x_8 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__2(x_6, x_7, x_4);
x_9 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_9, 0, x_8);
x_10 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_10, 0, x_1);
lean_ctor_set(x_10, 1, x_9);
x_11 = lean_box(0);
x_12 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
return x_12;
}
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__3(size_t x_1, size_t x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
x_4 = lean_usize_dec_lt(x_2, x_1);
if (x_4 == 0)
{
return x_3;
}
else
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x_9; size_t x_10; lean_object* x_11;
x_5 = lean_array_uget(x_3, x_2);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_array_uset(x_3, x_2, x_6);
x_8 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_8, 0, x_5);
x_9 = 1;
x_10 = lean_usize_add(x_2, x_9);
x_11 = lean_array_uset(x_7, x_2, x_8);
x_2 = x_10;
x_3 = x_11;
goto _start;
}
}
}
static lean_object* _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("imports", 7);
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("errors", 6);
return x_1;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; size_t x_7; size_t x_8; lean_object* x_9; 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; lean_object* x_18;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____closed__1;
x_4 = l_Lean_Json_opt___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__1(x_3, x_2);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_array_get_size(x_5);
x_7 = lean_usize_of_nat(x_6);
lean_dec(x_6);
x_8 = 0;
x_9 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__3(x_7, x_8, x_5);
x_10 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_10, 0, x_9);
x_11 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____closed__2;
x_12 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_12, 0, x_11);
lean_ctor_set(x_12, 1, x_10);
x_13 = lean_box(0);
x_14 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_14, 0, x_12);
lean_ctor_set(x_14, 1, x_13);
x_15 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_13);
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_4);
lean_ctor_set(x_16, 1, x_15);
x_17 = l_List_join___rarg(x_16);
x_18 = l_Lean_Json_mkObj(x_17);
return x_18;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_4; size_t x_5; lean_object* x_6;
x_4 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__2(x_4, x_5, x_3);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_4; size_t x_5; lean_object* x_6;
x_4 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____spec__3(x_4, x_5, x_3);
return x_6;
}
}
static lean_object* _init_l_Lean_Elab_instToJsonPrintImportResult___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472_), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_instToJsonPrintImportResult() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Elab_instToJsonPrintImportResult___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_517____spec__1(size_t x_1, size_t x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
x_4 = lean_usize_dec_lt(x_2, x_1);
if (x_4 == 0)
{
return x_3;
}
else
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x_9; size_t x_10; lean_object* x_11;
x_5 = lean_array_uget(x_3, x_2);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_array_uset(x_3, x_2, x_6);
x_8 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472_(x_5);
x_9 = 1;
x_10 = lean_usize_add(x_2, x_9);
x_11 = lean_array_uset(x_7, x_2, x_8);
x_2 = x_10;
x_3 = x_11;
goto _start;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_517_(lean_object* x_1) {
_start:
{
lean_object* x_2; size_t x_3; size_t x_4; 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; lean_object* x_12; lean_object* x_13;
x_2 = lean_array_get_size(x_1);
x_3 = lean_usize_of_nat(x_2);
lean_dec(x_2);
x_4 = 0;
x_5 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_517____spec__1(x_3, x_4, x_1);
x_6 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_6, 0, x_5);
x_7 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____closed__1;
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_6);
x_9 = lean_box(0);
x_10 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_10, 0, x_8);
lean_ctor_set(x_10, 1, x_9);
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_11, 1, x_9);
x_12 = l_List_join___rarg(x_11);
x_13 = l_Lean_Json_mkObj(x_12);
return x_13;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_517____spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_4; size_t x_5; lean_object* x_6;
x_4 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_517____spec__1(x_4, x_5, x_3);
return x_6;
}
}
static lean_object* _init_l_Lean_Elab_instToJsonPrintImportsResult___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_517_), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_instToJsonPrintImportsResult() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Elab_instToJsonPrintImportsResult___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__1(size_t x_1, size_t x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = lean_usize_dec_lt(x_2, x_1);
if (x_5 == 0)
{
lean_object* x_6;
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_3);
lean_ctor_set(x_6, 1, x_4);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11;
x_7 = lean_array_uget(x_3, x_2);
x_8 = lean_unsigned_to_nat(0u);
x_9 = lean_array_uset(x_3, x_2, x_8);
x_10 = 0;
x_11 = l_Lean_Message_toString(x_7, x_10, x_4);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13; size_t x_14; size_t x_15; lean_object* x_16;
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = 1;
x_15 = lean_usize_add(x_2, x_14);
x_16 = lean_array_uset(x_9, x_2, x_12);
x_2 = x_15;
x_3 = x_16;
x_4 = x_13;
goto _start;
}
else
{
uint8_t x_18;
lean_dec(x_9);
x_18 = !lean_is_exclusive(x_11);
if (x_18 == 0)
{
return x_11;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_11, 0);
x_20 = lean_ctor_get(x_11, 1);
lean_inc(x_20);
lean_inc(x_19);
lean_dec(x_11);
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
return x_21;
}
}
}
}
}
static lean_object* _init_l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(1u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2(size_t x_1, size_t x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = lean_usize_dec_lt(x_2, x_1);
if (x_5 == 0)
{
lean_object* x_6;
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_3);
lean_ctor_set(x_6, 1, x_4);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_22;
x_7 = lean_array_uget(x_3, x_2);
x_8 = lean_unsigned_to_nat(0u);
x_9 = lean_array_uset(x_3, x_2, x_8);
x_22 = l_IO_FS_readFile(x_7, x_4);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_23 = lean_ctor_get(x_22, 0);
lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
lean_dec(x_22);
x_25 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_25, 0, x_7);
x_26 = l_Lean_Elab_parseImports(x_23, x_25, x_24);
if (lean_obj_tag(x_26) == 0)
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; uint8_t x_32;
x_27 = lean_ctor_get(x_26, 0);
lean_inc(x_27);
x_28 = lean_ctor_get(x_27, 1);
lean_inc(x_28);
x_29 = lean_ctor_get(x_26, 1);
lean_inc(x_29);
lean_dec(x_26);
x_30 = lean_ctor_get(x_27, 0);
lean_inc(x_30);
lean_dec(x_27);
x_31 = lean_ctor_get(x_28, 1);
lean_inc(x_31);
lean_dec(x_28);
lean_inc(x_31);
x_32 = l_Std_PersistentArray_anyM___at_Lean_MessageLog_hasErrors___spec__1(x_31);
if (x_32 == 0)
{
lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; size_t x_39; size_t x_40; lean_object* x_41;
lean_dec(x_31);
x_33 = l_List_redLength___rarg(x_30);
x_34 = lean_mk_empty_array_with_capacity(x_33);
lean_dec(x_33);
x_35 = l_List_toArrayAux___rarg(x_30, x_34);
x_36 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_36, 0, x_35);
x_37 = l_Lean_Elab_PrintImportResult_errors___default___closed__1;
x_38 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_38, 0, x_36);
lean_ctor_set(x_38, 1, x_37);
x_39 = 1;
x_40 = lean_usize_add(x_2, x_39);
x_41 = lean_array_uset(x_9, x_2, x_38);
x_2 = x_40;
x_3 = x_41;
x_4 = x_29;
goto _start;
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; size_t x_48; size_t x_49; lean_object* x_50;
lean_dec(x_30);
x_43 = l_Lean_MessageLog_toList(x_31);
x_44 = l_List_redLength___rarg(x_43);
x_45 = lean_mk_empty_array_with_capacity(x_44);
lean_dec(x_44);
x_46 = l_List_toArrayAux___rarg(x_43, x_45);
x_47 = lean_array_get_size(x_46);
x_48 = lean_usize_of_nat(x_47);
lean_dec(x_47);
x_49 = 0;
x_50 = l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__1(x_48, x_49, x_46, x_29);
if (lean_obj_tag(x_50) == 0)
{
lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; size_t x_55; size_t x_56; lean_object* x_57;
x_51 = lean_ctor_get(x_50, 0);
lean_inc(x_51);
x_52 = lean_ctor_get(x_50, 1);
lean_inc(x_52);
lean_dec(x_50);
x_53 = lean_box(0);
x_54 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_54, 1, x_51);
x_55 = 1;
x_56 = lean_usize_add(x_2, x_55);
x_57 = lean_array_uset(x_9, x_2, x_54);
x_2 = x_56;
x_3 = x_57;
x_4 = x_52;
goto _start;
}
else
{
lean_object* x_59; lean_object* x_60;
x_59 = lean_ctor_get(x_50, 0);
lean_inc(x_59);
x_60 = lean_ctor_get(x_50, 1);
lean_inc(x_60);
lean_dec(x_50);
x_10 = x_59;
x_11 = x_60;
goto block_21;
}
}
}
else
{
lean_object* x_61; lean_object* x_62;
x_61 = lean_ctor_get(x_26, 0);
lean_inc(x_61);
x_62 = lean_ctor_get(x_26, 1);
lean_inc(x_62);
lean_dec(x_26);
x_10 = x_61;
x_11 = x_62;
goto block_21;
}
}
else
{
lean_object* x_63; lean_object* x_64;
lean_dec(x_7);
x_63 = lean_ctor_get(x_22, 0);
lean_inc(x_63);
x_64 = lean_ctor_get(x_22, 1);
lean_inc(x_64);
lean_dec(x_22);
x_10 = x_63;
x_11 = x_64;
goto block_21;
}
block_21:
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; size_t x_17; size_t x_18; lean_object* x_19;
x_12 = lean_box(0);
x_13 = lean_io_error_to_string(x_10);
x_14 = l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___closed__1;
x_15 = lean_array_push(x_14, x_13);
x_16 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_16, 0, x_12);
lean_ctor_set(x_16, 1, x_15);
x_17 = 1;
x_18 = lean_usize_add(x_2, x_17);
x_19 = lean_array_uset(x_9, x_2, x_16);
x_2 = x_18;
x_3 = x_19;
x_4 = x_11;
goto _start;
}
}
}
}
LEAN_EXPORT lean_object* l_IO_println___at_Lean_Elab_printImportsJson___spec__3(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; uint32_t x_5; lean_object* x_6; lean_object* x_7;
x_3 = lean_unsigned_to_nat(80u);
x_4 = l_Lean_Json_pretty(x_1, x_3);
x_5 = 10;
x_6 = lean_string_push(x_4, x_5);
x_7 = l_IO_print___at_IO_println___spec__1(x_6, x_2);
return x_7;
}
}
LEAN_EXPORT lean_object* lean_print_imports_json(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; size_t x_4; size_t x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_3 = lean_array_get_size(x_1);
x_4 = lean_usize_of_nat(x_3);
lean_dec(x_3);
x_5 = 0;
x_6 = l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2(x_4, x_5, x_1, x_2);
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_6, 1);
lean_inc(x_8);
lean_dec(x_6);
x_9 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_517_(x_7);
x_10 = l_IO_println___at_Lean_Elab_printImportsJson___spec__3(x_9, x_8);
return x_10;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7;
x_5 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_6 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_7 = l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__1(x_5, x_6, x_3, x_4);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7;
x_5 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_6 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_7 = l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2(x_5, x_6, x_3, x_4);
return x_7;
}
}
lean_object* initialize_Init(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Parser_Module(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Data_Json(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Elab_Import(uint8_t builtin, lean_object* w) {
lean_object * res;
@ -1077,6 +1774,9 @@ lean_dec_ref(res);
res = initialize_Lean_Parser_Module(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Data_Json(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_headerToImports___closed__1 = _init_l_Lean_Elab_headerToImports___closed__1();
lean_mark_persistent(l_Lean_Elab_headerToImports___closed__1);
l_Lean_Elab_headerToImports___closed__2 = _init_l_Lean_Elab_headerToImports___closed__2();
@ -1089,6 +1789,34 @@ l_Lean_Elab_processHeader___closed__1 = _init_l_Lean_Elab_processHeader___closed
lean_mark_persistent(l_Lean_Elab_processHeader___closed__1);
l_Lean_Elab_parseImports___closed__1 = _init_l_Lean_Elab_parseImports___closed__1();
lean_mark_persistent(l_Lean_Elab_parseImports___closed__1);
l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401____closed__1 = _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401____closed__1();
lean_mark_persistent(l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401____closed__1);
l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401____closed__2 = _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401____closed__2();
lean_mark_persistent(l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_401____closed__2);
l_Lean_Elab_instToJsonImport___closed__1 = _init_l_Lean_Elab_instToJsonImport___closed__1();
lean_mark_persistent(l_Lean_Elab_instToJsonImport___closed__1);
l_Lean_Elab_instToJsonImport = _init_l_Lean_Elab_instToJsonImport();
lean_mark_persistent(l_Lean_Elab_instToJsonImport);
l_Lean_Elab_PrintImportResult_imports_x3f___default = _init_l_Lean_Elab_PrintImportResult_imports_x3f___default();
lean_mark_persistent(l_Lean_Elab_PrintImportResult_imports_x3f___default);
l_Lean_Elab_PrintImportResult_errors___default___closed__1 = _init_l_Lean_Elab_PrintImportResult_errors___default___closed__1();
lean_mark_persistent(l_Lean_Elab_PrintImportResult_errors___default___closed__1);
l_Lean_Elab_PrintImportResult_errors___default = _init_l_Lean_Elab_PrintImportResult_errors___default();
lean_mark_persistent(l_Lean_Elab_PrintImportResult_errors___default);
l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____closed__1 = _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____closed__1();
lean_mark_persistent(l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____closed__1);
l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____closed__2 = _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____closed__2();
lean_mark_persistent(l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_472____closed__2);
l_Lean_Elab_instToJsonPrintImportResult___closed__1 = _init_l_Lean_Elab_instToJsonPrintImportResult___closed__1();
lean_mark_persistent(l_Lean_Elab_instToJsonPrintImportResult___closed__1);
l_Lean_Elab_instToJsonPrintImportResult = _init_l_Lean_Elab_instToJsonPrintImportResult();
lean_mark_persistent(l_Lean_Elab_instToJsonPrintImportResult);
l_Lean_Elab_instToJsonPrintImportsResult___closed__1 = _init_l_Lean_Elab_instToJsonPrintImportsResult___closed__1();
lean_mark_persistent(l_Lean_Elab_instToJsonPrintImportsResult___closed__1);
l_Lean_Elab_instToJsonPrintImportsResult = _init_l_Lean_Elab_instToJsonPrintImportsResult();
lean_mark_persistent(l_Lean_Elab_instToJsonPrintImportsResult);
l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___closed__1 = _init_l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___closed__1();
lean_mark_persistent(l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___closed__1);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus