Sebastian Ullrich
Sebastian Ullrich
We should add back the Lean 3 behavior of writing the Lean binary's commit hash into each .olean file and checking against it on load, optionally omitting the check during...
This is taken literally from helm-lsp
In contrast to the install script, tarballs can be sourced directly from Hydra: https://github.com/leanprover/lean4/blob/e8b58abffcf2eadc436435cf6e6733827d818ed6/.github/workflows/nix-ci.yml#L34-L44
Suggested plan: * Inject a `leanpkg lean-upgrade ` command into `leanpkg` (i.e. it will only be available when calling `~/.elan/bin/leanpkg`). This is not just a convenience command for editing the...
We should copy stack's [script command](https://docs.haskellstack.org/en/stable/GUIDE/#script-interpreter) to extend isolation to standalone files and gists.
The rustup.rs source code provided a perfect starting point, but there are lots of places where we can remove or simplify code for our needs.
See https://github.com/Kha/elan/issues/20
In a file I get ``` `/home/sebastian/.elan/toolchains/leanprover--lean4---nightly-2022-08-10/bin/lake print-paths Init` failed: stderr: Error parsing '././lakefile.lean'. Please restart the lean server after fixing the Lake configuration file. ``` but going back to...
**Describe the bug** Given the following flake ```nix { description = "A very basic flake"; inputs.flake-utils.url = github:numtide/flake-utils; outputs = { self, nixpkgs, flake-utils }: flake-utils.lib.eachDefaultSystem (system: with nixpkgs.legacyPackages.${system}; {...
...while go-to-declaration should go to the typeclass as it does right now. I hope that's not too controversial (and may even have been suggested before)? Note that you can still...