Formatting

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",
+        "flake-utils": "flake-utils_2",
-        "nixpkgs": "nixpkgs_4",
+        "nixpkgs": "nixpkgs_3",
-        "rust-overlay": "rust-overlay_2"
+        "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": {

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 {
@@ -214,7 +213,11 @@ EOF";
       config = {
        
         nixpkgs.overlays = [
-         rust-overlay
+          (final: prev: {
+            # This is needed because the ccache used by lean4Pkg is broken
+            ccache = prev.ccache.override { doCheck = false; };
+          })
+          rust-overlay
         ];
 
         # TODO(jwall): This is needed for terraform
@@ -241,13 +244,14 @@ 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
+            #isabelle
-            patchedLibcxxPkgs.lean4
+            # 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
+            (lean4.override { stdenv = stdenv.override { allowedRequisites = null; cc = llvmPackages_11.clang; }; })
             terraform # TODO(jeremy): Replace with opentofu when that is an option.
             consul
             consul-template
             nomad
-            postgresql
             oha
             nodejs
             gnumake
@@ -273,7 +277,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 +288,6 @@ EOF";
             d2-lang
             plantuml-c4
             nssTools
-            packer
             nomad
             mkcert
             kubo
@@ -299,7 +301,8 @@ EOF";
             ripgrep
             fd
             lldb
-            llvmPackages.bintools-unwrapped
+            # TODO(jwall): For now it appears that a bunch of things around linking are broken on darwin so we are going to use clang11
+            llvmPackages.libcxxClang
             # TODO add sonic-pi here if it supports the arch
         ])
         ++ (with pkgs.ocamlPackages; [
@@ -313,7 +316,6 @@ EOF";
             sile
             runwhen
             durnitisp
-            jj
             age
             nurl
         ];

nix/base-system/init.lua

@@ -91,7 +91,7 @@ cmp.setup({
     sources = cmp.config.sources(
         {
             { name = 'nvim_lsp',               keyword_length = 3 }, -- from language server
-            { name = 'nvim_lsp_signature_help' }, -- display function signatures with current parameter emphasized
+            { name = 'nvim_lsp_signature_help' },                    -- display function signatures with current parameter emphasized
         },
         {
             { name = 'path' }, -- file paths
@@ -121,8 +121,6 @@ local caps = vim.tbl_deep_extend(
     { window = { progress = false } }
 );
 
-vim.lsp.set_log_level(vim.log.levels.TRACE)
-
 local lspconfig = require("lspconfig")
 
 -- Terraform lsp setup
@@ -197,9 +195,9 @@ lspconfig.tsserver.setup {
 lspconfig.rust_analyzer.setup {
     settings = {
         -- https://github.com/rust-lang/rust-analyzer/blob/master/docs/user/generated_config.adoc
-      ['rust-analyzer'] = {
+        ['rust-analyzer'] = {
-        cargo = { features = "all" }
+            cargo = { features = "all" }
-      }
+        }
     },
     capabilities = caps
 }
@@ -228,7 +226,7 @@ lspconfig.lua_ls.setup {
 }
 
 -- lsp configuration
-vim.api.nvim_create_autocmd('LspAttach', {
+vim.api.nvim_create_autocmd('LNspAttach', {
     callback = function(args)
         local opts = { buffer = args.buf }
         vim.keymap.set("n", '<C-Space>', function()
@@ -349,17 +347,17 @@ require('nvim-treesitter.configs').setup {
 }
 
 require 'treesitter-context'.setup {
-    enable = true,         -- Enable this plugin (Can be enabled/disabled later via commands)
+    enable = true,            -- Enable this plugin (Can be enabled/disabled later via commands)
-    max_lines = 5,         -- How many lines the window should span. Values <= 0 mean no limit.
+    max_lines = 5,            -- How many lines the window should span. Values <= 0 mean no limit.
-    min_window_height = 45, -- Minimum editor window height to enable context. Values <= 0 mean no limit.
+    min_window_height = 45,   -- Minimum editor window height to enable context. Values <= 0 mean no limit.
     line_numbers = true,
     multiline_threshold = 20, -- Maximum number of lines to collapse for a single context line
-    trim_scope = 'outer',  -- Which context lines to discard if `max_lines` is exceeded. Choices: 'inner', 'outer'
+    trim_scope = 'outer',     -- Which context lines to discard if `max_lines` is exceeded. Choices: 'inner', 'outer'
-    mode = 'cursor',       -- Line used to calculate context. Choices: 'cursor', 'topline'
+    mode = 'cursor',          -- Line used to calculate context. Choices: 'cursor', 'topline'
     -- Separator between context and content. Should be a single character string, like '-'.
     -- When separator is set, the context will only show up when there are at least 2 lines above cursorline.
     separator = nil,
-    zindex = 20,   -- The Z-index of the context window
+    zindex = 20,     -- The Z-index of the context window
     on_attach = nil, -- (fun(buf: integer): boolean) return false to disable attaching
 }
 
@@ -505,6 +503,21 @@ local harpoon = require('harpoon')
 
 harpoon:setup()
 
+local lean = require 'lean'
+
+lean.setup {
+    lsp = {
+        on_attach = function(client, bufnr)
+            local opts = { buffer = bufnr }
+            vim.keymap.set({ "n", "v" }, "<Leader>ti", function() vim.cmd("LeanInfoviewToggle") end, opts)
+            vim.keymap.set({ "n", "v" }, "<Leader>sg", function() vim.cmd("LeanGoal") end, opts)
+            vim.keymap.set({ "n", "v" }, "<Leader>stg", function() vim.cmd("LeanTermGoal") end, opts)
+            vim.api.nvim_buf_set_option(bufnr, 'omnifunc', 'v:lua.vim.lsp.omnifunc')
+        end
+    },
+    mappings = true,
+}
+
 -- telescope keymaps
 vim.keymap.set("n", "<Leader>pl", telescope.extensions.possession.list)
 vim.keymap.set("n", "<Leader>nff", telescope_builtins.fd)