feat: allow @[defaultTarget] extern_lib

leanprover · Jun 10, 2022 · 6ab6051 · 6ab6051
1 parent 320b691
commit 6ab6051
Showing 1 changed file with 6 additions and 4 deletions.
diff --git a/Lake/DSL/Attributes.lean b/Lake/DSL/Attributes.lean
@@ -20,13 +20,15 @@ initialize leanLibAttr : TagAttribute ←
 initialize leanExeAttr : TagAttribute ←
   registerTagAttribute `leanExe "mark a definition as a Lake Lean executable target configuration"
 
+initialize externLibAttr : TagAttribute ←
+  registerTagAttribute `externLib "mark a definition as a Lake external library target"
+
 initialize defaultTargetAttr : TagAttribute ←
   registerTagAttribute `defaultTarget "mark a Lake target as the package's default"
     fun name => do
       let valid ← getEnv <&> fun env =>
-        leanLibAttr.hasTag env name || leanExeAttr.hasTag env name
+        leanLibAttr.hasTag env name ||
+        leanExeAttr.hasTag env name ||
+        externLibAttr.hasTag env name
       unless valid do
         throwError "attribute `defaultTarget` can only be used on a target (e.g., `lean_lib`, `lean_exe`)"
-
-initialize externLibAttr : TagAttribute ←
-  registerTagAttribute `externLib "mark a definition as a Lake external library target"