diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4b257435..d7c9b008 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -75,13 +75,5 @@ jobs: run: sudo npm install -g lean-language-server if: contains(matrix.lean-version, 'lean:3') - - name: Install nvim dependencies - run: | - mkdir packpath - git clone --depth 1 https://github.com/AndrewRadev/switch.vim/ packpath/switch.vim - git clone --depth 1 https://github.com/tomtom/tcomment_vim packpath/tcomment_vim - git clone --depth 1 https://github.com/neovim/nvim-lspconfig packpath/nvim-lspconfig - git clone --depth 1 https://github.com/nvim-lua/plenary.nvim packpath/plenary.nvim - - name: Run tests run: make TEST_SEQUENTIAL=1 test diff --git a/Makefile b/Makefile index c6ba9fd2..d85f8c7d 100644 --- a/Makefile +++ b/Makefile @@ -6,6 +6,7 @@ SETUP = "lua require'lean'.setup$(SETUP_TABLE)" nvim: nvim --noplugin -u scripts/minimal_init.lua -c $(SETUP) $(ARGS) + docgen: nvim --headless --noplugin -u scripts/minimal_init.lua -c "luafile ./scripts/gendocs.lua" -c "qa" @@ -19,7 +20,17 @@ bump-test-fixtures: git add --all git commit -m "Bump the Lean versions in CI." -test: build-test-fixtures +clean-deps: + rm -rf packpath/ + +clone-deps: clean-deps + mkdir packpath && cd packpath && \ + git clone --filter=blob:none https://github.com/AndrewRadev/switch.vim && \ + git clone --filter=blob:none https://github.com/neovim/nvim-lspconfig && \ + git clone --filter=blob:none https://github.com/nvim-lua/plenary.nvim && \ + git clone --filter=blob:none https://github.com/tomtom/tcomment_vim + +test: build-test-fixtures clone-deps ./lua/tests/scripts/run_tests.sh _test: diff --git a/lua/tests/fixtures/example-lean4-project/lean-toolchain b/lua/tests/fixtures/example-lean4-project/lean-toolchain index f0a6d660..640f2091 100644 --- a/lua/tests/fixtures/example-lean4-project/lean-toolchain +++ b/lua/tests/fixtures/example-lean4-project/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.0.0 +leanprover/lean4:v4.1.0-rc1