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

chore: remove Lake flake

Browse source 
Fixes leanprover/lake#165
This commit is contained in:
Sebastian Ullrich 2023-07-19 13:18:09 +02:00
parent 8999ef067b
commit e2fbfb5731
3 changed files with 1 additions and 66 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/lake/.envrc
View file

@ -1 +0,0 @@
use flake

10
src/lake/README.md
View file

@ -360,15 +360,7 @@ After building, the `lake` binary will be located at `build/bin/lake` and the li
### Building with Nix Flakes
It is also possible to build Lake with the Nix setup `buildLeanPackage` from the [`lean4`](https://github.com/leanprover/lean4) repository. To do so, you need to have Nix installed with flakes enabled. It is recommended to also set up the Lean 4 binary cache as described in the Lean 4 repository.
It is then possible to build Lake with `nix build .` or run it from anywhere with `nix run github:leanprover/lake`.
A development environment with Lean 4 installed can be loaded automatically by running `nix develop` or automatically on `cd` with `direnv` by running `direnv allow`.
The versions of `nixpkgs` and `lean4` are fixed to specific hashes. They can be updated by running `nix flake update`.
Thank Anders Christiansen Sørby ([@Anderssorby](https://github.com/Anderssorby)) for this support!
Lake is built as part of the main Lean 4 flake at the repository root.
### Augmenting Lake's Search Path

56
src/lake/flake.nix
View file

@ -1,56 +0,0 @@
{
description = "Lake (Lean Make) is a new build system and package manager for Lean 4.";
inputs = {
nixpkgs.url = "github:nixos/nixpkgs/nixos-21.05";
lean = {
url = "github:leanprover/lean4";
};
flake-utils = {
url = "github:numtide/flake-utils";
inputs.nixpkgs.follows = "nixpkgs";
};
};
outputs =
{ self
, flake-utils
, nixpkgs
, lean
}:
flake-utils.lib.eachDefaultSystem (system:
let
pkgs = import nixpkgs { inherit system; };
packageName = "Lake";
src = ./.;
leanPkgs = lean.packages.${system};
project = leanPkgs.buildLeanPackage {
name = packageName;
inherit src;
};
cli = leanPkgs.buildLeanPackage {
name = "Lake.Main";
executableName = "lake";
deps = [ project ];
linkFlags = pkgs.lib.optional pkgs.stdenv.isLinux "-rdynamic";
inherit src;
};
in
{
packages = project // {
inherit (leanPkgs) lean;
cli = cli.executable;
};
defaultPackage = self.packages.${system}.cli;
apps.lake = flake-utils.lib.mkApp {
drv = cli.executable;
};
defaultApp = self.apps.${system}.lake;
inherit (project) devShell;
});
}