From 8fc0d047dd4a7be9b2a2ec92bce2f05d5a0c9c53 Mon Sep 17 00:00:00 2001 From: Jeremy Wall Date: Mon, 29 Jan 2024 21:49:43 -0500 Subject: [PATCH] Prepare to use lean4 from flake --- nix/base-system/flake.lock | 188 ++++++++----------------------------- nix/base-system/flake.nix | 21 ++--- nix/base-system/init.lua | 8 ++ 3 files changed, 55 insertions(+), 162 deletions(-) diff --git a/nix/base-system/flake.lock b/nix/base-system/flake.lock index badc170..2ab421b 100644 --- a/nix/base-system/flake.lock +++ b/nix/base-system/flake.lock @@ -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": { diff --git a/nix/base-system/flake.nix b/nix/base-system/flake.nix index f3eab17..920a353 100644 --- a/nix/base-system/flake.nix +++ b/nix/base-system/flake.nix @@ -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 ]; diff --git a/nix/base-system/init.lua b/nix/base-system/init.lua index c61d7db..92cd395 100644 --- a/nix/base-system/init.lua +++ b/nix/base-system/init.lua @@ -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", "pl", telescope.extensions.possession.list) vim.keymap.set("n", "nff", telescope_builtins.fd)