build.log

error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/i18n/.lake/build/lib:./.lake/packages/importGraph/.lake/build/lib:./.lake/packages/GameServer/server/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/mathlib/.lake/build/lib:./.lake/packages/checkdecls/.lake/build/lib:./.lake/packages/CMark/.lake/build/lib:./.lake/packages/UnicodeBasic/.lake/build/lib:./.lake/packages/leanInk/.lake/build/lib:./.lake/packages/doc-gen4/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/packages/i18n/.lake/build/lib:./.lake/build/lib:./.lake/packages/i18n/.lake/build/lib /home/zrtmrh/.elan/toolchains/leanprover--lean4---v4.7.0/bin/lean -Dtactic.hygienic=false -Dlinter.unusedVariables.funArgs=false -Dtrace.debug=false ./././Game/Levels/LinearMapsWorld/Level02.lean -R ././. -o ./.lake/build/lib/Game/Levels/LinearMapsWorld/Level02.olean -i ./.lake/build/lib/Game/Levels/LinearMapsWorld/Level02.ilean -c ./.lake/build/ir/Game/Levels/LinearMapsWorld/Level02.c --load-dynlib=./.lake/packages/i18n/.lake/build/lib/libleanTime.so --load-dynlib=./.lake/packages/i18n/.lake/build/lib/libTime-Basic-1.so --load-dynlib=./.lake/packages/i18n/.lake/build/lib/libTime-1.so
error: stdout:
./././Game/Levels/LinearMapsWorld/Level02.lean:19:2: error: unexpected token 'Introduction'; expected '#guard_msgs', 'DefinitionDoc', 'LemmaDoc', 'Statement', 'TacticDoc', 'TheoremDoc', 'abbrev', 'add_decl_doc', 'alias', 'axiom', 'binder_predicate', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'declare_config_elab', 'declare_opaque_type', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'irreducible_def', 'lemma', 'macro', 'macro_rules', 'notation', 'notation3', 'opaque', 'postfix', 'prefix', 'proof_wanted', 'register_builtin_option', 'register_label_attr', 'register_option', 'register_simp_attr', 'scoped', 'simproc', 'simproc_decl', 'structure', 'syntax', 'theorem' or 'unif_hint'
./././Game/Levels/LinearMapsWorld/Level02.lean:32:0: warning: Add a text to this command with `/-- yada yada -/ MyCommand`!
error: external command `/home/zrtmrh/.elan/toolchains/leanprover--lean4---v4.7.0/bin/lean` exited with code 1
[1659/1677] Building Game.Levels.LinearMapsWorld.Level02