Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
2610ace69d
In the Haskell proposal for top level mutable state https://wiki.haskell.org/Top_level_mutable_state, they describe the following problems with using the `IO` monad during initialization. "A more serious problem is that there is nothing to prevent arbitrary observable IO actions from appearing to the right of the arrow. If we perform all actions before executing main, then import becomes a side-effectful operation, rather than simply a way of bringing names into scope; furthermore we must specify the order in which actions from different modules are executed, which would appear to be difficult in general. If we execute actions on demand (as the unsafePerformIO hack does) then we are building an unsafe syntactic construct into the language." I believe this is not applicable to us. First, our imports are already side-effectful since we update attributes and the order we import modules already matters. Second, we have already a well-defined order in which we import modules. Finally, all global constants are already being initialized eagerly. Their ACIO proposal (`init_io` in our implementation) is too restrictive for what we want to do. For example, to implement an environment extension mechanism like we have discussed, we would also need `io.ref.write` and `io.ref.read`. I imagine, we would have a global table, and `register` would update this table. These extra actions do not satisfy the ACIO restrictions described in the Haskell proposal. From their document: "AC stands for Affine Central. An IO action u is affine if its effect is not indirectly observable, hence need not be performed if the result is unneeded. That is, if u >> v === v for all actions v. It is central if its effect commutes with every other IO action. That is, if do { x <- u; y <- v; w } === do { y <- v; x <- u; w } for all actions v and w." It feels like we would have to keep fighting with the ACIO restrictions. As I said above, our initialization order is well defined. So, we must document the `[init]` feature and tell users they should be aware that the `import` is important for initialization purposes, and that their initialization actions should be affine central whenever possible. |
||
|---|---|---|
| .github | ||
| bin | ||
| doc | ||
| gen | ||
| images | ||
| lean4-mode | ||
| library | ||
| script | ||
| src | ||
| tests | ||
| .appveyor.yml | ||
| .clang-format | ||
| .codecov.yml | ||
| .gitattributes | ||
| .gitignore | ||
| .travis.yml | ||
| LICENSE | ||
| README.md | ||
| License | Windows | Linux / macOS | Test Coverage | Chat |
|---|---|---|---|---|
 |
 |
 |
 |
About
- Homepage
- Theorem Proving in Lean
- Core library
- Change Log
- FAQ
- For HoTT mode, please use Lean2.
Installation
Stable and nightly binary releases of Lean are available on the homepage. For building Lean from source, see the build instructions.
Miscellaneous
- Building Doxygen Documentation:
doxygen src/Doxyfile - Coding Style
- Library Style Conventions
- Git Commit Conventions
- Automatic Builds
- Syntax Highlight Lean Code in LaTeX
- Exporting, and reference type-checkers