-
-
Save WildCryptoFox/a3c2de85461ed212c174b62565346d1b to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#0 0x000000000061e834 in lean::get_ginductive_num_params(lean::environment const&, lean::name const&) () | |
#1 0x000000000095072d in lean::for_each_compatible_constructor(lean::type_context_old&, lean::expr const&, std::function<void (lean::expr const&, lean::buffer<lean::expr, 16u>&)> const&) () | |
#2 0x0000000000ad352f in lean::elim_match_fn::process_complete(lean::elim_match_fn::problem const&) () | |
#3 0x0000000000acd0a2 in lean::elim_match_fn::process(lean::elim_match_fn::problem const&) () | |
#4 0x0000000000acde27 in lean::elim_match_fn::process_constructor_core(lean::elim_match_fn::problem const&, bool) () | |
#5 0x0000000000acd0c0 in lean::elim_match_fn::process(lean::elim_match_fn::problem const&) () | |
#6 0x0000000000ad35c4 in lean::elim_match_fn::process_complete(lean::elim_match_fn::problem const&) () | |
#7 0x0000000000acd0a2 in lean::elim_match_fn::process(lean::elim_match_fn::problem const&) () | |
#8 0x0000000000ad048c in lean::elim_match_fn::process_variable_inaccessible(lean::elim_match_fn::problem const&, bool) () | |
#9 0x0000000000ad0e26 in lean::elim_match_fn::process_inaccessible(lean::elim_match_fn::problem const&) () | |
#10 0x0000000000accfcf in lean::elim_match_fn::process(lean::elim_match_fn::problem const&) () | |
#11 0x0000000000acde27 in lean::elim_match_fn::process_constructor_core(lean::elim_match_fn::problem const&, bool) () | |
#12 0x0000000000acd0c0 in lean::elim_match_fn::process(lean::elim_match_fn::problem const&) () | |
#13 0x0000000000ad35c4 in lean::elim_match_fn::process_complete(lean::elim_match_fn::problem const&) () | |
#14 0x0000000000acd0a2 in lean::elim_match_fn::process(lean::elim_match_fn::problem const&) () | |
#15 0x0000000000ace85b in lean::elim_match_fn::operator()(lean::local_context const&, lean::expr const&) () | |
#16 0x0000000000ac210f in lean::elim_match(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&) () | |
#17 0x0000000000ac2678 in lean::mk_nonrec(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&) () | |
#18 0x0000000000958431 in lean::compile_equations_core(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&) () | |
#19 0x0000000000958923 in lean::compile_equations_main(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&, bool) () | |
#20 0x0000000000959e21 in lean::compile_equations(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&) () | |
#21 0x00000000007899d2 in lean::elaborator::visit_equations(lean::expr const&) () | |
#22 0x00000000007820d9 in lean::elaborator::visit_macro(lean::expr const&, lean::optional<lean::expr> const&, bool) () | |
#23 0x0000000000782c76 in lean::elaborator::visit(lean::expr const&, lean::optional<lean::expr> const&) () | |
#24 0x00000000007932bd in lean::elaborator::elaborate_with_type(lean::expr const&, lean::expr const&) () | |
#25 0x00000000007bcb0c in lean::single_definition_cmd_core(lean::parser_info&, lean::decl_cmd_kind, lean::cmd_meta)::{lambda(lean::expr)#1}::operator()(lean::expr) const () | |
#26 0x00000000007be8ae in lean::single_definition_cmd_core(lean::parser_info&, lean::decl_cmd_kind, lean::cmd_meta) () | |
#27 0x00000000007c054f in lean::definition_cmd_core(lean::parser&, lean::decl_cmd_kind, lean::cmd_meta const&) () | |
#28 0x00000000006fc506 in lean::definition_cmd(lean::parser&, lean::cmd_meta const&) () | |
#29 0x00000000006decb5 in std::_Function_handler<lean::environment (lean::parser&, lean::cmd_meta const&), lean::environment (*)(lean::parser&, lean::cmd_meta const&)>::_M_invoke(std::_Any_data const&, lean::parser&, lean::cmd_meta const&) () | |
#30 0x00000000006ba00f in lean::parser::parse_command(lean::cmd_meta const&) () | |
#31 0x00000000006ba99f in lean::parser::parse_command_like() () | |
#32 0x00000000007dca03 in lean::module_parser::parse_next_command_like(lean::optional<std::vector<std::shared_ptr<lean::gtask_cell>, std::allocator<std::shared_ptr<lean::gtask_cell> > > > const&)::{lambda()#1}::operator()() const () | |
#33 0x00000000007e120e in lean::task_builder<lean::module_parser_result>::base_task_imp<lean::module_parser::parse_next_command_like(lean::optional<std::vector<std::shared_ptr<lean::gtask_cell>, std::allocator<std::shared_ptr<lean::gtask_cell> > > > const&)::{lambda()#1}>::execute(void*) () | |
#34 0x00000000005c75da in lean::library_scopes_imp::execute(void*) () | |
#35 0x00000000004d530a in lean::cancellable_task_imp::execute(void*) () | |
#36 0x00000000007e29b0 in lean::task_cell<lean::module_parser_result>::execute() () | |
#37 0x00000000004d4fc0 in lean::task_queue::execute(std::shared_ptr<lean::gtask_cell> const&) () | |
#38 0x00000000005c378f in std::_Function_handler<void (), lean::mt_task_queue::spawn_worker()::{lambda()#1}>::_M_invoke(std::_Any_data const&) () | |
#39 0x00000000004d21e5 in lean::lthread::imp::_main(void*) () | |
#40 0x0000000000491d1b in start_thread (arg=0x7ffff7ff8700) at pthread_create.c:463 | |
#41 0x0000000000c53c8f in clone () |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
$ time lean src/segfault.lean ; echo $? ; time lean --trust=0 src/segfault.lean ; echo $? | |
Segmentation fault | |
real 0m0.328s | |
user 0m0.300s | |
sys 0m0.031s | |
139 | |
Segmentation fault | |
real 0m2.183s | |
user 0m2.133s | |
sys 0m0.050s | |
139 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
structure bar (x : Type) := | |
(data : x) | |
inductive foo | |
| q {c} (x : bar c) | |
namespace foo | |
def z : foo → unit | |
| (q (⟨tt⟩ : bar bool)) := () | |
| _ := () | |
end foo |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Lean (version 3.18.4, commit f539be1e867c, Release)