Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
255 stars 25 forks source link

Perform ftdetect in pure lua with no plugin call #273

Closed 4e554c4c closed 2 years ago

4e554c4c commented 2 years ago

Summary: I use the packer package manager which lets one only enable certain plugins if a filetype related to them is set. In order to get around the issue that these plugins also may also set those filetypes---packer installs and loads only the filedetect scripts of the ft triggered plugins. If one attempts to do this for lean.nvim, then the filedetect script fails as it immediately calls into the lean.nvim plugin which is yet to be loaded. Since filedetect scripts can be pure lua in neovim, i have replaced the ftdetect/lean3.vim shim with the standalone ftdetect/lean.lua script. In order to get around configuration issues, this filedetect script configures the ft configuration global which can be modified by the plugin itself.

Test Plan: edited lua/tests/fixtures/example-lean4-project/Test.lean and lua/tests/fixtures/example-lean3-project/src/foo.lean and verified that set ft? returned lean and lean3 respectively.

before:

$ TEST_FILE=lua/tests/ft_spec.lua ./lua/tests/scripts/run_tests.sh

========================================
Testing:    lua/tests/ft_spec.lua
Success ||  ft.detect detects nonexisting lean 4 files
Success ||  ft.detect detects nested nonexisting lean 4 files
Success ||  ft.detect detects existing lean 4 files
Success ||  ft.detect detects nested existing lean 4 files
Success ||  ft.detect detects nonexisting lean 3 files
Success ||  ft.detect detects nested nonexisting lean 3 files
Success ||  ft.detect detects existing lean 3 files
Success ||  ft.detect detects nested existing lean 3 files
Fail    ||  ft.detect detects lean 4 standard library files
            lua/tests/ft_spec.lua:30: attempt to call field 'wait_for_loading_pins' (a nil value)

            stack traceback:
                lua/tests/ft_spec.lua:30: in function <lua/tests/ft_spec.lua:24>

Fail    ||  ft.detect marks lean 4 standard library files nomodifiable by default
            lua/tests/ft_spec.lua:42: Didn't jump to core Lean!
            Expected to be truthy, but value was:
            (nil)

            stack traceback:
                lua/tests/ft_spec.lua:42: in function <lua/tests/ft_spec.lua:39>

Success ||  ft.detect does not mark other lean 4 files nomodifiable
Fail    ||  ft.detect detects lean 3 standard library files
            lua/tests/ft_spec.lua:57: attempt to call field 'wait_for_line_diagnostics' (a nil value)

            stack traceback:
                lua/tests/ft_spec.lua:57: in function <lua/tests/ft_spec.lua:51>

Fail    ||  ft.detect marks lean 3 standard library files nomodifiable by default
            lua/tests/ft_spec.lua:68: Expected to be truthy, but value was:
            (nil)

            stack traceback:
                lua/tests/ft_spec.lua:68: in function <lua/tests/ft_spec.lua:66>

Success ||  ft.detect does not mark other lean 3 files nomodifiable

Success:    10
Failed :    4
Errors :    0
========================================
Tests Failed. Exit: 1

after:

$ TEST_FILE=lua/tests/ft_spec.lua ./lua/tests/scripts/run_tests.sh

========================================
Testing:    lua/tests/ft_spec.lua
Success ||  ft.detect detects nested nonexisting lean 4 files
Success ||  ft.detect detects existing lean 4 files
Success ||  ft.detect detects nested existing lean 4 files
Success ||  ft.detect detects nonexisting lean 4 files
Success ||  ft.detect detects nested nonexisting lean 3 files
Success ||  ft.detect detects existing lean 3 files
Success ||  ft.detect detects nested existing lean 3 files
Success ||  ft.detect detects nonexisting lean 3 files
Fail    ||  ft.detect detects lean 4 standard library files
            lua/tests/ft_spec.lua:30: attempt to call field 'wait_for_loading_pins' (a nil value)

            stack traceback:
                lua/tests/ft_spec.lua:30: in function <lua/tests/ft_spec.lua:24>

Fail    ||  ft.detect marks lean 4 standard library files nomodifiable by default
            lua/tests/ft_spec.lua:42: Didn't jump to core Lean!
            Expected to be truthy, but value was:
            (nil)

            stack traceback:
                lua/tests/ft_spec.lua:42: in function <lua/tests/ft_spec.lua:39>

Success ||  ft.detect does not mark other lean 4 files nomodifiable
Fail    ||  ft.detect detects lean 3 standard library files
            lua/tests/ft_spec.lua:57: attempt to call field 'wait_for_line_diagnostics' (a nil value)

            stack traceback:
                lua/tests/ft_spec.lua:57: in function <lua/tests/ft_spec.lua:51>

Fail    ||  ft.detect marks lean 3 standard library files nomodifiable by default
            lua/tests/ft_spec.lua:68: Expected to be truthy, but value was:
            (nil)

            stack traceback:
                lua/tests/ft_spec.lua:68: in function <lua/tests/ft_spec.lua:66>

Success ||  ft.detect does not mark other lean 3 files nomodifiable

Success:    10
Failed :    4
Errors :    0
========================================
Tests Failed. Exit: 1

same number of tests pass and fail.

Fixes #272

Julian commented 2 years ago

Thanks! Left 2 small comments, appreciate the PR!

Julian commented 2 years ago

Perfect! Thanks for double checking. This looks great now, merging!