vfox plugin for Lean 4 theorem prover and programming language.
mise supports vfox plugins as a backend.
Install the latest version globally:
mise use -g vfox:edlontech/vfox-leanInstall a specific version in the current project:
mise use vfox:edlontech/vfox-lean@4.27.0This records the version in your mise.toml:
[tools]
"vfox:edlontech/vfox-lean" = "4.27.0"vfox add lean
vfox install lean@4.27.0
vfox use lean@4.27.0This plugin reads lean-toolchain files, the same format used by elan. All of these formats are supported:
leanprover/lean4:v4.27.0
leanprover/lean4:4.27.0
v4.27.0
4.27.0
With mise, place a lean-toolchain file in your project and it will be picked up automatically.
The plugin sets the following environment variables:
| Variable | Value |
|---|---|
PATH |
<install-dir>/shims is prepended |
LEAN_HOME |
Set to the installation directory |
| OS | x86_64 | aarch64 |
|---|---|---|
| Linux | yes | yes |
| macOS | yes | yes |
| Windows | yes | no |
Apache-2.0