search

Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
277 stars 26 forks source link

Use `lean --version` to infer filetype when `elan` is installed. #119

Closed rish987 closed 3 years ago

rish987 commented 3 years ago

Closes #88, failed Lean 3 stdlib ft test pending leanprover/elan#36. Also fixed the stdlib filetype tests.

codecov[bot] commented 3 years ago

Codecov Report

Merging #119 (dd1a73a) into main (d0307a1) will decrease coverage by 0.55%. The diff coverage is 82.35%.

Impacted file tree graph

@@            Coverage Diff             @@
##             main     #119      +/-   ##
==========================================
- Coverage   94.73%   94.18%   -0.56%     
==========================================
  Files          31       31              
  Lines        1690     1702      +12     
==========================================
+ Hits         1601     1603       +2     
- Misses         89       99      +10
Impacted Files Coverage Δ
lua/lean/ft.lua 71.42% <71.42%> (-28.58%) :arrow_down:
lua/lean/lean3.lua 77.77% <90.00%> (-22.23%) :arrow_down:

Continue to review full report at Codecov.

Legend - Click here to learn more Δ = absolute <relative> (impact), ø = not affected, ? = missing data Powered by Codecov. Last update d0307a1...dd1a73a. Read the comment docs.

rish987 commented 3 years ago

@gebner I think there might be a slight MacOS bug with leanprover/elan#36, see test failures -- since our default toolchain in CI is Lean 3 (and the error mistook lean for lean3), I have a suspicion that it has to do with leanprover/elan#36 checking the path case-sensitively, while MacOS has a case-insensitive (all-lowercase) filesystem.

gebner commented 3 years ago

I have a suspicion that it has to do with leanprover/elan#36 checking the path case-sensitively, while MacOS has a case-insensitive (all-lowercase) filesystem.

This is a potential explanation. But I think we need someone with access to a MacOS machine to debug this (and test the fix).

Julian commented 3 years ago

I have a mountain of things on my plate now for the next few days so I'm going to be quite slow at many things, but will see if I can circle back when I get a moment.

rish987 commented 3 years ago

Nevermind Gabriel your code is good (also tested it at rish987/elan@6658cab, let me know if that's worth upstreaming). I fixed this by schedule_wraping our elan- based filetype detection.

Julian commented 3 years ago

Can you separate (and feel free to merge separately) the unrelated changes here so it's easier to see what this does?