make -> just

The README is updated with the new syntax for running recipes.

Author: Julian

.github/workflows/ci.yml

@@ -75,5 +75,8 @@ jobs:
         run: sudo npm install -g lean-language-server
         if: contains(matrix.lean-version, 'lean:3')
 
+      - uses: extractions/setup-just@v1
       - name: Run tests
-        run: make TEST_SEQUENTIAL=1 test
+        run: just test
+        env:
+          TEST_SEQUENTIAL: 1

Makefile

@@ -341,32 +341,39 @@ Contributing
 Contributions are most welcome.
 Feel free to send pull requests for anything you'd like to see, or open an issue if you'd like to discuss.
 
-Running the tests can be done via the ``Makefile``:
+Running the tests can be done via `just <https://github.com/casey/just>`_ using the adjacent `justfile <../justfile>`_:
 
 .. code:: sh
 
-    $ make test
+    $ just
 
-which will execute against a minimal ``vimrc`` isolated from your own setup.
+which will execute against a minimal ``init.lua`` isolated from your own setup.
+
+After running the test suite once, you can save some time re-cloning dependencies by instead now running:
 
 .. code:: sh
 
-    $ TEST_FILE=lua/tests/foo_spec.lua make test
+    $ just retest
+
+You can also run single test files by running:
+
+.. code:: sh
 
-can be used to run just one specific test file, which can be faster.
+    $ just retest lua/tests/ft_spec.lua
 
 Some linting and style checking is done via `pre-commit <https://pre-commit.com/#install>`_, which once installed (via the linked instructions) is run via:
 
 .. code:: sh
 
-    $ make lint
+    $ just lint
 
 or on each commit automatically if you have run ``pre-commit install`` in your repository checkout.
 
 You can also use
 
 .. code:: sh
 
-    $ make nvim SETUP_TABLE='{ lsp = { enable = true }, mappings = true }'
+    $ just nvim '{ lsp = { enable = true }, mappings = true }'
 
-to get a normal running neovim (again isolated from your own configuration), where ``SETUP_TABLE`` is a (Lua) table like one would pass to ``lean.setup``.
+to get a normal running neovim (again isolated from your own configuration), where the provided argument is a (Lua) table like one would pass to ``lean.setup``.
+Any further arguments will be passed to ``nvim``.

README.rst

@@ -0,0 +1,55 @@
+has_lean3 := if `leanpkg help 2>&1 >/dev/null; echo $?` == "0" { "true" } else { "false" }
+
+packpath := justfile_directory() + "/packpath"
+scripts := justfile_directory() + "/scripts"
+tests := justfile_directory() + "/lua/tests"
+fixtures := tests + "/fixtures"
+
+init_lua := scripts + "/minimal_init.lua"
+runner := scripts + "/run_tests.lua"
+
+# Run the lean.nvim test suite.
+test: _rebuild-test-fixtures _clone-test-dependencies
+    @just retest
+
+# Run the test suite without rebuilding or recloning any dependencies.
+retest *test_files=tests:
+    nvim --headless -u {{ init_lua }} -l {{ runner }} {{ test_files }}
+
+# Run an instance of neovim with the same minimal init used to run tests.
+nvim setup_table='{}' *ARGS='':
+    nvim -u {{ init_lua }} -c "lua require('lean').setup{{ setup_table }}" {{ ARGS }}
+
+# Coarsely profile how long the whole test suite takes to run.
+profile-test *ARGS: _rebuild-test-fixtures _clone-test-dependencies
+    hyperfine --warmup 2 {{ ARGS }} "just retest"
+
+# Lint lean.nvim for style and typing issues.
+lint:
+    pre-commit run --all-files
+    @echo
+    {{ if `lua-language-server --version 2>&1 >/dev/null; echo $?` != "0" { error('lua-language-server not found') } else { "" } }}
+    lua-language-server --check lua/lean --checklevel=Warning --configpath "{{ justfile_directory() }}/.luarc.json"
+
+# Update the versions of test fixtures used in CI.
+bump-test-fixtures:
+    cd {{ fixtures }}/example-lean3-project/; {{ if `leanpkg help 2>&1 >/dev/null; echo $?` != "0" { "" } else { `leanproject up` } }}
+    cd {{ fixtures }}/example-lean4-project/; gh api -H 'Accept: application/vnd.github.raw' '/repos/leanprover-community/Mathlib4/contents/lean-toolchain' >lean-toolchain
+    git add --all
+    git commit -m "Bump the Lean versions in CI."
+
+# Delete any previously cloned test dependencies.
+_clean-test-dependencies:
+    rm -rf '{{ packpath }}'
+    mkdir '{{ packpath }}'
+
+# Clone any neovim dependencies required for the plugin + test suite.
+_clone-test-dependencies: _clean-test-dependencies
+    for dependency in AndrewRadev/switch.vim Julian/inanis.nvim neovim/nvim-lspconfig nvim-lua/plenary.nvim tomtom/tcomment_vim; do \
+        git clone --quiet --filter=blob:none "https://github.com/$dependency" "{{ packpath }}/$(basename $dependency)"; \
+    done
+
+# Rebuild some test fixtures used in the test suite.
+_rebuild-test-fixtures:
+    cd "{{ justfile_directory() }}/lua/tests/fixtures/example-lean3-project/" {{ if `leanpkg help 2>&1 >/dev/null; echo $?` != "0" { "" } else { `leanpkg build` } }}
+    cd "{{ justfile_directory() }}/lua/tests/fixtures/example-lean4-project/"; lake build

justfile

@@ -4,9 +4,10 @@ local opts = {
   sequential = vim.env.TEST_SEQUENTIAL ~= nil,
 }
 
-local test_file = vim.env.TEST_FILE or './lua/tests/'
-if vim.fn.isdirectory(test_file) == 1 then
-  harness.test_directory(test_file, opts)
-else
-  harness.test_file(test_file, opts)
+for _, test_file in ipairs(arg) do
+  if vim.fn.isdirectory(test_file) == 1 then
+    harness.test_directory(test_file, opts)
+  else
+    harness.test_file(test_file, opts)
+  end
 end