Formatting

More lean keymappings
don't anchor llvm to 11 anymore
2024-01-31 20:52:11 -05:00 · 2024-01-31 20:52:04 -05:00 · 2024-01-31 20:36:36 -05:00 · 2024-01-31 20:36:10 -05:00 · 2024-01-31 13:52:24 -05:00 · 2024-01-29 23:38:57 -05:00
3 changed files with 82 additions and 177 deletions
--- 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": {
--- 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 {
@ -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
-            patchedLibcxxPkgs.lean4
+            #isabelle
+            # 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
        ];
--- a/nix/base-system/init.lua
+++ b/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'] = {
-        cargo = { features = "all" }
-      }
+        ['rust-analyzer'] = {
+            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)
-    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.
+    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.
+    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'
-    mode = 'cursor',       -- Line used to calculate context. Choices: 'cursor', 'topline'
+    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'
    -- 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)
Author	SHA1	Message	Date
Jeremy Wall	c185dbec6f	Formatting	2024-01-31 20:52:11 -05:00
Jeremy Wall	bd62b52285	More lean keymappings	2024-01-31 20:52:04 -05:00
Jeremy Wall	ca3b74c5f6	don't anchor llvm to 11 anymore	2024-01-31 20:36:36 -05:00
Jeremy Wall	ebb61135a9	Keybindings for lean4.nvim	2024-01-31 20:36:10 -05:00
Jeremy Wall	094df66621	Pin the clang version to 11 for lean beause reasons.	2024-01-31 13:52:24 -05:00
Jeremy Wall	38d5d1d009	Turn off lsp trace logging	2024-01-29 23:38:57 -05:00
Jeremy Wall	8fc0d047dd	Prepare to use lean4 from flake	2024-01-29 23:38:32 -05:00