diff --git a/flake.lock b/flake.lock index 53785fa847..a38dfabf8f 100644 --- a/flake.lock +++ b/flake.lock @@ -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" } } }, diff --git a/flake.nix b/flake.nix index 03ac3959ce..3f5cc51428 100644 --- a/flake.nix +++ b/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; diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index 57426d6af5..d722e597b3 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -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; }; }; diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix index d39b63d6f2..e4c5bcffc4 100644 --- a/nix/buildLeanPackage.nix +++ b/nix/buildLeanPackage.nix @@ -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\": \"\", \"text\": \"%s\"}\n", $0 }' diff --git a/nix/derivation.nix b/nix/derivation.nix deleted file mode 100644 index a723439204..0000000000 --- a/nix/derivation.nix +++ /dev/null @@ -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; - }; -} diff --git a/nix/lean-stage0/bin/lean b/nix/lean-stage0/bin/lean deleted file mode 100755 index 0c2dc28fdf..0000000000 --- a/nix/lean-stage0/bin/lean +++ /dev/null @@ -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 diff --git a/nix/nixpkgs.nix b/nix/nixpkgs.nix deleted file mode 100644 index f3c495028a..0000000000 --- a/nix/nixpkgs.nix +++ /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 ` - sha256 = "1z8fnqxi0zd3wmjnmc4l2s4nq812mx0h4r09zdqi5si2in6rksxs"; -}) {} diff --git a/shell.nix b/shell.nix index 1a65b9d616..a4346c1a35 100644 --- a/shell.nix +++ b/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 ]; + }; +}