From abd96e748f3b4c031fa10ecb370657e2a886a8df Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Nov 2016 21:30:19 -0800 Subject: [PATCH] fix(frontends/lean/parser): crash on Win 10 --- src/frontends/lean/parser.cpp | 4 ++-- tests/lean/server/crash1.input | 6 ++++++ 2 files changed, 8 insertions(+), 2 deletions(-) create mode 100644 tests/lean/server/crash1.input diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 86b65f0755..2a85bcc703 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2007,8 +2007,8 @@ expr parser::parse_tactic(unsigned) { /** \brief Helper class for creating type context only if needed */ class lazy_type_context : public abstract_type_context { - environment const & m_env; - options const & m_opts; + environment m_env; + options m_opts; std::unique_ptr m_ctx; type_context & ctx() { if (!m_ctx) diff --git a/tests/lean/server/crash1.input b/tests/lean/server/crash1.input new file mode 100644 index 0000000000..8b19434204 --- /dev/null +++ b/tests/lean/server/crash1.input @@ -0,0 +1,6 @@ +{"command":"sync","file_name":"c:/Users/leonardo/projects/lean/build/debug/tst.lean","content":"def f : nat → nat\n| 0 := 0\n| (n+1) := f n + f n\n\nopen tactic\n\n\n\nmeta def tac : tactic unit :=\ndo x ← target,\n y ← infer_type x >>= whnf,\n trace y,\n return ()\n"} +{"command":"check"} +{"command":"sync","file_name":"c:/Users/leonardo/projects/lean/build/debug/tst.lean","content":"def f : nat → nat\n| 0 := 0\n| (n+1) := f n + f n\n\nopen tactic\n\nset_option trace.compiler\n\nmeta def tac : tactic unit :=\ndo x ← target,\n y ← infer_type x >>= whnf,\n trace y,\n return ()\n"} +{"command":"check"} +{"command":"sync","file_name":"c:/Users/leonardo/projects/lean/build/debug/tst.lean","content":"def f : nat → nat\n| 0 := 0\n| (n+1) := f n + f n\n\nopen tactic\n\nset_option trace.compiler true\n\nmeta def tac : tactic unit :=\ndo x ← target,\n y ← infer_type x >>= whnf,\n trace y,\n return ()\n"} +{"command":"check"}