WAIT MY LEAN SETUP WORKS LET'S GO

This commit is contained in:
mehbark 2024-06-20 12:42:11 -04:00
parent a66e6a7a1e
commit 192e6673bd
5 changed files with 217 additions and 29 deletions

View file

@ -28,12 +28,12 @@
"nixpkgs": "nixpkgs" "nixpkgs": "nixpkgs"
}, },
"locked": { "locked": {
"lastModified": 1711118970, "lastModified": 1717421885,
"narHash": "sha256-fRaKydMSwd1zl6ptBKvn5ej2pqtI8xi9dioFmR8QA+g=", "narHash": "sha256-sSmJt2r4Dx01QCpafOo0r8PNPkZVj46LYJx2REqCwg0=",
"rev": "73fed26f0231ae650122beb3ac1b7654b5cc682c", "rev": "a676a9d2b3fad3891e550ea43d9b4f56063063a8",
"revCount": 425, "revCount": 448,
"type": "tarball", "type": "tarball",
"url": "https://api.flakehub.com/f/pinned/DeterminateSystems/fh/0.1.10/018e66b1-a218-7f23-949d-ace71c4e4c8b/source.tar.gz" "url": "https://api.flakehub.com/f/pinned/DeterminateSystems/fh/0.1.11/018fdea3-513b-72eb-ac8e-c9d5184ec551/source.tar.gz"
}, },
"original": { "original": {
"type": "tarball", "type": "tarball",
@ -53,6 +53,22 @@
"url": "https://flakehub.com/f/edolstra/flake-compat/1.0.1.tar.gz" "url": "https://flakehub.com/f/edolstra/flake-compat/1.0.1.tar.gz"
} }
}, },
"flake-compat_2": {
"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-schemas": { "flake-schemas": {
"locked": { "locked": {
"narHash": "sha256-j8SR19V1SRysyJwpOBF4TLuAvAjF5t+gMiboN4gYQDU=", "narHash": "sha256-j8SR19V1SRysyJwpOBF4TLuAvAjF5t+gMiboN4gYQDU=",
@ -84,6 +100,24 @@
"type": "github" "type": "github"
} }
}, },
"flake-utils_2": {
"inputs": {
"systems": "systems_3"
},
"locked": {
"lastModified": 1710146030,
"narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
"type": "github"
},
"original": {
"owner": "numtide",
"repo": "flake-utils",
"type": "github"
}
},
"home-manager": { "home-manager": {
"inputs": { "inputs": {
"nixpkgs": [ "nixpkgs": [
@ -91,11 +125,11 @@
] ]
}, },
"locked": { "locked": {
"lastModified": 1716930911, "lastModified": 1717525419,
"narHash": "sha256-t4HT5j3Jy7skRB5PINnxcEBCkgE89rGBpwTI7YS4Ffo=", "narHash": "sha256-5z2422pzWnPXHgq2ms8lcCfttM0dz+hg+x1pCcNkAws=",
"owner": "nix-community", "owner": "nix-community",
"repo": "home-manager", "repo": "home-manager",
"rev": "a9b36cbe9292a649222b89fdb9ae9907e9c74086", "rev": "a7117efb3725e6197dd95424136f79147aa35e5b",
"type": "github" "type": "github"
}, },
"original": { "original": {
@ -143,11 +177,11 @@
"xdph": "xdph" "xdph": "xdph"
}, },
"locked": { "locked": {
"lastModified": 1716968065, "lastModified": 1717605046,
"narHash": "sha256-MRgORve3xpie/Cq5r9lmJfbg6e0DGM2IqmBawOW/Ou4=", "narHash": "sha256-zzdMmUNJCPY1KqVjzpukHOecae1AiAzwmBN5hq7jM2U=",
"owner": "hyprwm", "owner": "hyprwm",
"repo": "Hyprland", "repo": "Hyprland",
"rev": "a60c7283e677ed81a466d1c0c864c8a05e192cac", "rev": "c95845b1488b4bd63e901cbdc4cb68c27a45971b",
"type": "github" "type": "github"
}, },
"original": { "original": {
@ -233,6 +267,62 @@
"type": "github" "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"
}
},
"leanpkgs": {
"inputs": {
"flake-utils": "flake-utils_2",
"lean4-mode": "lean4-mode",
"nix": "nix",
"nixpkgs": [
"nixpkgs"
],
"nixpkgs-old": "nixpkgs-old"
},
"locked": {
"lastModified": 1717679178,
"narHash": "sha256-KLHGILjSIXG9qIB7iPeeD2RraO1rAyZLsTgS4IJktWw=",
"owner": "leanprover",
"repo": "lean4",
"rev": "0a0f1d7cc717592d1014bf6ec929372654e97965",
"type": "github"
},
"original": {
"owner": "leanprover",
"repo": "lean4",
"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"
}
},
"naersk": { "naersk": {
"inputs": { "inputs": {
"nixpkgs": [ "nixpkgs": [
@ -241,15 +331,37 @@
] ]
}, },
"locked": { "locked": {
"narHash": "sha256-TunvZMCxXHvU6fz5kq3XTLfojIvTDlbFGfPUFtwCU5o=", "lastModified": 1713520724,
"rev": "06a99941d72e2202ed62b8aa08b9869817fea56f", "narHash": "sha256-CO8MmVDmqZX2FovL75pu5BvwhW+Vugc7Q6ze7Hj8heI=",
"revCount": 332, "rev": "c5037590290c6c7dae2e42e7da1e247e54ed2d49",
"revCount": 335,
"type": "tarball", "type": "tarball",
"url": "https://api.flakehub.com/f/pinned/nix-community/naersk/0.1.332%2Brev-06a99941d72e2202ed62b8aa08b9869817fea56f/018b61d4-48e5-77e8-8893-9f917732b11a/source.tar.gz" "url": "https://api.flakehub.com/f/pinned/nix-community/naersk/0.1.335%2Brev-c5037590290c6c7dae2e42e7da1e247e54ed2d49/018ef76d-0fd8-71be-8bed-58aa46d5dc3a/source.tar.gz"
}, },
"original": { "original": {
"type": "tarball", "type": "tarball",
"url": "https://flakehub.com/f/nix-community/naersk/0.1.332.tar.gz" "url": "https://flakehub.com/f/nix-community/naersk/0.1.335.tar.gz"
}
},
"nix": {
"inputs": {
"flake-compat": "flake-compat_2",
"libgit2": "libgit2",
"nixpkgs": "nixpkgs_3",
"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"
} }
}, },
"nixlib": { "nixlib": {
@ -301,6 +413,39 @@
"url": "https://flakehub.com/f/NixOS/nixpkgs/0.1.514192.tar.gz" "url": "https://flakehub.com/f/NixOS/nixpkgs/0.1.514192.tar.gz"
} }
}, },
"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"
}
},
"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": { "nixpkgs_2": {
"locked": { "locked": {
"lastModified": 1716330097, "lastModified": 1716330097,
@ -319,11 +464,27 @@
}, },
"nixpkgs_3": { "nixpkgs_3": {
"locked": { "locked": {
"lastModified": 1716914467, "lastModified": 1709083642,
"narHash": "sha256-KkT6YM/yNQqirtYj/frn6RRakliB8RDvGqVGGaNhdcU=", "narHash": "sha256-7kkJQd4rZ+vFrzWu8sTRtta5D1kBG0LSRYAfhtmMlSo=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "b550fe4b4776908ac2a861124307045f8e717c8e",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "release-23.11",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs_4": {
"locked": {
"lastModified": 1717459389,
"narHash": "sha256-I8/plBsua4/NZ5bKgj+z7/ThiWuud1YFwLsn1QQ5PgE=",
"owner": "nixos", "owner": "nixos",
"repo": "nixpkgs", "repo": "nixpkgs",
"rev": "4a3fc4cf736b7d2d288d7a8bf775ac8d4c0920b4", "rev": "3b01abcc24846ae49957b30f4345bab4b3f1d14b",
"type": "github" "type": "github"
}, },
"original": { "original": {
@ -360,8 +521,9 @@
"flake-utils": "flake-utils", "flake-utils": "flake-utils",
"home-manager": "home-manager", "home-manager": "home-manager",
"hyprland": "hyprland", "hyprland": "hyprland",
"leanpkgs": "leanpkgs",
"nixos-generators": "nixos-generators", "nixos-generators": "nixos-generators",
"nixpkgs": "nixpkgs_3", "nixpkgs": "nixpkgs_4",
"pesterchum": "pesterchum" "pesterchum": "pesterchum"
} }
}, },
@ -412,6 +574,21 @@
"type": "github" "type": "github"
} }
}, },
"systems_3": {
"locked": {
"lastModified": 1681028828,
"narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
"owner": "nix-systems",
"repo": "default",
"rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
"type": "github"
},
"original": {
"owner": "nix-systems",
"repo": "default",
"type": "github"
}
},
"xdph": { "xdph": {
"inputs": { "inputs": {
"hyprland-protocols": "hyprland-protocols", "hyprland-protocols": "hyprland-protocols",

View file

@ -19,6 +19,9 @@
pesterchum.url = "git+https://g.pyrope.net/pesterchum"; pesterchum.url = "git+https://g.pyrope.net/pesterchum";
pesterchum.inputs.nixpkgs.follows = "nixpkgs"; pesterchum.inputs.nixpkgs.follows = "nixpkgs";
leanpkgs.url = "github:leanprover/lean4";
leanpkgs.inputs.nixpkgs.follows = "nixpkgs";
# for l8r :::;) # for l8r :::;)
#homeage.url = "github:jordanisaacs/homeage"; #homeage.url = "github:jordanisaacs/homeage";
#homeage.inputs.nixpkgs.follows = "nixpkgs"; #homeage.inputs.nixpkgs.follows = "nixpkgs";
@ -33,6 +36,7 @@
hyprland, hyprland,
fh, fh,
pesterchum, pesterchum,
leanpkgs,
... ...
}: }:
let let
@ -47,6 +51,7 @@
home-manager.useUserPackages = true; home-manager.useUserPackages = true;
home-manager.users.mbk = (import ./home.nix) { home-manager.users.mbk = (import ./home.nix) {
inherit conf; inherit conf;
leanpkgs = leanpkgs.packages.x86_64-linux;
more-packages = [ more-packages = [
pesterchum.packages.x86_64-linux.default pesterchum.packages.x86_64-linux.default
]; ];

View file

@ -1,4 +1,4 @@
{ conf, more-packages ? [] }: { conf, more-packages ? [], leanpkgs }:
{ config, pkgs, ... }: { config, pkgs, ... }:
let let
wm = conf.wm; wm = conf.wm;
@ -52,6 +52,8 @@ in
# i like having easy access to a lot of repls # i like having easy access to a lot of repls
deno deno
ghc ghc
ghcid
cabal-install
sbcl sbcl
chez chez
guile guile
@ -69,6 +71,9 @@ in
rustfmt rustfmt
idris2 idris2
# might as well use it consistently
leanpkgs.lean-all
# (builtins.foldl' (a: b: "${a} ${b}") "" (builtins.attrNames leanpkgs))
haskell-language-server haskell-language-server
typst typst
@ -326,15 +331,15 @@ in
# not working right now # not working right now
programs.emacs = { programs.emacs = {
enable = true; enable = true;
package = pkgs.emacs29; package = pkgs.emacs29-pgtk;
extraPackages = epkgs: with epkgs; [ extraPackages = epkgs: with epkgs; [
which-key which-key
all-the-icons-ivy all-the-icons-ivy
bind-key bind-key
counsel counsel
gruvbox-theme gruvbox-theme
leanpkgs.lean4-mode
lsp-mode lsp-mode
# lean-mode
avy avy
consult consult
embark embark
@ -379,7 +384,6 @@ in
cider cider
haskell-mode haskell-mode
lsp-haskell
direnv direnv

View file

@ -978,7 +978,7 @@ If the new path's directories does not exist, create them."
"is" 'erc-server-select "is" 'erc-server-select
"ia" 'erc-track-switch-buffer "ia" 'erc-track-switch-buffer
;clojure ; clojure
"cii" 'cider-jack-in "cii" 'cider-jack-in
"cim" 'cider-inspire-me "cim" 'cider-inspire-me
@ -998,6 +998,9 @@ If the new path's directories does not exist, create them."
; cd => clojure doc ; cd => clojure doc
"cd" 'cider-doc "cd" 'cider-doc
; haskell
"hg" 'haskell-hoogle
)) ))
(use-package evil-goggles (use-package evil-goggles
@ -1061,12 +1064,8 @@ If the new path's directories does not exist, create them."
(use-package lsp-mode (use-package lsp-mode
:ensure t :ensure t
:hook ((haskell-mode . lsp-deferred))
:commands (lsp lsp-deferred)) :commands (lsp lsp-deferred))
(use-package lsp-haskell
:ensure t)
; yay ; yay
(setq confirm-kill-processes nil) (setq confirm-kill-processes nil)
(setq auto-save-interval 100) (setq auto-save-interval 100)

View file

@ -113,6 +113,9 @@
# "haskell.ghcupExecutablePath" = "/home/mbk/.ghcup/bin/ghcup"; # "haskell.ghcupExecutablePath" = "/home/mbk/.ghcup/bin/ghcup";
"haskell.manageHLS" = "PATH"; "haskell.manageHLS" = "PATH";
"haskell.plugin.tactics.config.auto_gas" = 8; "haskell.plugin.tactics.config.auto_gas" = 8;
"haskell.plugin.ghcide-code-actions-type-signatures.globalOn" = true;
"haskell.plugin.changeTypeSignature.globalOn" = true;
"haskell.plugin.ghcide-type-lenses.config.mode" = "exported";
"idris.numbersOfContinuousTypechecking" = 50; "idris.numbersOfContinuousTypechecking" = 50;
"idris.warnPartial" = true; "idris.warnPartial" = true;
"latex-workshop.view.pdf.viewer" = "tab"; "latex-workshop.view.pdf.viewer" = "tab";