lean4-htt/Lake/Config
tydeu a0626a9334 refactor: libDir -> nativeLibDir; oleanDir -> leanLibDir
also
* remove deprecated `isLeanOnly`
* touch-up some docs
2023-07-01 11:53:52 -04:00
..
Context.lean refactor: intro Lake.Env & add it to Workspace 2022-07-11 23:06:19 -04:00
Dependency.lean chore: move NameMap into a separate file 2022-09-14 21:32:25 -04:00
Env.lean chore: reduce imports in Lake.Build.Actions 2023-02-02 20:38:06 -05:00
ExternLib.lean fix: do not require Environment to be inhabited 2023-01-11 15:01:45 -05:00
ExternLibConfig.lean feat: recursive builds in extern_lib 2022-08-04 16:58:42 -04:00
FacetConfig.lean feat: show number of files to go when building 2023-04-18 20:58:40 -04:00
Glob.lean fix: do not build missing directory modules (+ test) 2023-06-29 17:42:27 -04:00
InstallPath.lean refactor: intro Lake.Env & add it to Workspace 2022-07-11 23:06:19 -04:00
LeanConfig.lean feat: add untraced weakLeanArgs 2023-06-08 03:29:51 -04:00
LeanExe.lean fix: do not require Environment to be inhabited 2023-01-11 15:01:45 -05:00
LeanExeConfig.lean feat: library-level module configuration 2022-06-26 20:35:23 -04:00
LeanLib.lean refactor: libDir -> nativeLibDir; oleanDir -> leanLibDir 2023-07-01 11:53:52 -04:00
LeanLibConfig.lean feat: library defaultFacets setting 2022-11-10 20:48:02 -05:00
Module.lean refactor: libDir -> nativeLibDir; oleanDir -> leanLibDir 2023-07-01 11:53:52 -04:00
Monad.lean feat: add some helpers for pkg and lib roots 2023-06-29 23:00:03 -04:00
Opaque.lean refactor: pattern TargetConfig off FacetConfig 2022-07-27 19:54:15 -04:00
Package.lean refactor: libDir -> nativeLibDir; oleanDir -> leanLibDir 2023-07-01 11:53:52 -04:00
Script.lean feat: bare lake run default scripts 2023-04-15 20:07:47 -04:00
TargetConfig.lean chore: remove dangerous instances 2023-04-15 18:16:53 -04:00
Workspace.lean refactor: libDir -> nativeLibDir; oleanDir -> leanLibDir 2023-07-01 11:53:52 -04:00
WorkspaceConfig.lean feat: -U to update & build; add packagesDir to manifest 2022-12-02 14:17:57 -05:00