chore: Nix: rebase old shell.nix setup on new flake.nix one, add shell nix attribute for pinned flakes-enable Nix
This commit is contained in:
Sebastian Ullrich
parent
4d3d7cb4a6
commit
092d5d67b4
8 changed files with 102 additions and 78 deletions
70
flake.lock
generated
70
flake.lock
generated
|
|
@ -15,7 +15,57 @@
|
|||
"type": "github"
|
||||
}
|
||||
},
|
||||
"lowdown-src": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
"lastModified": 1598695561,
|
||||
"narHash": "sha256-gyH/5j+h/nWw0W8AcR2WKvNBUsiQ7QuxqSJNXAwV+8E=",
|
||||
"owner": "kristapsdz",
|
||||
"repo": "lowdown",
|
||||
"rev": "1705b4a26fbf065d9574dce47a94e8c7c79e052f",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "kristapsdz",
|
||||
"repo": "lowdown",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nix": {
|
||||
"inputs": {
|
||||
"lowdown-src": "lowdown-src",
|
||||
"nixpkgs": "nixpkgs"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1605624824,
|
||||
"narHash": "sha256-hJnqMzKKHjVrOTanOdb74kokOV/k5yFuQO2c2Jkm51A=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nix",
|
||||
"rev": "ae3191666f1828d9694fb615a721d409fb8582bd",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "NixOS",
|
||||
"repo": "nix",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs": {
|
||||
"locked": {
|
||||
"lastModified": 1602702596,
|
||||
"narHash": "sha256-fqJ4UgOb4ZUnCDIapDb4gCrtAah5Rnr2/At3IzMitig=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "ad0d20345219790533ebe06571f82ed6b034db31",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"id": "nixpkgs",
|
||||
"ref": "nixos-20.09-small",
|
||||
"type": "indirect"
|
||||
}
|
||||
},
|
||||
"nixpkgs_2": {
|
||||
"locked": {
|
||||
"lastModified": 1600913051,
|
||||
"narHash": "sha256-9PDPLwaZ/QzafO3M/yCeGWraI20fJNnGz7nzAfZsDes=",
|
||||
|
|
@ -34,7 +84,25 @@
|
|||
"root": {
|
||||
"inputs": {
|
||||
"flake-utils": "flake-utils",
|
||||
"nixpkgs": "nixpkgs"
|
||||
"nix": "nix",
|
||||
"nixpkgs": "nixpkgs_2",
|
||||
"temci": "temci"
|
||||
}
|
||||
},
|
||||
"temci": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
"lastModified": 1605533625,
|
||||
"narHash": "sha256-ndP2SzBX+/aupoZbWocQGefImSu+BN9zW7SYOFIP6AQ=",
|
||||
"owner": "parttimenerd",
|
||||
"repo": "temci",
|
||||
"rev": "e6936f61f11bd7a57078049dd6ba2b3cb2ce6e5a",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "parttimenerd",
|
||||
"repo": "temci",
|
||||
"type": "github"
|
||||
}
|
||||
}
|
||||
},
|
||||
|
|
|
|||
17
flake.nix
17
flake.nix
|
|
@ -3,10 +3,19 @@
|
|||
|
||||
inputs.nixpkgs.url = github:NixOS/nixpkgs/nixpkgs-unstable;
|
||||
inputs.flake-utils.url = github:numtide/flake-utils;
|
||||
inputs.temci = {
|
||||
url = github:parttimenerd/temci;
|
||||
flake = false;
|
||||
};
|
||||
inputs.nix.url = github:NixOS/nix;
|
||||
|
||||
outputs = { self, nixpkgs, flake-utils }: flake-utils.lib.eachDefaultSystem (system:
|
||||
outputs = { self, nixpkgs, flake-utils, temci, nix }: flake-utils.lib.eachDefaultSystem (system:
|
||||
with nixpkgs.legacyPackages.${system};
|
||||
let
|
||||
nix-pinned = writeScriptBin "nix" ''
|
||||
#!${bash}/bin/bash
|
||||
${nix.defaultPackage.${system}}/bin/nix --experimental-features 'nix-command flakes' $@
|
||||
'';
|
||||
cc = ccacheWrapper.override rec {
|
||||
cc = llvmPackages_10.clang.override {
|
||||
# linker go brrr
|
||||
|
|
@ -26,6 +35,7 @@
|
|||
buildLeanPackage = callPackage (import ./nix/buildLeanPackage.nix) {
|
||||
inherit (lean) stdenv lean leanc;
|
||||
inherit lean-emacs;
|
||||
nix = nix-pinned;
|
||||
};
|
||||
lean4-mode = emacsPackages.melpaBuild {
|
||||
pname = "lean4-mode";
|
||||
|
|
@ -41,8 +51,11 @@
|
|||
with epkgs; [ dash dash-functional f flycheck s ] ++ [ lean4-mode ]);
|
||||
in rec {
|
||||
packages = {
|
||||
inherit lean4-mode;
|
||||
inherit cc lean4-mode;
|
||||
lean = lean.stage1 // lean // { inherit buildLeanPackage; };
|
||||
temci = (import temci {}).override { doCheck = false; };
|
||||
nix = nix-pinned;
|
||||
nixpkgs = nixpkgs.legacyPackages.${system};
|
||||
} // lean.stage1.Lean;
|
||||
|
||||
defaultPackage = packages.lean;
|
||||
|
|
|
|||
|
|
@ -47,6 +47,7 @@ rec {
|
|||
desc = "stage${toString stage}";
|
||||
build = buildLeanPackage.override { lean = prevStage; lean-final = self; };
|
||||
in (all: all // all.lean) rec {
|
||||
inherit leancpp;
|
||||
Init = build { name = "Init"; src = ../src; srcDir = "/src"; deps = {}; };
|
||||
Std = build { name = "Std"; src = ../src; srcDir = "/src"; deps = { inherit Init; }; };
|
||||
Lean = build { name = "Lean"; src = ../src; srcDir = "/src"; deps = { inherit Init Std; }; };
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
{ debug ? false, stdenv, lib, coreutils, gnused, lean, leanc ? lean, lean-final ? lean, writeScriptBin, bash, lean-emacs }:
|
||||
{ debug ? false, stdenv, lib, coreutils, gnused, lean, leanc ? lean, lean-final ? lean, writeScriptBin, bash, lean-emacs, nix }:
|
||||
with builtins; let
|
||||
# "Init.Core" ~> "Init/Core.lean"
|
||||
modToLean = mod: replaceStrings ["."] ["/"] mod + ".lean";
|
||||
|
|
@ -107,6 +107,8 @@ in
|
|||
lean-dev = writeScriptBin "lean" ''
|
||||
#!${bash}/bin/bash
|
||||
set -euo pipefail
|
||||
PATH=${nix}/bin:$PATH
|
||||
|
||||
call() {
|
||||
if [[ $json == 1 ]]; then
|
||||
$@ 2>&1 | awk '/{/ { print $0; next } { gsub(/"/, "\\\"", $0); gsub(/\n/, "\\n", $0); printf "{\"severity\": \"warning\", \"pos_line\": 0, \"pos_col\": 0, \"file_name\": \"<stdin>\", \"text\": \"%s\"}\n", $0 }'
|
||||
|
|
|
|||
|
|
@ -1,25 +0,0 @@
|
|||
{ llvmPackages, bash, cmake, ccache, python, gmp }:
|
||||
|
||||
let gmp-static = gmp.override { withStatic = true; };
|
||||
in llvmPackages.stdenv.mkDerivation rec {
|
||||
name = "lean-${version}";
|
||||
version = "local";
|
||||
|
||||
# I have way too many untracked files in my checkout
|
||||
src = if builtins.pathExists ../.git then builtins.fetchGit { url = ../.; } else ../.;
|
||||
|
||||
nativeBuildInputs = [ bash cmake python ];
|
||||
buildInputs = [ gmp-static llvmPackages.llvm ];
|
||||
enableParallelBuilding = true;
|
||||
|
||||
preConfigure = ''
|
||||
patchShebangs stage0/src/bin src/bin
|
||||
'';
|
||||
|
||||
meta = with llvmPackages.stdenv.lib; {
|
||||
description = "Automatic and interactive theorem prover";
|
||||
homepage = https://leanprover.github.io/;
|
||||
license = licenses.asl20;
|
||||
platforms = platforms.unix;
|
||||
};
|
||||
}
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
#!/usr/bin/env bash
|
||||
set -euo pipefail
|
||||
|
||||
root="$(realpath "$(dirname "$0")")/../../.."
|
||||
input="${@: -1}"
|
||||
input="$(realpath --relative-to="$root/src" "$input")"
|
||||
input="${input%.lean}"
|
||||
input="${input//\//.}"
|
||||
nix develop "$root#lean.stdlib.mods.\"$input\"" -c lean $@ 2> /dev/null
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
import (builtins.fetchTarball {
|
||||
name = "nixpkgs-unstable-2020-04-08";
|
||||
# Commit hash from `git ls-remote https://github.com/NixOS/nixpkgs-channels nixpkgs-unstable`
|
||||
url = https://github.com/nixos/nixpkgs/archive/3b4df94aeb6e215085d08e3d5b0edc1313b9f584.tar.gz;
|
||||
# Hash obtained using `nix-prefetch-url --unpack <url>`
|
||||
sha256 = "1z8fnqxi0zd3wmjnmc4l2s4nq812mx0h4r09zdqi5si2in6rksxs";
|
||||
}) {}
|
||||
47
shell.nix
47
shell.nix
|
|
@ -1,38 +1,19 @@
|
|||
{ pkgs ? import ./nix/nixpkgs.nix, llvmPackages ? pkgs.llvmPackages_latest } @ args:
|
||||
|
||||
let attribs = rec {
|
||||
lean = import ./default.nix args;
|
||||
temci = (import (builtins.fetchGit { url = http://github.com/parttimenerd/temci.git; rev = "c972086f4af2c98d8b815441cfb305f608f3cee9"; }) {}).override {
|
||||
doCheck = false;
|
||||
};
|
||||
lean4-mode = pkgs.emacsPackages.melpaBuild {
|
||||
pname = "lean4-mode";
|
||||
version = "1";
|
||||
src = ./lean4-mode;
|
||||
packageRequires = with pkgs.emacsPackages.melpaPackages; [ dash dash-functional f flycheck s ];
|
||||
propagatedUserEnvPkgs = [ lean ];
|
||||
recipe = pkgs.writeText "recipe" ''
|
||||
(lean4-mode :repo "leanprover/lean4" :fetcher github :files ("*.el"))
|
||||
'';
|
||||
fileSpecs = [ "*.el" ];
|
||||
};
|
||||
emacs = pkgs.emacsWithPackages (epkgs:
|
||||
# ???
|
||||
with pkgs.emacsPackages.melpaPackages; [ dash dash-functional f flycheck s ] ++ [ lean4-mode ]);
|
||||
run-emacs = pkgs.mkShell {
|
||||
shellHook = ''
|
||||
${emacs}/bin/emacs
|
||||
exit 0
|
||||
'';
|
||||
};
|
||||
shell = pkgs.mkShell.override { stdenv = lean.stdenv; } rec {
|
||||
inputsFrom = [ lean ];
|
||||
buildInputs = with pkgs; [ temci ccache mdbook ];
|
||||
let
|
||||
flakePkgs = (import ./default.nix).packages.${builtins.currentSystem};
|
||||
pkgs = flakePkgs.nixpkgs;
|
||||
in
|
||||
# use `shell` as default
|
||||
(attribs: attribs.shell // attribs) rec {
|
||||
inherit (flakePkgs) temci;
|
||||
shell = pkgs.mkShell.override { stdenv = pkgs.overrideCC pkgs.stdenv (flakePkgs.cc.override { extraConfig = ""; }); } rec {
|
||||
inputsFrom = [ flakePkgs.lean.leancpp ];
|
||||
buildInputs = with pkgs; [ temci ccache ];
|
||||
# https://github.com/NixOS/nixpkgs/issues/60919
|
||||
hardeningDisable = [ "all" ];
|
||||
# more convenient `ctest` output
|
||||
CTEST_OUTPUT_ON_FAILURE = 1;
|
||||
};
|
||||
};
|
||||
# use `shell` as default
|
||||
in attribs.shell // attribs
|
||||
nix = pkgs.mkShell {
|
||||
buildInputs = [ flakePkgs.nix ];
|
||||
};
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue