v4.1.0-merge

The final v4.1.0-pre release before Lake's merge into the Lean core.

v4.0.0

Lake v4.0.0 has mixture of programmatic improvements and new features. It also removes all previously deprecated settings. The biggest highlights are cloud build support and custom facets. It also completely revamps Lake's build API to make it more powerful (and hopefully easier to use in the long run).

Highlights

Cloud Build Support: Lake now supports uploading build artifacts to a GitHub release and automatically downloading said artifacts for a package. This way end users do not have build releases from the source themselves, which can save a lot of time. See the GitHub Release Builds section of the README for more details.

Custom Package, Module, and Library Facets: Custom package and module facets are now officially released and have been joined by the new addition of library facets. Once defined, the new facet (e.g., foo) can be built on any current or future object of its type (e.g., through lake build pkg:foo for a package facet). See the Defining New Facets section of the README for details on the syntax.

Build API Overhaul: The API for builds has undergone a complete revamp, eliminating the old notion of Target/ActiveTarget. Instead, builds are invoked directly (e.g., staticLibTarget is replaced by buildStaticLib). In addition, it is now much easier to invoke the build of one target / facet from another target / facet. As a result of this change, all previous extern_lib functions are broken. Take a look at the updated ffi example for pointers on how to migrate.

Better Logging: Thanks to Mario (#108), Lake now has -q/--quiet and -v/-verbose toggles to control how much information it logs. Its default now longer logs every command invocation but instead provides simple one-line progress reports (e.g., Building Foo).

Improved Dependency Resolution: The dependency resolution procedure has been dramatically improved. Lake will now attempt to use the version of a package listed in a dependency manifest for deeply nested dependencies (#70) and if conflicts emerge try to pick a version that will satisfy everyone (e.g., the latest version for the shared input revision). Lake will also log the dependencies it encounters during resolution on a lake update or when -v is used. It will also issue a warning if the input revision in the root lakefile and manifest differ (#85).

--old Option: Lake now supports the --old option to avoid rebuilding intermediate imports / dependencies of modules unless their source files themselves have changed (#44).

Removals: All deprecated features have been removed. This means builtin package targets (i.e., targets that were part of the package statement and set via e.g., libRoots) have been removed. extraDepTarget has also been replaced with the new extraDepTargets, which is a list of target names the package should build before anything else.

Full Commit Log

• b899c0a release: 4.0.0
• e1d43a7 fix: improve targets/facets UX (e.g., errors when type incorrect)
• 26be594 doc: update README and some comments
• 1ed9913 chore: bump Lean version
• 4fe15f6 chore: bump Lake version
• 15a6401 feat: make manifest file configurable
• 35873c6 feat: replace extraDepTarget with extraDepTargets
• 0d4013a test: make test 44 more consistent
• 1bd8430 refactor: split CLI actions into separate file
• 63f575b feat: ws.runBuild
• 967c01a feat: facet info param + unique names for facet syntax
• 7ee2f76 refactor: move fetching releases to extraDep build
• 884e166 refactor: renames + cleanup
• 40927d8 feat: recursive builds in extern_lib
• d7b2dcf chore: test 44 shell script fixes
• de3daae ci: add diffutils to Windows MSYS2 setup
• db0f16c feat: --old to use outdated unchanged modules
• 1c1daf2 refactor: remove remainder of Target code
• 5c2c513 doc: correct require syntax docs
• 757ed04 refactor: cleanup (primarily resolve code)
• bd44264 fix: pass pkg linking args to extern lib linking
• 79321cd refactor: cleanup logging API (unify BuildIO with LogIO)
• ca87bef feat: platform bits in build archive name + related cleanup
• 6b6cc7f feat: inherit deep desp's revision from dep's manifest
• 9662b6c feat: store config rev in manifest and warn on change
• c6606ed chore: correctly mark version as prerelease
• e3e17ad feat: cloud build support
• ae629af feat: verbosity options for logging + neater build progress
• 8c623a3 refactor: Lake.Build.Topological tweaks + docs
• 8322e8d refactor: pattern TargetConfig off FacetConfig
• 430ac1d refactor: replace ActiveTarget with Job
• 93693d7 chore: fix targets example
• bfa94d5 refactor: reduce use of targets + IndexT cleanup
• f1d9921 refactor: remove many used Target methods
• f8b7eeb fix: apply nameToSharedLib to modTargets too
• 8ed9bc6 refactor: move info into target task
• 34f7937 refactor: remove facet target helpers
• cae36dc chore: cleanup at recBuildExternalDynlibs
• e134863 feat: library facets
• fa3c7e2 feat: build all CLI targets in the same build pass
• 21991dd refactor: remove module facet special casing
• 2bc1778 chore: remove package config builtin targets
• 8037b9a chore: start next Lake version

v3.2.2

This is minor release that mostly includes bug fixes (#102, #104) and quality of life improvements (#60, #82, #88).

The highlights are lake exe <target> <args> (#82) to build and run executable targets in a single command, lake run and lake scripts as shorthand for lake script run and lake script list (#88), get_config? and -K for key-value command line Lake options, and meta if for conditional configurations (#80).

It also includes a number of internal refactors to set up bigger features in the future, and removes a build bottleneck in Lake.Build.Index.

Full Commit History

dcf8e1f release: 3.2.2
623bbba chore: bump Lean version
5401769 ci: don't skip after successful duplicate
0704277 feat: support pkg/ to disambiguate packages
05e770b refactor: merge IndexTargets into Index
dda1afc chore: try to fix meta test script on macOS
d8939b2 feat: add do helper for grouping cmds + meta test
6cb33dc feat: add meta if helper command for config switchs
2de99f7 refactor: make LeanLib.buildModules a proper recursive build
e83c150 docs: touch-up of Lake.Util.Family comments
e6a6715 refactor: simplify FacetConifg and build monads ala #107
0ca66ed refactor: move mod/pkg facets from pkg to ws
6eb081d chore: convert doc/mod comments from /- to /--//-!
ef4f3f1 feat: resolve depss while loading a pkg
aaaee4d doc: mention types of root(s)/lib/exeName in README
a7bc6ad refactor: split config elab into its own file
3454c01 refactor: move all manifest code to its file + split Package.load
c625851 refactor: move config loading code into its own directory
c401fb8 test: try to fix sed script for test 104 for MacOS
398a9e7 fix: do not fetch if dep rev matches manifest
8621324 refactor: add LawfulCmpEq + post-PR cleanup
9156ae6 chore: update Lean version
372e00b chore: hash field in Name was dropped
a582b4a doc: add trace to glossary + cleanup
267ffd1 doc: add glossary of Lake terminology to README
0d39b1e refactor: intro Lake.Env & add it to Workspace
ff619a3 fix: Glob.forEachModuleIn
d102a09 fix: flake.nix
27ae158 chore: update Lean version
c326f43 fix: restore script arg syntax
a4764ed chore: adapt to simpleBinder removal
78d1075 chore: the for in elaborator now propagates the element type to the body
2e205f9 feat: lake exe CLI to run workspace exes
53be27a chore: skip elan test if no elan found
9a4a987 chore: remove redundant declaration in .envrc
e7f85ea chore: update flake.nix
080cda1 feat: add shorthands for lake script run/list
505104c refactor: reorg cli code some (e.g., split cmds into defs)
7e9014e feat: replace __args__ with get_config? + related refactors
5b9194d misc: hoist facet name check to load + related bugfixes/refactors
dc19606 chore: start next Lake version

v3.2.1

A patch for v3.2.0. See its release notes for details on the big changes in v3.2.x.

This patch fixes bugs with lake update (#94) and precompileModules (#93) and refactors getLeanEnv to getAugmentedEnv which augments rather than overwrites environment variable search paths (#91).

Full Commit Log

• b651e87 release: 3.2.1
• 37b5225 chore: bump Lean version
• f102db6 feat: setup lean/lake env for server even if config has errors
• f99c4b4 feat: add module file path helpers
• a9dcdab refactor: LeanExe.facet -> exeFacet
• c4b1b93 fix: properly update deps w/ no branch or dir but no manifest
• 53513da fix: don't set LEAN_CC unless necessary + detect src dirs
• 21f83e3 fix: linking libraries on Unix
• 3a20f2b feat: augment server env + add dynlib search path
• 2987a61 fix: parameterize CustomData by package and target name
• 795d825 refactor: DynamicType -> FamilyDef
• ddf3655 chore: bump Lean version
• 9189b42 chore: start next Lake version
• 2987d36 chore: String.getOp has been removed
• 34cdc7c test: use -fPIC in ffi example
• 8438858 chore: don't use ../$LAKE idiom

v3.2.0

Whereas Lake v3.1.x had highly visible UI/UX changes, most of the v3.2.0 changes are internal. However, these internal changes allow for some cool new features, including precompileModules and the experimental custom targets and module and package facets.

Highlights

Precompile Modules: The major headline feature for this release is the precompileModules package and library setting. With this flag turned on, Lake will build a native shared library for each import of a module and load it into lean via --load-dynlib. This speeds up the evaluation of metaprograms and enables the interpreter to run functions marked @[extern].

Feature Preview of Custom Targets & Module & Package Facets: Also included in this release are the beta preview versions of custom targets and package and module facets. These features are currently unstable, as is any use of the current build / target API, as it is expected to change drastically in upcoming releases. Only custom targets are presently documented, as they serve as a potential replacement for extraDepTarget, which has been deprecated.

Deprecation of extraDepTarget: None of Lake's examples or tests presently use extraDepTarget and the Lake's internal target API has never truly been documented, so its precise functionality is not nailed down. This makes it difficult to know exactly how it is being used and what its replacement needs to support. Thus, a deprecation warning has been added on its use to notify users of the plan to remove it and motivate them to specify what features they would like to see in its replacement.

Package Configuration Templates: lake init and lake new now allow the user to specify a template to follow (e.g., lake new <package-name> <template>) in initializing the package. Current options are std (the original template -- library plus executable), lib (just a library), exe (just an executable), and math (a library with a mathlib dependency).

Removals: The deprecated PackageConfig.moreLibTargets, PackageConfig.dependencies, Packager, IOPackager, PackageFacet.oleans, and PackageFacet.bin have been removed.

Notable Issues / PRs Addressed

• #47 feat: precompileModules
• #74 Files are compiled twice when compiled
• #75 Rebuild fails after module is rebuilt without .c while old .c remains
• #76 lake serve fails when lakefile.lean doesn't compile
• #84 lake update doesn't update

Full Commit Log

• 6c495e8 refactor: remove dead package DSL code
• 1929d4a chore: bump Lean version
• 077e6ac doc: update README
• 4ffd3ff refactor: simplify custom target API (for now)
• a4a9025 chore: remove some deprecated features + deprecate extraDepTarget
• a05deb9 chore: fix wording
• 1a2550f feat: add build types (e.g., debug, release)
• 8c267a8 fix: keyName regression caused by refactor
• ab8098b feat: inductive BuildKey + proper custom targets
• a71edb0 refactor: remove unnecesssary build key subtypes
• cc2104a fix: properly trace module imports
• 80bd8b7 feat: preliminary custom package facets
• 1c8c019 feat: preliminary custom targets
• b80b32e chore: update Lean version + adapt to TSyntax
• 175793d feat: use nativeFacets in exe's recBuild
• d15f8fd fix: make root module "private" to the package
• 1501702 fix: dummy git identity in test to make runner happy
• a34343d fix: properly update git packages specified by branch
• 8f50916 refactor: typify git repos + log stdout/stderr on git failures
• 24b9dd9 fix: build o files again to enable incremental rebuilds
• 26c49fa fix: precompile imports of precompiled imports
• 88dc993 fix: use Lake install's olean files over LEAN_PATH
• d0896b3 fix: use library, not package, for lean root dir
• d23660c feat: user-specified native module facets for libraries
• aa10cea feat: preliminary custom module facets
• b082443 chore: add note highlighting perf decision
• 182a578 perf: do not build object files of imports when linking executable
• afc25a9 refactor: minor cleanup
• e89c16b refactor: build code cleanup / reorg
• 696e46d refactor: move lib/exe targets into the index
• d169be0 feat: library-level module configuration
• e4930e0 refactor: add LeanLib/LeanExe/ExternLib + reorg & cleanup
• ac87b53 fix: properly link libraries on MacOS
• 99f96f3 feat: link libraries in a path and platform independent way
• ff1f2c6 test: "fix" library loading issues
• 32f0dbe feat: include external libraries in precompilation
• 7f018f2 feat: add isLeanOnly package config
• 344da08 fix: report precompiled dynlibs to server
• 44d5610 refactor: use IndexT at Index.lean
• 5b502ec refactor: move recurse arg into the monad stack
• cc23002 fix: precompile mods if they want not if their importer wants
• b82b2ff test: expand precompile example to test #83
• 13930f2 refactor: reorg build code into smaller, focused files
• f4c604b refactor: generalize module facet build code to any target
• 23938ed feat: basic precompiled modules + builtin module facets
• 12e2463 chore: update Lean version
• 8eb2236 chore: adapt to where syntax change
• 521d064 ci: skip duplicate/unnecessary jobs
• 9270c2d chore: remove lean-toolchain from version agnostic tests
• 2256c95 chore: update Lean version
• 6730fa5 chore: replace constant with opaque
• a3dc5dd chore: opaque is now a command keyword
• 2eb0f03 chore: fix test
• bfdf1ae test: add test for #75
• 3952331 refactor: simplify module target code + related cleanup
• 204ee22 chore: use bash shebang in test scripts
• 71f1e9a chore: fix new shell scripts' premissions
• bc559a0 test: reorg + regression tests
• c0f89d5 fix: don't require know expected type for __dir__/__args__
• f26dbe1 fix: lake serve fallback regression
• ce2570c chore: update Lean version
• 7d59f02 feat: different package templates

v3.1.1

A hot fix for v3.1.0. See that release's notes instead.

e0238e5 feat: rev opt in git dep + fix path opt in require

v3.1.0

The headline feature for this release is the ability to add multiple different Lean library and executable targets to a package using the new lean_lib and lean_exe syntax. Other new syntax has also been introduced: for specifying dependencies (require), defining external library targets (extern_lib replacing moreLibTargets), and getting the directory and arguments of a package (__dir__ and __args__). Deprecation warnings have been adding to the now outdated approaches the syntax replaces.

The revision of resolved (Git) package dependencies are also now saved to a manifest.json file in the packages directory (by default, lean_packages). This makes it easy for Lake to reproduce the exact set of dependencies (e.g., for CI, see #59) when the revision specified in the Lake configuration file is vague (e.g., a branch like master). As part of this change, lake build no longer updates dependencies (it does still clone them). To update them, use the new lake update (which has replaced lake configure).

See the updated Lake README for details on the new setup.

Details

Full List of Deprecations

• The dependencies field of package has been deprecated in favor of the new require syntax.
• The package (dir) (args) form of the package syntax has been deprecated in favor of __dir__ and __args__ macros for accessing the package directory and configuration arguments (see the FFI example for a demonstration of the use of __dir__). These macros make it possible to access this data from other targets (e.g., extern_lib declarations).
• The use of IO in package declarations has been deprecated. The behavior can generally be replaced with metaprogramming, making the need for such a form superfluous. Raise an issue on the Lake repository if you have a use case that really needed this feature.
• The moreLibTargets package configuration has been deprecated in favor of the new extern_lib syntax. Currently, the order of the libraries defined by extern_lib is undefined, which may cause linking issues if a particular order is required. Raise an issue on the Lake repository if you need this addressed quickly.
• Package facets have been deprecated (e.g., libRoots, libName, binRoot, binName, defaultFacet, etc.). Instead, define the library and executable targets for a package via the new lean_lib and lean_exe syntax. Lake will produce a deprecation warning if no such targets exist (as that is its best proxy for the use of this feature). if you want to silence this warning (because your package doesn't need targets for some reason), you can set the defaultFacet to the new value none to disable it.

Other Minor Changes

• lake serve now prints all output to stderr (#72, #71)
• The binary trace now includes the Lean version (#62) and the module trace includes moreLeanArgs (#50)
• Various performance improvements (c.f., #64, #65, #66, #71)

Complete Commit History

a369f0c doc: update defaultFacet description
90c5cd7 chore: silence some "unused variable" warnings
4eeaf3b test: make git example clone local repo
4d90870 doc: update w/ extern_lib + some cleanup
6ab6051 feat: allow @[defaultTarget] extern_lib
320b691 feat: extend DSL syntax and improve docs
6dfb980 chore: bump Lean version
d781892 feat: replace moreLibTargets w/ new extern_lib syntax
d731214 chore: improve imports lean-only build condition
3aa2a8c doc: fix heading
b482019 feat: trim log messages + simplify MonadLog
287a523 fix: delete duplicate improperly case Ffi.lean
c37362b feat: none package facet to avoid warnings in scripts example
71455c8 doc: update with new features + other cleanup
be45aa9 chore: deprecate package facets
3272068 feat: packages names don't eat up an identifier
d4c630e feat: attr to mark targets as package defaults
b276fb8 chore: warnings on deprecated features
b90f018 fix: another casing error in targets test
3deeaab fix: casing in targets test
0d0bee4 refactor: preserve case in exe root default
4376d86 fix: include submodules at hasModule + test
e26a040 feat: syntax for defining extra lib & exe targets
76c30b7 fix: properly catch CLI errors
0de8d7c fix: exe link args & targets test
82c0823 feat: multi lib & exe targets w/ updated build CLI syntax
43140c9 refactor: split lib and exe config from package
e3e55e6 refactor: MainM code cleanup
12d5155 refactor: split up DSL.Commands
4bbdcc5 feat: __dir__/__args__ syntax for config settings
94847d1 refactor: merge MonadLog and LogMethods
d763d3d refactor: some CLI code cleanup
cb287e3 feat: caption process stdout and stderr
775bb7f feat: new require syntax for package deps
cb0eab4 refactor: cleanup runFrontend
e2e6c94 perf: cache imported environment
a04e5a6 feat: retool configure into update
1a707e6 feat: only update deps in configure + don't ignore manifest.json
609c922 fix: only write manifest if a package was resolved
d231aae feat: save resolved packages in a manifest
463c4f0 fix: include moreLeanArgs in module trace
3595a56 fix: include Lean version in binary trace

v3.0.1

A few minor bug fixes and performance improvements plus some code maintenance to update Lake to the latest Lean (i.e., nightly 05-16-2022).

v3.0.0

The first official release of Lake since it has been bundled with Lean.

Includes a wide swath of changes since the last official release. With some key highlights the default configuration file being renamed lakefile.lean, a DSL syntax for said configuration file, CLI changes (e.g., adding lake env and lake serve, renaming lake run to lake script run, etc.), and a large number of API refactors (which are too numerous to list here).

v2.1.0

A minor release to get Lake in shape so it can be bundled with Lean.

The most significant changes are Lake's new use of a lean-toolchain file to specify the Lean toolchain of package for elan and the split of Packager into two: a pure (the new Packager) and an impure (renamed IOPackager) version.