refactor: remove module facet special casing

Lake/Build/Facets.lean

@@ -39,24 +39,24 @@ which produce the Lean binaries of the module (i.e., `olean` and `ilean`).
 It is thus the facet used by default for building imports of a module.
 Also, if the module is not lean-only, it produces `c` files as well.
 -/
-abbrev Module.leanBinFacet  := `lean.bin
-module_data lean.bin : ActiveOpaqueTarget
+abbrev Module.leanBinFacet := `bin
+module_data bin : ActiveOpaqueTarget
 
 /-- The `olean` file produced by `lean`  -/
-abbrev Module.oleanFacet  := `olean
+abbrev Module.oleanFacet := `olean
 module_data olean : ActiveFileTarget
 
 /-- The `ilean` file produced by `lean` -/
 abbrev Module.ileanFacet := `ilean
 module_data ilean : ActiveFileTarget
 
 /-- The C file built from the Lean file via `lean` -/
-abbrev Module.cFacet := `lean.c
-module_data lean.c : ActiveFileTarget
+abbrev Module.cFacet := `c
+module_data c : ActiveFileTarget
 
 /-- The object file built from `lean.c` -/
-abbrev Module.oFacet := `lean.o
-module_data lean.o : ActiveFileTarget
+abbrev Module.oFacet := `o
+module_data o : ActiveFileTarget
 
 /-- Shared library for `--load-dynlib` -/
 abbrev Module.dynlibFacet := `dynlib

Lake/CLI/Build.lean

@@ -18,18 +18,8 @@ def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package
 
 open Module in
 def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except CliError OpaqueTarget :=
-  if facet.isAnonymous || facet == `bin  then
+  if facet.isAnonymous then
     return mod.facetTarget leanBinFacet
-  else if facet == `ilean then
-    return mod.facetTarget ileanFacet
-  else if facet == `olean then
-    return mod.facetTarget oleanFacet
-  else if facet == `c then
-    return mod.facetTarget cFacet
-  else if facet == `o then
-    return mod.facetTarget oFacet
-  else if facet == `dynlib then
-    return mod.facetTarget dynlibFacet
   else if let some config := ws.findModuleFacetConfig? facet then do
     let some target := config.toTarget? (mod.facet facet) rfl
       | throw <| CliError.nonTargetFacet "module" facet

Lake/CLI/Help.lean

@@ -73,31 +73,23 @@ A target is specified with a string of the form:
 The optional `@` and `+` markers can be used to disambiguate packages
 and modules from other kinds of targets (i.e., executables and libraries).
 
-PACKAGE FACETS:         build the package's ...
-  exe                   binary executable
-  leanLib               Lean library (*.olean and *.ilean files)
-  staticLib             static library
-  sharedLib             shared library
-
 LIBRARY FACETS:         build the library's ...
-  lean                  Lean binaries (*.olean and *.ilean files)
-  static                static binary
-  shared                shared binary
+  lean (default)        Lean binaries (*.olean and *.ilean files)
+  static                static binary (*.a file)
+  shared                shared binary (*.so, *.dll, or *.dylib file)
 
 MODULE FACETS:          build the module's ...
-  [default]             Lean binaries (*.olean and *.ilean files)
-  c                     *.c file
-  o                     *.o file (of the *.c file)
+  bin (default)         Lean binaries (*.olean and *.ilean files)
+  c                     C file produced by `lean`
+  o                     *.o object file (of its `lean.c` C file)
   dynlib                shared library (e.g., for `--load-dynlib`)
 
 TARGET EXAMPLES:        build the ...
   a                     default facet of target `a`
   @a                    default target(s) of package `a`
   +A                    olean and .ilean files of module `A`
   a/b                   default facet of target `b` of package `a`
-  a/+A:c                c file of module `A` of package `a`
-  @a:leanLib            lean library of package `a`
-  :exe                  root package's executable
+  a/+A:c           C file of module `A` of package `a`
 
 A bare `build` command will build the default facet of the root package.
 Package dependencies are not updated during a build."