`nanoda` and `nanoda_lib` don't work on current mathlib
bryangingechen opened this issue · 9 comments
Not sure if this is due to an issue in mathlib or in one of these programs, but I figured I'd report it here nonetheless.
Steps:
- Checkout this commit of mathlib: leanprover-community/mathlib3@6b5e48d
- Build or run
leanproject get-cache - Run
lean --recursive --export=mathlib.txt src/
Running nanoda -f ../../../mathlib/mathlib.txt (with ) results in the following error:
expr line 74; Expected a `Sort` term in inductive mod, got App(App(App(Const(Anon :: "category_theory" :: "presieve", [Param(Anon :: "v"), Param(Anon :: "u")]), Local(serial : "154208", of : Binding { pp_name: Anon :: "C", ty: Sort(1 + Param(Anon :: "u")), style: Implicit }), Local(serial : "154209", of : Binding { pp_name: Anon :: "_inst_1", ty: App(Const(Anon :: "category_theory" :: "category", [Param(Anon :: "v"), Param(Anon :: "u")]), Local(serial : "154208", of : Binding { pp_name: Anon :: "C", ty: Sort(1 + Param(Anon :: "u")), style: Implicit }), style: InstImplicit }), Local(serial : "154210", of : Binding { pp_name: Anon :: "X", ty: Local(serial : "154208", of : Binding { pp_name: Anon :: "C", ty: Sort(1 + Param(Anon :: "u")), style: Implicit }, style: Implicit })
Running cargo run --release --example basic 4 ../mathlib/mathlib.txt results in the following error:
thread 'main' panicked at 'internal error: entered unreachable code: ensur_sort could not produce a sort!', src/tc/infer.rs:190:26
See also Zulip thread
Sorry for the delay, this didn't show up on my github feed for some reason. I'll take a closer look at this over the weekend, but I did some initial probing and this shouldn't be too hard to figure out since the error is happening in one of the very first steps of the check for category_theory.presieve.singleton. The inductive modules between this version and the old version are really different, so that's extra weird.
Was the issue in the Zulip thread with leanchecker just an OOM error?
Sorry for the delay, this didn't show up on my github feed for some reason. I'll take a closer look at this over the weekend, but I did some initial probing and this shouldn't be too hard to figure out since the error is happening in one of the very first steps of the check for
category_theory.presieve.singleton. The inductive modules between this version and the old version are really different, so that's extra weird.
Cool, thanks!
Was the issue in the Zulip thread with leanchecker just an OOM error?
I think so. The tracking issue is here: leanprover-community/lean#543
Thanks again for bringing this to my attention, it now works on 6b5e48d and the most recent build, 32547fc. Now that I know leanproject get-cache exists, I'll set up something automated to build the newest version and test this repo against it. The issue is that I wasn't calling whnf on the elements of the inductive type's telescope while traversing it.
I need to implement the nested inductive support this summer, and after looking at the inductive module again I'm very motivated to give the whole thing an overhaul. I've spent a lot of time over the last 6-8 months working with the kind of indirect data structures this library is based on, and some of the design choices I made to accommodate mutuals can be done much better.
@ammkrn Thanks for looking into this!
By the way, here's another mathlib commit which crashes both leanchecker and nanoda_lib: leanprover-community/mathlib3@c8892e4 (Zulip thread)
thread '<unnamed>' panicked at 'assertion failed: self.def_eq(other, tc) == EqShort', src/tc/eq.rs:274:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread '<unnamed>' panicked at 'assertion failed: self.def_eq(other, tc) == EqShort', src/tc/eq.rs:274:9
thread 'main' panicked at 'A thread in `check_loop` panicked while being joined: Any', src/parser.rs:357:30
I'll do you one better, here's the output with RUST_BACKTRACE=full:
thread '<unnamed>' panicked at 'assertion failed: self.def_eq(other, tc) == EqShort', src/tc/eq.rs:274:9
stack backtrace:
0: 0x10d658321 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::ha0848bb2602b5d05
1: 0x10d616660 - core::fmt::write::h9f3ccac2ef682b93
2: 0x10d657ae6 - std::io::Write::write_fmt::h0a47673aab280496
3: 0x10d6574f9 - std::panicking::default_hook::{{closure}}::h850c6aaf5e80c2f5
4: 0x10d656c05 - std::panicking::rust_panic_with_hook::h76436d4cf7a368ac
5: 0x10d64c93d - std::panicking::begin_panic::{{closure}}::h42c8ca115b96f06f
6: 0x10d64c908 - std::sys_common::backtrace::__rust_end_short_backtrace::ha5b5f01b7b9176ec
7: 0x10d67d73d - std::panicking::begin_panic::he38dc4db1e029ef7
8: 0x10d624c3a - nanoda_lib::tc::infer::<impl nanoda_lib::utils::Ptr2<core::marker::PhantomData<&nanoda_lib::expr::Expr>>>::infer::hf47eafdee8afd611
9: 0x10d624474 - nanoda_lib::tc::infer::<impl nanoda_lib::utils::Ptr2<core::marker::PhantomData<&nanoda_lib::expr::Expr>>>::infer::hf47eafdee8afd611
10: 0x10d62538e - nanoda_lib::tc::infer::<impl nanoda_lib::utils::Ptr2<core::marker::PhantomData<&nanoda_lib::expr::Expr>>>::infer::hf47eafdee8afd611
11: 0x10d624474 - nanoda_lib::tc::infer::<impl nanoda_lib::utils::Ptr2<core::marker::PhantomData<&nanoda_lib::expr::Expr>>>::infer::hf47eafdee8afd611
12: 0x10d62538e - nanoda_lib::tc::infer::<impl nanoda_lib::utils::Ptr2<core::marker::PhantomData<&nanoda_lib::expr::Expr>>>::infer::hf47eafdee8afd611
13: 0x10d64b1f6 - nanoda_lib::env::Declar::check::ha5ff5c5adec213d0
14: 0x10d631b78 - crossbeam_utils::thread::ScopedThreadBuilder::spawn::{{closure}}::h49194537eb90c913
15: 0x10d64c95e - std::sys_common::backtrace::__rust_begin_short_backtrace::h561dc3c2027a3d9d
16: 0x10d6316d0 - core::ops::function::FnOnce::call_once{{vtable.shim}}::h6aede359153c24be
17: 0x10d67950d - std::sys::unix::thread::Thread::new::thread_start::hedb7cc0d930a8f40
18: 0x7fff7472a2eb - __pthread_body
19: 0x7fff7472d249 - __pthread_start
thread '<unnamed>' panicked at 'assertion failed: self.def_eq(other, tc) == EqShort', src/tc/eq.rs:274:9
stack backtrace:
0: 0x10d658321 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::ha0848bb2602b5d05
1: 0x10d616660 - core::fmt::write::h9f3ccac2ef682b93
2: 0x10d657ae6 - std::io::Write::write_fmt::h0a47673aab280496
3: 0x10d6574f9 - std::panicking::default_hook::{{closure}}::h850c6aaf5e80c2f5
4: 0x10d656c05 - std::panicking::rust_panic_with_hook::h76436d4cf7a368ac
5: 0x10d64c93d - std::panicking::begin_panic::{{closure}}::h42c8ca115b96f06f
6: 0x10d64c908 - std::sys_common::backtrace::__rust_end_short_backtrace::ha5b5f01b7b9176ec
7: 0x10d67d73d - std::panicking::begin_panic::he38dc4db1e029ef7
8: 0x10d624c3a - nanoda_lib::tc::infer::<impl nanoda_lib::utils::Ptr2<core::marker::PhantomData<&nanoda_lib::expr::Expr>>>::infer::hf47eafdee8afd611
9: 0x10d624474 - nanoda_lib::tc::infer::<impl nanoda_lib::utils::Ptr2<core::marker::PhantomData<&nanoda_lib::expr::Expr>>>::infer::hf47eafdee8afd611
10: 0x10d624474 - nanoda_lib::tc::infer::<impl nanoda_lib::utils::Ptr2<core::marker::PhantomData<&nanoda_lib::expr::Expr>>>::infer::hf47eafdee8afd611
11: 0x10d62538e - nanoda_lib::tc::infer::<impl nanoda_lib::utils::Ptr2<core::marker::PhantomData<&nanoda_lib::expr::Expr>>>::infer::hf47eafdee8afd611
12: 0x10d624474 - nanoda_lib::tc::infer::<impl nanoda_lib::utils::Ptr2<core::marker::PhantomData<&nanoda_lib::expr::Expr>>>::infer::hf47eafdee8afd611
13: 0x10d62538e - nanoda_lib::tc::infer::<impl nanoda_lib::utils::Ptr2<core::marker::PhantomData<&nanoda_lib::expr::Expr>>>::infer::hf47eafdee8afd611
14: 0x10d64b1f6 - nanoda_lib::env::Declar::check::ha5ff5c5adec213d0
15: 0x10d631b78 - crossbeam_utils::thread::ScopedThreadBuilder::spawn::{{closure}}::h49194537eb90c913
16: 0x10d64c95e - std::sys_common::backtrace::__rust_begin_short_backtrace::h561dc3c2027a3d9d
17: 0x10d6316d0 - core::ops::function::FnOnce::call_once{{vtable.shim}}::h6aede359153c24be
18: 0x10d67950d - std::sys::unix::thread::Thread::new::thread_start::hedb7cc0d930a8f40
19: 0x7fff7472a2eb - __pthread_body
20: 0x7fff7472d249 - __pthread_start
thread 'main' panicked at 'A thread in `check_loop` panicked while being joined: Any', src/parser.rs:357:30
stack backtrace:
0: 0x10d658321 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::ha0848bb2602b5d05
1: 0x10d616660 - core::fmt::write::h9f3ccac2ef682b93
2: 0x10d657ae6 - std::io::Write::write_fmt::h0a47673aab280496
3: 0x10d6574f9 - std::panicking::default_hook::{{closure}}::h850c6aaf5e80c2f5
4: 0x10d656c05 - std::panicking::rust_panic_with_hook::h76436d4cf7a368ac
5: 0x10d67519a - std::panicking::begin_panic_handler::{{closure}}::h516c76d70abf04f6
6: 0x10d675108 - std::sys_common::backtrace::__rust_end_short_backtrace::h653290b4f930faed
7: 0x10d6750b0 - _rust_begin_unwind
8: 0x10d67975f - core::panicking::panic_fmt::hde9134dd19c9a74f
9: 0x10d679d55 - core::option::expect_none_failed::h686aad664d56bca5
10: 0x10d633997 - crossbeam_utils::thread::scope::hd4b6ced884b67f63
11: 0x10d63795a - nanoda_lib::parser::Parser::parser_loop::h9f1d32c52e15c5e9
12: 0x10d613e74 - basic::main::h5e8ddbcdc3f2edae
13: 0x10d61532a - std::sys_common::backtrace::__rust_begin_short_backtrace::h2d5353a8f1cdb129
14: 0x10d6145b4 - _main
Zulip won't let me reply to your thread, it says I'm not subscribed to the stream. The offender is mv_polynomial.total_degree_mul. FWIW Trepplein is also failing, so there seems to be consensus. Trepplein's error message says mv_polynomial.degrees_mul, but that's a local error and not the top level declaration. If leanchecker is failing but the proof isn't throwing an error in Lean proper, my guess is that this is an issue with the exporter.
As a short term measure, I added an example executable examples/debug.rs that will run the checker on 1 thread only and print the names of the declarations as they're compiled and checked. You can invoke it with:
cargo run --release --example debug <path to export file>
@ammkrn Ah, that's strange; you should be able to subscribe yourself to the stream, but in the meantime, I've copied your reply to Zulip. Thanks again for looking into this!
It looks like the mystery has been solved: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.236572.20crashes.20leanchecker/near/229293401