diff --git a/.github/workflows/nix-ci.yml b/.github/workflows/nix-ci.yml index 69d038b8d3..9db7eea053 100644 --- a/.github/workflows/nix-ci.yml +++ b/.github/workflows/nix-ci.yml @@ -103,7 +103,7 @@ jobs: continue-on-error: true - name: Build manual run: | - nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test,inked} -o push-doc + nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,inked} -o push-doc nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc # https://github.com/netlify/cli/issues/1809 cp -r --dereference ./result ./dist @@ -146,5 +146,3 @@ jobs: - name: Fixup CCache Cache run: | sudo chown -R $USER /nix/var/cache - - name: CCache stats - run: CCACHE_DIR=/nix/var/cache/ccache nix run .#nixpkgs.ccache -- -s diff --git a/doc/flake.lock b/doc/flake.lock index 9a791f73a1..da279454f6 100644 --- a/doc/flake.lock +++ b/doc/flake.lock @@ -18,12 +18,15 @@ } }, "flake-utils": { + "inputs": { + "systems": "systems" + }, "locked": { - "lastModified": 1656928814, - "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=", + "lastModified": 1710146030, + "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", "owner": "numtide", "repo": "flake-utils", - "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249", + "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", "type": "github" }, "original": { @@ -35,13 +38,12 @@ "lean": { "inputs": { "flake-utils": "flake-utils", - "lean4-mode": "lean4-mode", - "nix": "nix", - "nixpkgs": "nixpkgs_2" + "nixpkgs": "nixpkgs", + "nixpkgs-old": "nixpkgs-old" }, "locked": { "lastModified": 0, - "narHash": "sha256-YnYbmG0oou1Q/GE4JbMNb8/yqUVXBPIvcdQQJHBqtPk=", + "narHash": "sha256-saRAtQ6VautVXKDw1XH35qwP0KEBKTKZbg/TRa4N9Vw=", "path": "../.", "type": "path" }, @@ -50,22 +52,6 @@ "type": "path" } }, - "lean4-mode": { - "flake": false, - "locked": { - "lastModified": 1659020985, - "narHash": "sha256-+dRaXB7uvN/weSZiKcfSKWhcdJVNg9Vg8k0pJkDNjpc=", - "owner": "leanprover", - "repo": "lean4-mode", - "rev": "37d5c99b7b29c80ab78321edd6773200deb0bca6", - "type": "github" - }, - "original": { - "owner": "leanprover", - "repo": "lean4-mode", - "type": "github" - } - }, "leanInk": { "flake": false, "locked": { @@ -83,22 +69,6 @@ "type": "github" } }, - "lowdown-src": { - "flake": false, - "locked": { - "lastModified": 1633514407, - "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=", - "owner": "kristapsdz", - "repo": "lowdown", - "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8", - "type": "github" - }, - "original": { - "owner": "kristapsdz", - "repo": "lowdown", - "type": "github" - } - }, "mdBook": { "flake": false, "locked": { @@ -115,65 +85,13 @@ "type": "github" } }, - "nix": { - "inputs": { - "lowdown-src": "lowdown-src", - "nixpkgs": "nixpkgs", - "nixpkgs-regression": "nixpkgs-regression" - }, - "locked": { - "lastModified": 1657097207, - "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=", - "owner": "NixOS", - "repo": "nix", - "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f", - "type": "github" - }, - "original": { - "owner": "NixOS", - "repo": "nix", - "type": "github" - } - }, "nixpkgs": { "locked": { - "lastModified": 1653988320, - "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=", + "lastModified": 1710889954, + "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1", - "type": "github" - }, - "original": { - "owner": "NixOS", - "ref": "nixos-22.05-small", - "repo": "nixpkgs", - "type": "github" - } - }, - "nixpkgs-regression": { - "locked": { - "lastModified": 1643052045, - "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", - "type": "github" - }, - "original": { - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", - "type": "github" - } - }, - "nixpkgs_2": { - "locked": { - "lastModified": 1657208011, - "narHash": "sha256-BlIFwopAykvdy1DYayEkj6ZZdkn+cVgPNX98QVLc0jM=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "2770cc0b1e8faa0e20eb2c6aea64c256a706d4f2", + "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b", "type": "github" }, "original": { @@ -183,6 +101,23 @@ "type": "github" } }, + "nixpkgs-old": { + "flake": false, + "locked": { + "lastModified": 1581379743, + "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-19.03", + "repo": "nixpkgs", + "type": "github" + } + }, "root": { "inputs": { "alectryon": "alectryon", @@ -194,6 +129,21 @@ "leanInk": "leanInk", "mdBook": "mdBook" } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } } }, "root": "root", diff --git a/doc/flake.nix b/doc/flake.nix index 77af0ea086..9e5666069e 100644 --- a/doc/flake.nix +++ b/doc/flake.nix @@ -17,7 +17,7 @@ }; outputs = inputs@{ self, ... }: inputs.flake-utils.lib.eachDefaultSystem (system: - with inputs.lean.packages.${system}; with nixpkgs; + with inputs.lean.packages.${system}.deprecated; with nixpkgs; let doc-src = lib.sourceByRegex ../. ["doc.*" "tests(/lean(/beginEndAsMacro.lean)?)?"]; in { @@ -44,21 +44,6 @@ mdbook build -d $out ''; }; - # We use a separate derivation instead of `checkPhase` so we can push it but not `doc` to the binary cache - test = stdenv.mkDerivation { - name ="lean-doc-test"; - src = doc-src; - buildInputs = [ lean-mdbook stage1.Lean.lean-package strace ]; - patchPhase = '' - cd doc - patchShebangs test - ''; - buildPhase = '' - mdbook test - touch $out - ''; - dontInstall = true; - }; leanInk = (buildLeanPackage { name = "Main"; src = inputs.leanInk; diff --git a/flake.lock b/flake.lock index f675631d5b..1055544c1f 100644 --- a/flake.lock +++ b/flake.lock @@ -1,21 +1,5 @@ { "nodes": { - "flake-compat": { - "flake": false, - "locked": { - "lastModified": 1673956053, - "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=", - "owner": "edolstra", - "repo": "flake-compat", - "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9", - "type": "github" - }, - "original": { - "owner": "edolstra", - "repo": "flake-compat", - "type": "github" - } - }, "flake-utils": { "inputs": { "systems": "systems" @@ -34,71 +18,18 @@ "type": "github" } }, - "lean4-mode": { - "flake": false, - "locked": { - "lastModified": 1709737301, - "narHash": "sha256-uT9JN2kLNKJK9c/S/WxLjiHmwijq49EgLb+gJUSDpz0=", - "owner": "leanprover", - "repo": "lean4-mode", - "rev": "f1f24c15134dee3754b82c9d9924866fe6bc6b9f", - "type": "github" - }, - "original": { - "owner": "leanprover", - "repo": "lean4-mode", - "type": "github" - } - }, - "libgit2": { - "flake": false, - "locked": { - "lastModified": 1697646580, - "narHash": "sha256-oX4Z3S9WtJlwvj0uH9HlYcWv+x1hqp8mhXl7HsLu2f0=", - "owner": "libgit2", - "repo": "libgit2", - "rev": "45fd9ed7ae1a9b74b957ef4f337bc3c8b3df01b5", - "type": "github" - }, - "original": { - "owner": "libgit2", - "repo": "libgit2", - "type": "github" - } - }, - "nix": { - "inputs": { - "flake-compat": "flake-compat", - "libgit2": "libgit2", - "nixpkgs": "nixpkgs", - "nixpkgs-regression": "nixpkgs-regression" - }, - "locked": { - "lastModified": 1711102798, - "narHash": "sha256-CXOIJr8byjolqG7eqCLa+Wfi7rah62VmLoqSXENaZnw=", - "owner": "NixOS", - "repo": "nix", - "rev": "a22328066416650471c3545b0b138669ea212ab4", - "type": "github" - }, - "original": { - "owner": "NixOS", - "repo": "nix", - "type": "github" - } - }, "nixpkgs": { "locked": { - "lastModified": 1709083642, - "narHash": "sha256-7kkJQd4rZ+vFrzWu8sTRtta5D1kBG0LSRYAfhtmMlSo=", + "lastModified": 1710889954, + "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "b550fe4b4776908ac2a861124307045f8e717c8e", + "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b", "type": "github" }, "original": { "owner": "NixOS", - "ref": "release-23.11", + "ref": "nixpkgs-unstable", "repo": "nixpkgs", "type": "github" } @@ -120,44 +51,10 @@ "type": "github" } }, - "nixpkgs-regression": { - "locked": { - "lastModified": 1643052045, - "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", - "type": "github" - }, - "original": { - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", - "type": "github" - } - }, - "nixpkgs_2": { - "locked": { - "lastModified": 1710889954, - "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b", - "type": "github" - }, - "original": { - "owner": "NixOS", - "ref": "nixpkgs-unstable", - "repo": "nixpkgs", - "type": "github" - } - }, "root": { "inputs": { "flake-utils": "flake-utils", - "lean4-mode": "lean4-mode", - "nix": "nix", - "nixpkgs": "nixpkgs_2", + "nixpkgs": "nixpkgs", "nixpkgs-old": "nixpkgs-old" } }, diff --git a/flake.nix b/flake.nix index aef11952f4..cceb1de454 100644 --- a/flake.nix +++ b/flake.nix @@ -1,38 +1,21 @@ { - description = "Lean interactive theorem prover"; + description = "Lean development flake. Not intended for end users."; inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable"; # old nixpkgs used for portable release with older glibc (2.27) inputs.nixpkgs-old.url = "github:NixOS/nixpkgs/nixos-19.03"; inputs.nixpkgs-old.flake = false; inputs.flake-utils.url = "github:numtide/flake-utils"; - inputs.nix.url = "github:NixOS/nix"; - inputs.lean4-mode = { - url = "github:leanprover/lean4-mode"; - 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"; - #}; - outputs = { self, nixpkgs, nixpkgs-old, flake-utils, nix, lean4-mode, ... }@inputs: flake-utils.lib.eachDefaultSystem (system: + outputs = { self, nixpkgs, nixpkgs-old, flake-utils, ... }@inputs: flake-utils.lib.eachDefaultSystem (system: let - pkgs = import nixpkgs { - inherit system; - # for `vscode-with-extensions` - config.allowUnfree = true; - }; + pkgs = import nixpkgs { inherit system; }; # An old nixpkgs for creating releases with an old glibc pkgsDist-old = import nixpkgs-old { inherit system; }; # An old nixpkgs for creating releases with an old glibc pkgsDist-old-aarch = import nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; }; - lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; inherit nix lean4-mode; }; + lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; }; devShellWithDist = pkgsDist: pkgs.mkShell.override { stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang; @@ -58,41 +41,15 @@ GDB = pkgsDist.gdb; }); in { - packages = lean-packages // rec { - debug = lean-packages.override { debug = true; }; - stage0debug = lean-packages.override { stage0debug = true; }; - asan = lean-packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address" "-DLEANC_EXTRA_FLAGS=-fsanitize=address" "-DSMALL_ALLOCATOR=OFF" "-DSYMBOLIC=OFF" ]; }; - asandebug = asan.override { debug = true; }; - tsan = lean-packages.override { - extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=thread" "-DLEANC_EXTRA_FLAGS=-fsanitize=thread" "-DCOMPRESSED_OBJECT_HEADER=OFF" ]; - stage0 = (lean-packages.override { - # Compressed headers currently trigger data race reports in tsan. - # Turn them off for stage 0 as well so stage 1 can read its own stdlib. - extraCMakeFlags = [ "-DCOMPRESSED_OBJECT_HEADER=OFF" ]; - }).stage1; - }; - tsandebug = tsan.override { debug = true; }; - stage0-from-input = lean-packages.override { - stage0 = pkgs.writeShellScriptBin "lean" '' - exec ${inputs.lean-stage0.packages.${system}.lean}/bin/lean -Dinterpreter.prefer_native=false "$@" - ''; - }; - inherit self; + packages = { + # to be removed when Nix CI is not needed anymore + inherit (lean-packages) cacheRoots test update-stage0-commit ciShell; + deprecated = lean-packages; }; - defaultPackage = lean-packages.lean-all; # The default development shell for working on lean itself devShells.default = devShellWithDist pkgs; devShells.oldGlibc = devShellWithDist pkgsDist-old; devShells.oldGlibcAArch = devShellWithDist pkgsDist-old-aarch; - - checks.lean = lean-packages.test; - }) // rec { - templates.pkg = { - path = ./nix/templates/pkg; - description = "A custom Lean package"; - }; - - defaultTemplate = templates.pkg; - }; + }); } diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index faa3b0d394..4a31516fdc 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -2,7 +2,7 @@ stdenv, lib, cmake, gmp, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs, ... } @ args: with builtins; -rec { +lib.warn "The Nix-based build is deprecated" rec { inherit stdenv; sourceByRegex = p: rs: lib.sourceByRegex p (map (r: "(/src/)?${r}") rs); buildCMake = args: stdenv.mkDerivation ({ diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix index 879d552efd..2d7e7feab1 100644 --- a/nix/buildLeanPackage.nix +++ b/nix/buildLeanPackage.nix @@ -1,5 +1,5 @@ { lean, lean-leanDeps ? lean, lean-final ? lean, leanc, - stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, lean-emacs, lean-vscode, nix, substituteAll, symlinkJoin, linkFarmFromDrvs, + stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, substituteAll, symlinkJoin, linkFarmFromDrvs, runCommand, darwin, mkShell, ... }: let lean-final' = lean-final; in lib.makeOverridable ( @@ -197,19 +197,6 @@ with builtins; let then map (m: m.module) header.imports else abort "errors while parsing imports of ${mod}:\n${lib.concatStringsSep "\n" header.errors}"; in mkMod mod (map (dep: if modDepsMap ? ${dep} then modCandidates.${dep} else externalModMap.${dep}) deps)) modDepsMap; - makeEmacsWrapper = name: emacs: lean: writeShellScriptBin name '' - ${emacs} --eval "(progn (setq lean4-rootdir \"${lean}\"))" "$@" - ''; - makeVSCodeWrapper = name: lean: writeShellScriptBin name '' - PATH=${lean}/bin:$PATH ${lean-vscode}/bin/code "$@" - ''; - printPaths = deps: writeShellScriptBin "print-paths" '' - echo '${toJSON { - oleanPath = [(depRoot "print-paths" deps)]; - srcPath = ["."] ++ map (dep: dep.src) allExternalDeps; - loadDynlibPaths = map pathOfSharedLib (loadDynlibsOfDeps deps); - }}' - ''; expandGlob = g: if typeOf g == "string" then [g] else if g.glob == "one" then [g.mod] @@ -257,48 +244,4 @@ in rec { -o $out/bin/${executableName} \ ${lib.concatStringsSep " " allLinkFlags} '') {}; - - lean-package = writeShellScriptBin "lean" '' - LEAN_PATH=${modRoot}:$LEAN_PATH LEAN_SRC_PATH=$LEAN_SRC_PATH:${src} exec ${lean-final}/bin/lean "$@" - ''; - emacs-package = makeEmacsWrapper "emacs-package" lean-package; - vscode-package = makeVSCodeWrapper "vscode-package" lean-package; - - link-ilean = writeShellScriptBin "link-ilean" '' - dest=''${1:-.} - mkdir -p $dest/build/lib - ln -sf ${iTree}/* $dest/build/lib - ''; - - makePrintPathsFor = deps: mods: printPaths deps // mapAttrs (_: mod: makePrintPathsFor (deps ++ [mod]) mods) mods; - print-paths = makePrintPathsFor [] (mods' // externalModMap); - # `lean` wrapper that dynamically runs Nix for the actual `lean` executable so the same editor can be - # used for multiple projects/after upgrading the `lean` input/for editing both stage 1 and the tests - lean-bin-dev = substituteAll { - name = "lean"; - dir = "bin"; - src = ./lean-dev.in; - isExecutable = true; - srcRoot = fullSrc; # use root flake.nix in case of Lean repo - inherit bash nix srcTarget srcArgs; - }; - lake-dev = substituteAll { - name = "lake"; - dir = "bin"; - src = ./lake-dev.in; - isExecutable = true; - srcRoot = fullSrc; # use root flake.nix in case of Lean repo - inherit bash nix srcTarget srcArgs; - }; - lean-dev = symlinkJoin { name = "lean-dev"; paths = [ lean-bin-dev lake-dev ]; }; - emacs-dev = makeEmacsWrapper "emacs-dev" "${lean-emacs}/bin/emacs" lean-dev; - emacs-path-dev = makeEmacsWrapper "emacs-path-dev" "emacs" lean-dev; - vscode-dev = makeVSCodeWrapper "vscode-dev" lean-dev; - - devShell = mkShell { - buildInputs = [ nix ]; - shellHook = '' - export LEAN_SRC_PATH="${srcPath}" - ''; - }; }) diff --git a/nix/packages.nix b/nix/packages.nix index 693e212a10..c8e8bbe22f 100644 --- a/nix/packages.nix +++ b/nix/packages.nix @@ -1,9 +1,6 @@ -{ src, pkgs, nix, ... } @ args: +{ src, pkgs, ... } @ args: with pkgs; let - nix-pinned = writeShellScriptBin "nix" '' - ${nix.packages.${system}.default}/bin/nix --experimental-features 'nix-command flakes' --extra-substituters https://lean4.cachix.org/ --option warn-dirty false "$@" - ''; # https://github.com/NixOS/nixpkgs/issues/130963 llvmPackages = if stdenv.isDarwin then llvmPackages_11 else llvmPackages_15; cc = (ccacheWrapper.override rec { @@ -42,40 +39,9 @@ let inherit (lean) stdenv; lean = lean.stage1; inherit (lean.stage1) leanc; - inherit lean-emacs lean-vscode; - nix = nix-pinned; })); - lean4-mode = emacsPackages.melpaBuild { - pname = "lean4-mode"; - version = "1"; - commit = "1"; - src = args.lean4-mode; - packageRequires = with pkgs.emacsPackages.melpaPackages; [ dash f flycheck magit-section lsp-mode s ]; - recipe = pkgs.writeText "recipe" '' - (lean4-mode - :repo "leanprover/lean4-mode" - :fetcher github - :files ("*.el" "data")) - ''; - }; - lean-emacs = emacsWithPackages [ lean4-mode ]; - # updating might be nicer by building from source from a flake input, but this is good enough for now - vscode-lean4 = vscode-utils.extensionFromVscodeMarketplace { - name = "lean4"; - publisher = "leanprover"; - version = "0.0.63"; - sha256 = "sha256-kjEex7L0F2P4pMdXi4NIZ1y59ywJVubqDqsoYagZNkI="; - }; - lean-vscode = vscode-with-extensions.override { - vscodeExtensions = [ vscode-lean4 ]; - }; in { - inherit cc lean4-mode buildLeanPackage llvmPackages vscode-lean4; - lean = lean.stage1; - stage0print-paths = lean.stage1.Lean.print-paths; - HEAD-as-stage0 = (lean.stage1.Lean.overrideArgs { srcTarget = "..#stage0-from-input.stage0"; srcArgs = "(--override-input lean-stage0 ..\?rev=$(git rev-parse HEAD) -- -Dinterpreter.prefer_native=false \"$@\")"; }); - HEAD-as-stage1 = (lean.stage1.Lean.overrideArgs { srcTarget = "..\?rev=$(git rev-parse HEAD)#stage0"; }); - nix = nix-pinned; + inherit cc buildLeanPackage llvmPackages; nixpkgs = pkgs; ciShell = writeShellScriptBin "ciShell" '' set -o pipefail @@ -83,5 +49,4 @@ in { # prefix lines with cumulative and individual execution time "$@" |& ts -i "(%.S)]" | ts -s "[%M:%S" ''; - vscode = lean-vscode; -} // lean.stage1.Lean // lean.stage1 // lean +} // lean.stage1