Prepare to use lean4 from flake
This commit is contained in:
parent
6de5297111
commit
8fc0d047dd
188
nix/base-system/flake.lock
generated
188
nix/base-system/flake.lock
generated
@ -165,24 +165,6 @@
|
||||
"inputs": {
|
||||
"systems": "systems"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1689068808,
|
||||
"narHash": "sha256-6ixXo3wt24N/melDWjq70UuHQLxGV8jZvooRanIHXw0=",
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"rev": "919d646de7be200f3bf08cb76ae1f09402b6f9b4",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"flake-utils_3": {
|
||||
"inputs": {
|
||||
"systems": "systems_2"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1687709756,
|
||||
"narHash": "sha256-Y5wKlQSkgEK2weWdOu4J3riRd+kV/VCgHsqLNTTWQ/0=",
|
||||
@ -197,7 +179,7 @@
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"flake-utils_4": {
|
||||
"flake-utils_3": {
|
||||
"locked": {
|
||||
"lastModified": 1649676176,
|
||||
"narHash": "sha256-OWKJratjt2RW151VUlJPRALb7OU2S5s+f0vLj4o1bHM=",
|
||||
@ -212,9 +194,9 @@
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"flake-utils_5": {
|
||||
"flake-utils_4": {
|
||||
"inputs": {
|
||||
"systems": "systems_3"
|
||||
"systems": "systems_2"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1681202837,
|
||||
@ -230,9 +212,9 @@
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"flake-utils_6": {
|
||||
"flake-utils_5": {
|
||||
"inputs": {
|
||||
"systems": "systems_4"
|
||||
"systems": "systems_3"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1681202837,
|
||||
@ -307,26 +289,6 @@
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"jj-flake": {
|
||||
"inputs": {
|
||||
"flake-utils": "flake-utils_2",
|
||||
"nixpkgs": "nixpkgs_3",
|
||||
"rust-overlay": "rust-overlay"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1694797768,
|
||||
"narHash": "sha256-CA9AQ+lvgbCOfH++A0rHKguTBBn0EEcVRLMAmkDecQo=",
|
||||
"owner": "martinvonz",
|
||||
"repo": "jj",
|
||||
"rev": "e288a152d052a531e0ccb25ae27ce07412d65447",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "martinvonz",
|
||||
"repo": "jj",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"libtexpdf-src": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
@ -363,7 +325,7 @@
|
||||
},
|
||||
"naersk_2": {
|
||||
"inputs": {
|
||||
"nixpkgs": "nixpkgs_7"
|
||||
"nixpkgs": "nixpkgs_6"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1650101877,
|
||||
@ -381,9 +343,9 @@
|
||||
},
|
||||
"nil-flake": {
|
||||
"inputs": {
|
||||
"flake-utils": "flake-utils_3",
|
||||
"nixpkgs": "nixpkgs_4",
|
||||
"rust-overlay": "rust-overlay_2"
|
||||
"flake-utils": "flake-utils_2",
|
||||
"nixpkgs": "nixpkgs_3",
|
||||
"rust-overlay": "rust-overlay"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1694177726,
|
||||
@ -446,20 +408,6 @@
|
||||
}
|
||||
},
|
||||
"nixpkgs_3": {
|
||||
"locked": {
|
||||
"lastModified": 1691683125,
|
||||
"narHash": "sha256-FMU62G57HDbJwU+9V3q7I0mBaQYTYQdtPNlJt2t5/A4=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "4d2389b927696ef8da4ef76b03f2d306faf87929",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"id": "nixpkgs",
|
||||
"type": "indirect"
|
||||
}
|
||||
},
|
||||
"nixpkgs_4": {
|
||||
"locked": {
|
||||
"lastModified": 1690441914,
|
||||
"narHash": "sha256-Ac+kJQ5z9MDAMyzSc0i0zJDx2i3qi9NjlW5Lz285G/I=",
|
||||
@ -475,7 +423,7 @@
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs_5": {
|
||||
"nixpkgs_4": {
|
||||
"locked": {
|
||||
"lastModified": 1701282334,
|
||||
"narHash": "sha256-MxCVrXY6v4QmfTwIysjjaX0XUhqBbxTWWB4HXtDYsdk=",
|
||||
@ -491,7 +439,7 @@
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs_6": {
|
||||
"nixpkgs_5": {
|
||||
"locked": {
|
||||
"lastModified": 1689850295,
|
||||
"narHash": "sha256-fUYf6WdQlhd2H+3aR8jST5dhFH1d0eE22aes8fNIfyk=",
|
||||
@ -507,7 +455,7 @@
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs_7": {
|
||||
"nixpkgs_6": {
|
||||
"locked": {
|
||||
"lastModified": 1650109093,
|
||||
"narHash": "sha256-tqlnKrAdJktRLXTou9le0oTqrYBAFpGscV5RADdpArU=",
|
||||
@ -521,7 +469,7 @@
|
||||
"type": "indirect"
|
||||
}
|
||||
},
|
||||
"nixpkgs_8": {
|
||||
"nixpkgs_7": {
|
||||
"locked": {
|
||||
"lastModified": 1682109806,
|
||||
"narHash": "sha256-d9g7RKNShMLboTWwukM+RObDWWpHKaqTYXB48clBWXI=",
|
||||
@ -539,7 +487,7 @@
|
||||
},
|
||||
"nurl-flake": {
|
||||
"inputs": {
|
||||
"nixpkgs": "nixpkgs_6"
|
||||
"nixpkgs": "nixpkgs_5"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1701273941,
|
||||
@ -555,22 +503,6 @@
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"patchedLibcxx": {
|
||||
"locked": {
|
||||
"lastModified": 1705990968,
|
||||
"narHash": "sha256-MYonu7rb4/U++uQtORQqIMc3DX6M1PI1GETAt2br5Vo=",
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "1c4b0767f4ef0d277c7352eae00337c0a379b69d",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "1c4b0767f4ef0d277c7352eae00337c0a379b69d",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"root": {
|
||||
"inputs": {
|
||||
"agenix-flake": "agenix-flake",
|
||||
@ -578,12 +510,10 @@
|
||||
"darwin": "darwin_2",
|
||||
"durnitisp-flake": "durnitisp-flake",
|
||||
"harpoon-src": "harpoon-src",
|
||||
"jj-flake": "jj-flake",
|
||||
"nil-flake": "nil-flake",
|
||||
"nixpkgs": "nixpkgs_5",
|
||||
"nixpkgs": "nixpkgs_4",
|
||||
"nixpkgs-darwin": "nixpkgs-darwin",
|
||||
"nurl-flake": "nurl-flake",
|
||||
"patchedLibcxx": "patchedLibcxx",
|
||||
"roslyn-lsp": "roslyn-lsp",
|
||||
"runwhen-flake": "runwhen-flake",
|
||||
"rust-overlay-flake": "rust-overlay-flake",
|
||||
@ -612,7 +542,7 @@
|
||||
"runwhen-flake": {
|
||||
"inputs": {
|
||||
"flake-compat": "flake-compat_2",
|
||||
"flake-utils": "flake-utils_4",
|
||||
"flake-utils": "flake-utils_3",
|
||||
"naersk": "naersk_2"
|
||||
},
|
||||
"locked": {
|
||||
@ -630,52 +560,6 @@
|
||||
}
|
||||
},
|
||||
"rust-overlay": {
|
||||
"inputs": {
|
||||
"flake-utils": [
|
||||
"jj-flake",
|
||||
"flake-utils"
|
||||
],
|
||||
"nixpkgs": [
|
||||
"jj-flake",
|
||||
"nixpkgs"
|
||||
]
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1691719735,
|
||||
"narHash": "sha256-GhPn5EIhGt7aFwgC6RELZJC7mUIol9O0k7Dsf2Hu0AM=",
|
||||
"owner": "oxalica",
|
||||
"repo": "rust-overlay",
|
||||
"rev": "ac9d8b2e9acc153145e6fa3c78f9ba458ae517bf",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "oxalica",
|
||||
"repo": "rust-overlay",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"rust-overlay-flake": {
|
||||
"inputs": {
|
||||
"flake-utils": "flake-utils_5",
|
||||
"nixpkgs": [
|
||||
"nixpkgs"
|
||||
]
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1694743934,
|
||||
"narHash": "sha256-4pn0x+OiOFWefBpgyufFVaAeG+LwfVUI/HMCma8xdHU=",
|
||||
"owner": "oxalica",
|
||||
"repo": "rust-overlay",
|
||||
"rev": "6a26dd6da9b4f28d9b4c397bd22b5df4bec8f78a",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "oxalica",
|
||||
"repo": "rust-overlay",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"rust-overlay_2": {
|
||||
"inputs": {
|
||||
"flake-utils": [
|
||||
"nil-flake",
|
||||
@ -700,13 +584,34 @@
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"rust-overlay-flake": {
|
||||
"inputs": {
|
||||
"flake-utils": "flake-utils_4",
|
||||
"nixpkgs": [
|
||||
"nixpkgs"
|
||||
]
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1694743934,
|
||||
"narHash": "sha256-4pn0x+OiOFWefBpgyufFVaAeG+LwfVUI/HMCma8xdHU=",
|
||||
"owner": "oxalica",
|
||||
"repo": "rust-overlay",
|
||||
"rev": "6a26dd6da9b4f28d9b4c397bd22b5df4bec8f78a",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "oxalica",
|
||||
"repo": "rust-overlay",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"sile-flake": {
|
||||
"inputs": {
|
||||
"flake-compat": "flake-compat_3",
|
||||
"flake-utils": "flake-utils_6",
|
||||
"flake-utils": "flake-utils_5",
|
||||
"gitignore": "gitignore",
|
||||
"libtexpdf-src": "libtexpdf-src",
|
||||
"nixpkgs": "nixpkgs_8"
|
||||
"nixpkgs": "nixpkgs_7"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1694595810,
|
||||
@ -767,21 +672,6 @@
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"systems_4": {
|
||||
"locked": {
|
||||
"lastModified": 1681028828,
|
||||
"narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
|
||||
"owner": "nix-systems",
|
||||
"repo": "default",
|
||||
"rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "nix-systems",
|
||||
"repo": "default",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"treesitter-context": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
|
||||
@ -3,8 +3,11 @@
|
||||
# Default to sane nixpkgs versions
|
||||
nixpkgs.url = "github:nixos/nixpkgs/23.11";
|
||||
unstable.url = "nixpkgs";
|
||||
patchedLibcxx.url = "github:nixos/nixpkgs?rev=1c4b0767f4ef0d277c7352eae00337c0a379b69d";
|
||||
nixpkgs-darwin.url = "github:nixos/nixpkgs/nixpkgs-23.11-darwin";
|
||||
#lean4-flake = {
|
||||
# url = "github:leanprover/lean4/v4.4.0";
|
||||
# inputs.nixpkgs.follows = "nixpkgs";
|
||||
#};
|
||||
darwin = {
|
||||
url = "github:lnl7/nix-darwin";
|
||||
# ensure that darwinSystem uses our nixpkgs version
|
||||
@ -22,7 +25,6 @@
|
||||
url = "github:oxalica/rust-overlay";
|
||||
inputs.nixpkgs.follows = "nixpkgs";
|
||||
};
|
||||
jj-flake.url = "github:martinvonz/jj";
|
||||
harpoon-src = {
|
||||
url = "github:ThePrimeagen/harpoon/harpoon2";
|
||||
flake = false;
|
||||
@ -49,7 +51,6 @@
|
||||
runwhen-flake,
|
||||
durnitisp-flake,
|
||||
rust-overlay-flake,
|
||||
jj-flake,
|
||||
agenix-flake,
|
||||
nil-flake,
|
||||
nurl-flake,
|
||||
@ -57,8 +58,8 @@
|
||||
d2-vim-src,
|
||||
treesitter-context,
|
||||
roslyn-lsp,
|
||||
#lean4-flake,
|
||||
unstable,
|
||||
patchedLibcxx,
|
||||
... # We don't use the self or nixpkgs args here so we just glob it.
|
||||
}:
|
||||
rec {
|
||||
@ -169,7 +170,6 @@ EOF";
|
||||
trouble-nvim
|
||||
nightfox-nvim
|
||||
melange-nvim
|
||||
julia-vim # TODO I should get julia language server support set up instead.
|
||||
telescope-nvim
|
||||
telescope-lsp-handlers-nvim
|
||||
plenary-nvim
|
||||
@ -197,11 +197,10 @@ EOF";
|
||||
durnitisp = durnitisp-flake.defaultPackage."${system}";
|
||||
rust-overlay = rust-overlay-flake.overlays.default;
|
||||
sile = sile-flake.defaultPackage.${system};
|
||||
jj = jj-flake.packages."${system}".jujutsu;
|
||||
age = agenix-flake.packages."${system}".default;
|
||||
nurl = nurl-flake.packages."${system}".default;
|
||||
unstablePkgs = import unstable { inherit system; };
|
||||
patchedLibcxxPkgs = import patchedLibcxx { inherit system; };
|
||||
#lean4Pkg = lean4-flake.defaultPackage."${system}";
|
||||
in { config, pkgs, ... }: let
|
||||
d2-lang = pkgs.callPackage ./d2.nix {};
|
||||
in {
|
||||
@ -241,13 +240,12 @@ EOF";
|
||||
environment.systemPackages = (with pkgs; [
|
||||
# TODO(jwall): This appears to be broken due to: https://github.com/NixOS/nixpkgs/issues/166205
|
||||
# Should be fixed by: https://github.com/NixOS/nixpkgs/pull/282624
|
||||
patchedLibcxxPkgs.isabelle
|
||||
patchedLibcxxPkgs.lean4
|
||||
#isabelle
|
||||
lean4
|
||||
terraform # TODO(jeremy): Replace with opentofu when that is an option.
|
||||
consul
|
||||
consul-template
|
||||
nomad
|
||||
postgresql
|
||||
oha
|
||||
nodejs
|
||||
gnumake
|
||||
@ -273,7 +271,6 @@ EOF";
|
||||
#podman-desktop # Broken on darwin right now with electron build issues.
|
||||
# Note that podman expects qemu to be installed in order to use the podman machine setup.
|
||||
qemu
|
||||
podman
|
||||
lima
|
||||
rlwrap
|
||||
docker-client
|
||||
@ -285,7 +282,6 @@ EOF";
|
||||
d2-lang
|
||||
plantuml-c4
|
||||
nssTools
|
||||
packer
|
||||
nomad
|
||||
mkcert
|
||||
kubo
|
||||
@ -313,7 +309,6 @@ EOF";
|
||||
sile
|
||||
runwhen
|
||||
durnitisp
|
||||
jj
|
||||
age
|
||||
nurl
|
||||
];
|
||||
|
||||
@ -505,6 +505,14 @@ local harpoon = require('harpoon')
|
||||
|
||||
harpoon:setup()
|
||||
|
||||
require('lean').setup{
|
||||
lsp = {
|
||||
on_attach = function(client, bufnr)
|
||||
end
|
||||
},
|
||||
mappings = true,
|
||||
}
|
||||
|
||||
-- telescope keymaps
|
||||
vim.keymap.set("n", "<Leader>pl", telescope.extensions.possession.list)
|
||||
vim.keymap.set("n", "<Leader>nff", telescope_builtins.fd)
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user