max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: tweak README + fix some typos

Browse source
This commit is contained in:
tydeu 2023-04-15 18:32:21 -04:00
parent caa4494cb7
commit 227a350747
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
README.md
View file

@ -105,7 +105,7 @@ Examples of different package configurations can be found in the [`examples`](ex
## Glossary of Terms
Lake uses a lot of terms common in software development -- like workspace, package, library, executable, target, etc. -- and some more esoteric onces -- like facet. However, whether common or not these terms mean different things to different people, so it is important to elucidiate how Lake defines these terms:
Lake uses a lot of terms common in software development -- like workspace, package, library, executable, target, etc. -- and some more esoteric ones -- like facet. However, whether common or not, these terms mean different things to different people, so it is important to elucidate how Lake defines these terms:
* A **package** is the **fundamental unit of code distribution in Lake**. Packages can be sourced from the local file system or downloaded from the web (e.g., via Git). The `package` declaration in package's lakefile names it and [defines its basic properties](#package-configuration-options).
@ -139,9 +139,9 @@ Lake provides a large assortment of configuration options for packages.
* `manifestFile`: The path of a package's manifest file, which stores the exact versions of its resolved dependencies. Defaults to `lake-manifest.json`.
* `srcDir`: The directory containing the package's Lean source files. Defaults to the package's directory. (This will be passed to `lean` as the `-R` option.)
* `buildDir`: The directory to which Lake should output the package's build results. Defaults to `build`.
* `oleanDir`: The build subdirectory to which Lake should output the package's `.olean` files. Defaults to `lib`.
* `irDir`: The build subdirectory to which Lake should output the package's intermediary results (e.g., `.c` and `.o` files). Defaults to `ir`.
* `libDir`: The build subdirectory to which Lake should output the package's libraries. Defaults to `lib`.
* `oleanDir`: The build subdirectory to which Lake should output the package's binary Lean libraries (i.e., `.olean`, `.ilean` files). Defaults to `lib`.
* `irDir`: The build subdirectory to which Lake should output the package's intermediary results (e.g., `.c`, `.o` files). Defaults to `ir`.
* `libDir`: The build subdirectory to which Lake should output the package's native libraries (e.g., `.a`, `.so`, `.dll` files). Defaults to `lib`.
* `binDir`: The build subdirectory to which Lake should output the package's binary executables. Defaults to `bin`.
### Build & Run