diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index eb5fb4692..aea843cca 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2346,7 +2346,8 @@ class parser::imp { return; } try { - parser import_parser(m_env, m_io_state, in, m_script_state, true /* use exceptions */, false /* not interactive */); + script_state state; // Empty state object for the imported module + parser import_parser(m_env, m_io_state, in, &state, true /* use exceptions */, false /* not interactive */); import_parser(); } catch (interrupted &) { throw; diff --git a/tests/lean/macro.lean b/tests/lean/macro.lean new file mode 100644 index 000000000..fa7434d91 --- /dev/null +++ b/tests/lean/macro.lean @@ -0,0 +1,11 @@ +(** +macro("IdMacro", + { macro_arg.Expr }, + function (env, e) + return e + end +) +**) + +Show IdMacro 10. +Import "module.lean" diff --git a/tests/lean/macro.lean.expected.out b/tests/lean/macro.lean.expected.out new file mode 100644 index 000000000..62a807e22 --- /dev/null +++ b/tests/lean/macro.lean.expected.out @@ -0,0 +1,5 @@ + Set: pp::colors + Set: pp::unicode +10 +Error (line: 2, pos: 5) unknown identifier 'IdMacro' +Error (line: 11, pos: 0) failed to import file './module.lean' diff --git a/tests/lean/module.lean b/tests/lean/module.lean new file mode 100644 index 000000000..7b10352c0 --- /dev/null +++ b/tests/lean/module.lean @@ -0,0 +1,2 @@ +(* The following command should fail because the IdMacro is not defined *) +Show IdMacro 20. \ No newline at end of file diff --git a/tests/lean/module.lean.expected.out b/tests/lean/module.lean.expected.out new file mode 100644 index 000000000..2607ee6d7 --- /dev/null +++ b/tests/lean/module.lean.expected.out @@ -0,0 +1,3 @@ + Set: pp::colors + Set: pp::unicode +Error (line: 2, pos: 5) unknown identifier 'IdMacro'