Skip to content

Commit

Permalink
Clone testing dependencies in the Makefile.
Browse files Browse the repository at this point in the history
  • Loading branch information
Julian committed Sep 24, 2023
1 parent af46a11 commit e639c7e
Show file tree
Hide file tree
Showing 3 changed files with 13 additions and 10 deletions.
8 changes: 0 additions & 8 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
13 changes: 12 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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"

Expand All @@ -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:
Expand Down
2 changes: 1 addition & 1 deletion lua/tests/fixtures/example-lean4-project/lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.0.0
leanprover/lean4:v4.1.0-rc1

0 comments on commit e639c7e

Please sign in to comment.