From 73065860f3f78e663fa45b69d0ba1964e7d497ff Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 16 Oct 2020 17:52:18 +0200
Subject: [PATCH] fix: refuse to generate code for imported parsers to avoid
 duplicate declarations

---
 src/Lean/ParserCompiler.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index 33f6aabf09..79617414a5 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -68,6 +68,8 @@ match e with
       -- synthesize a new `[combinatorAttr c]`
       some value ← pure cinfo.value?
         | throwError $ "don't know how to generate " ++ ctx.varName ++ " for non-definition '" ++ toString e ++ "'";
+      none ← pure $ env.getModuleIdxFor? c
+        | throwError $ "refusing to generate code for imported parser declaration '" ++ c ++ "'; use `@[runParserAttributeHooks]` on its definition instead.";
       value ← compileParserBody $ preprocessParserBody ctx value;
       ty ← forallTelescope cinfo.type fun params _ =>
         params.foldrM (fun param ty => do