sorryfill modification for Lean 4

[gihanmarasingha]

Tests whether the buffer is lean3 or lean4 and adapts sorry.fill accordingly.

Note, in the modified indentation code, that "\194\183" is the unicode for the centered dot character, used for indentation of Lean 4 subgoals.

[Julian]

Thanks! Could you perhaps give at least a quick shot towards making the tests for this function to cover Lean 4 as well? They live in the tests folder and already are obviously covering the Lean 3 behavior but not the Lean 4 one.

[gihanmarasingha]

Thanks! Could you perhaps give at least a quick shot towards making the tests for this function to cover Lean 4 as well? They live in the tests folder and already are obviously covering the Lean 3 behavior but not the Lean 4 one.

Sure. I'll have a go at that.

However, local testing doesn't quite work for me. When I run make test on my computer, only 24 of the 31 tests complete. For example, when I run

TEST_FILE=lua/tests/sorry_spec.lua make test 

I get a message

cd ./lua/tests/fixtures/example-lean3-project/ && leanpkg build
configuring example-lean3-project 0.1
mathlib: trying to update _target/deps/mathlib to revision 001ffdc42920050657fd45bd2b8bfbec8eaaeb29
> git checkout --detach 001ffdc42920050657fd45bd2b8bfbec8eaaeb29    # in directory _target/deps/mathlib
HEAD is now at 001ffdc429 feat(probability/independence): Independence of singletons (#18506)
> lean --make src
cd ./lua/tests/fixtures/example-lean4-project/ && lake build
./lua/tests/scripts/run_tests.sh
Scheduling: lua/tests/sorry_spec.lua

========================================    
Testing:    /Users/xxx/Documents/lean_projects/lean.nvim/lua/tests/sorry_spec.lua   
Server has stopped with error code 1.: 
make: *** [test] Error 1

Any idea why that is? I'm running macOS on an M2 mac.

[Julian]

Hmmm interesting. Do you have Lean 3 installed as well just to be sure?

[gihanmarasingha]

Hmmm interesting. Do you have Lean 3 installed as well just to be sure?

Yes. And I installed the lean-language-server as per the instructions on your repo.

[gihanmarasingha]

Hmmm interesting. Do you have Lean 3 installed as well just to be sure?

Yes. And I installed the lean-language-server as per the instructions on your repo.

If it helps, the tests that don't run are:

diags_spec.lua
fixtures.lua
helpers.lua
sorry_spec.lua
trythis_spec.lua
infoview/contents_spec.lua
infoview/widgets_spec.lua

[Julian]

And opening a lean 3 file doesn't error, and :checkhealth lean succeeds?

[gihanmarasingha]

I can certainly open lean 3 files in nvim (via your plugin!) and everything runs fine. Or just run lean on lean files in a Lean 3 project via the terminal.

When I run :checkhealth lean, I get nice green 'OK' messages whether I open neovim from within a Lean 3 project or a Lean 4 project (or no project). In particular, it works from within the example-lean3-project.

[Julian]

Interesting, OK I'll have to remind myself how you get plenary to show more information about the failures when I get back to a computer.

[gihanmarasingha]

I've given up on trying to get the tests working on my local machine and tested through GitHub actions instead. I've added some lean 4 testing code and will now push the latest commit.

[Julian]

Last night it occurred to me that perhaps the issue locally is not having the dependencies cloned to packpath/? That's something I see we didn't make the Makefile do automatically for you. But yes checking via GH actions is fine too.

[Julian]

REgardless this looks good to me, thanks again!

[gihanmarasingha]

My pleasure! I'm working on a small improvements.

In particular, it's nicer to have a sorry rather than a · sorry if there's only one goal. Will need to write some appropriate tests.