sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore: Nix: comment out rarely used lean-stage0 input

Browse Source 
Optional inputs would be nice.
This commit is contained in:
Sebastian Ullrich
2022-11-14 13:12:07 +01:00
parent fea819bf3c
commit 6e34c89cbb
2 changed files with 9 additions and 25 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
flake.lock generated
View File

@@ -15,21 +15,6 @@
"type": "github"
}
},
"lean-stage0": {
"locked": {
"lastModified": 0,
"narHash": "sha256-3K/43lSW4WIHNG+HHVKCD1odS63mHuaQ4ueHyTIkcls=",
"owner": "leanprover",
"repo": "lean4",
"rev": "0000000000000000000000000000000000000000",
"type": "github"
},
"original": {
"owner": "leanprover",
"repo": "lean4",
"type": "github"
}
},
"lean4-mode": {
"flake": false,
"locked": {
@@ -133,7 +118,6 @@
"root": {
"inputs": {
"flake-utils": "flake-utils",
"lean-stage0": "lean-stage0",
"lean4-mode": "lean4-mode",
"nix": "nix",
"nixpkgs": "nixpkgs_2"

18
flake.nix
View File

@@ -9,15 +9,15 @@
flake = false;
};
# used *only* by `stage0-from-input` below
inputs.lean-stage0 = {
url = github:leanprover/lean4;
inputs.nixpkgs.follows = "nixpkgs";
inputs.flake-utils.follows = "flake-utils";
inputs.nix.follows = "nix";
inputs.lean4-mode.follows = "lean4-mode";
};
#inputs.lean-stage0 = {
# url = github:leanprover/lean4;
# inputs.nixpkgs.follows = "nixpkgs";
# inputs.flake-utils.follows = "flake-utils";
# inputs.nix.follows = "nix";
# inputs.lean4-mode.follows = "lean4-mode";
#};
outputs = { self, nixpkgs, flake-utils, nix, lean4-mode, lean-stage0 }: flake-utils.lib.eachDefaultSystem (system:
outputs = { self, nixpkgs, flake-utils, nix, lean4-mode, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
let
pkgs = import nixpkgs {
inherit system;
@@ -42,7 +42,7 @@
tsandebug = tsan.override { debug = true; };
stage0-from-input = lean-packages.override {
stage0 = pkgs.writeShellScriptBin "lean" ''
exec ${lean-stage0.packages.${system}.lean}/bin/lean -Dinterpreter.prefer_native=false "$@"
exec ${inputs.lean-stage0.packages.${system}.lean}/bin/lean -Dinterpreter.prefer_native=false "$@"
'';
};
inherit self;