feat: none package facet to avoid warnings in scripts example

Author: tydeu

Diff for: Lake/CLI/Build.lean

@@ -16,6 +16,7 @@ def Package.defaultTarget (self : Package) : OpaqueTarget :=
   | .staticLib => self.staticLibTarget.withoutInfo
   | .sharedLib => self.sharedLibTarget.withoutInfo
   | .leanLib | .oleans => self.libTarget.withoutInfo
+  | .none => Target.nil
 
 def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package :=
   if spec.isEmpty then

Diff for: Lake/Config/Load.lean

@@ -111,7 +111,7 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
       let exes ← leanExeAttr.ext.getState env |>.foldM (init := {}) fun m d =>
         let eval := env.evalConstCheck LeanExeConfig leanOpts ``LeanExeConfig d
         return m.insert d <| ← IO.ofExcept eval.run.run
-      if libs.isEmpty && exes.isEmpty then
+      if libs.isEmpty && exes.isEmpty && !config.defaultFacet = .none then
         logWarning <| "Package targets are deprecated. " ++
           "Add a `lean_exe` and/or `lean_lib` default target to the package instead."
       let defaultTargets := defaultTargetAttr.ext.getState env |>.toArray

Diff for: Lake/Config/Package.lean

@@ -52,6 +52,7 @@ inductive PackageFacet
 | /-- The package's shared library. -/ sharedLib
 | /-- The package's lean library (e.g. `olean` / `ilean` files). -/ leanLib
 | /-- The package's `.olean` files. **DEPRECATED:** Use `leanLib` instead. -/ oleans
+| /-- The package has no buildable component. -/ none
 deriving BEq, DecidableEq, Repr
 instance : Inhabited PackageFacet := ⟨PackageFacet.exe⟩
 
@@ -221,6 +222,14 @@ structure PackageConfig extends WorkspaceConfig where
   -/
   moreLinkArgs : Array String := #[]
 
+  /--
+  Marks the package as only containing scripts.
+
+  Used to turn off deprecation warnings about package facets in packages
+  not intended to have any targets.
+  -/
+  scriptsOnly : Bool := false
+
 deriving Inhabited
 
 namespace PackageConfig

Diff for: examples/scripts/lakefile.lean

@@ -1,7 +1,8 @@
 import Lake
 open Lake DSL
 
-package scripts
+package scripts where
+  defaultFacet := .none
 
 /--
 Display a greeting