2ede81fe10
This PR fixes a number of bugs related to the handling of the source search path in the language server, where deleting files could cause several features to stop functioning and both untitled files and files that don't exist on disc could have conflicting module names. In detail, it makes the following adjustments: - The URI <-> module name conversion was adjusted to produce no name collisions. - File URIs in the search path yield a module name relative to the search path, as before. - File URIs not in the search path, non-file URIs and non-`.lean` files yield a `«external:<full uri>»` module name. - To avoid the issue of the URI -> module name conversion failing when a file is deleted from disc, we now cache the result of this conversion in the watchdog and the file worker when the file is first opened. - All of the URI <-> module name conversions now consistently go through `Server.documentUriFromModule?` and `moduleFromDocumentUri` to ensure that we don't have minor deviations for this conversion all over the place. - The threading of the source search path through the file worker (from `lake setup-file`) is removed. It turns out that `lake serve` already sets the correct source search path in the environment, so we can just always use the search path from the environment. - Since we can now answer more requests that need the .ileans in untitled files, a lot of the tests that test 'Go to definition' needed to be adjusted so that they use the information from the watchdog, not the file worker. As we load references asynchronously, this PR adds an internal `$/lean/waitForILeans` request that tests can use to wait for all .ilean files to be loaded and for the ilean references from the file worker for the current document version to be finalized. - As part of this PR, we noticed that the .ileans aren't available in the NixOS setup, so @Kha adjusted the Nix CI to fix this. ### Breaking changes - `Server.documentUriFromModule` has been renamed to `Server.documentUriFromModule?` and doesn't take a `SearchPath` argument anymore, as the `SearchPath` is now computed from the `LEAN_SRC_PATH` environment variable. It has also been moved from `Lean.Server.GoTo` to `Lean.Server.Utils`. - `Server.moduleFromDocumentUri` does not take a `SearchPath` argument anymore and won't return an `Option` anymore. It has also been moved from `Lean.Server.GoTo` to `Lean.Server.Utils`. - The `System.SearchPath.searchModuleNameOfUri` function has been removed. It is recommended to use `Server.moduleFromDocumentUri` instead. - The `initSrcSearchPath` function has been renamed to `getSrcSearchPath` and has been moved from `Lean.Util.Paths` to `Lean.Util.Path`. It also doesn't need to take a `pkgSearchPath` argument anymore. --------- Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
301 lines
6.6 KiB
Text
301 lines
6.6 KiB
Text
import Lean
|
||
--^ waitForILeans
|
||
example : True := by
|
||
apply True.intro
|
||
--^ textDocument/hover
|
||
|
||
example : True := by
|
||
simp [True.intro]
|
||
--^ textDocument/hover
|
||
|
||
example (n : Nat) : True := by
|
||
match n with
|
||
| Nat.zero => _
|
||
--^ textDocument/hover
|
||
| n + 1 => _
|
||
|
||
|
||
/-- My tactic -/
|
||
macro "mytac" o:"only"? e:term : tactic => `(tactic| exact $e)
|
||
|
||
example : True := by
|
||
mytac only True.intro
|
||
--^ textDocument/hover
|
||
--^ textDocument/hover
|
||
--^ textDocument/hover
|
||
|
||
/-- My way better tactic -/
|
||
macro_rules
|
||
| `(tactic| mytac $[only]? $e:term) =>
|
||
--^ textDocument/hover
|
||
--^ textDocument/hover
|
||
`(tactic| apply $e:term)
|
||
--^ textDocument/hover
|
||
--^ textDocument/hover
|
||
|
||
example : True := by
|
||
mytac only True.intro
|
||
--^ textDocument/hover
|
||
|
||
/-- My ultimate tactic -/
|
||
elab_rules : tactic
|
||
| `(tactic| mytac $[only]? $e) => do Lean.Elab.Tactic.evalTactic (← `(tactic| refine $e))
|
||
|
||
example : True := by
|
||
mytac only True.intro
|
||
--^ textDocument/hover
|
||
|
||
|
||
/-- My notation -/
|
||
macro (name := myNota) "mynota" e:term : term => pure e
|
||
--^ textDocument/hover
|
||
|
||
#check mynota 1
|
||
--^ textDocument/hover
|
||
|
||
/-- My way better notation -/
|
||
macro_rules
|
||
| `(mynota $e) => `(2 * $e)
|
||
|
||
#check mynota 1
|
||
--^ textDocument/hover
|
||
|
||
-- macro_rules take precedence over elab_rules for term/command, so use new syntax
|
||
syntax "mynota'" term : term
|
||
|
||
/-- My ultimate notation -/
|
||
elab_rules : term
|
||
| `(mynota' $e) => `($e * $e) >>= (Lean.Elab.Term.elabTerm · none)
|
||
|
||
#check mynota' 1
|
||
--^ textDocument/hover
|
||
|
||
@[inherit_doc]
|
||
infix:65 (name := myInfix) " >+< " => Nat.add
|
||
--^ textDocument/hover
|
||
--^ textDocument/hover
|
||
|
||
#check 1 >+< 2
|
||
--^ textDocument/hover
|
||
|
||
@[inherit_doc] notation "ℕ" => Nat
|
||
|
||
#check ℕ
|
||
--^ textDocument/hover
|
||
|
||
/-- My command -/
|
||
macro "mycmd" e:term : command => do
|
||
let seq ← `(Lean.Parser.Term.doSeq| $e:term)
|
||
--^ textDocument/hover
|
||
`(def hi := Id.run do $seq:doSeq)
|
||
--^ textDocument/hover
|
||
|
||
mycmd 1
|
||
--^ textDocument/hover
|
||
|
||
/-- My way better command -/
|
||
macro_rules
|
||
| `(mycmd $e) => `(@[inline] def hi := $e)
|
||
|
||
mycmd 1
|
||
--^ textDocument/hover
|
||
|
||
syntax "mycmd'" ppSpace sepBy1(term, " + ") : command
|
||
--^ textDocument/hover
|
||
--^ textDocument/hover
|
||
--^ textDocument/hover
|
||
|
||
/-- My ultimate command -/
|
||
elab_rules : command
|
||
| `(mycmd' $e) => do Lean.Elab.Command.elabCommand (← `(/-- hi -/ @[inline] def hi := $e))
|
||
|
||
mycmd' 1
|
||
--^ textDocument/hover
|
||
|
||
|
||
#check ({ a := }) -- should not show `sorry`
|
||
--^ textDocument/hover
|
||
|
||
example : True := by
|
||
simp [id True.intro]
|
||
--^ textDocument/hover
|
||
--^ textDocument/hover
|
||
|
||
|
||
example : Id Nat := do
|
||
let mut n := 1
|
||
n := 2
|
||
--^ textDocument/hover
|
||
n
|
||
|
||
|
||
opaque foo : Nat
|
||
|
||
#check _root_.foo
|
||
--^ textDocument/hover
|
||
|
||
namespace Bar
|
||
|
||
opaque foo : Nat
|
||
--^ textDocument/hover
|
||
|
||
#check _root_.foo
|
||
--^ textDocument/hover
|
||
|
||
def bar := 1
|
||
--^ textDocument/hover
|
||
|
||
structure Foo := mk ::
|
||
--^ textDocument/hover
|
||
--^ textDocument/hover
|
||
hi : Nat
|
||
--^ textDocument/hover
|
||
|
||
inductive Bar
|
||
--^ textDocument/hover
|
||
| mk : Bar
|
||
--^ textDocument/hover
|
||
|
||
instance : ToString Nat := ⟨toString⟩
|
||
--^ textDocument/hover
|
||
instance f : ToString Nat := ⟨toString⟩
|
||
--^ textDocument/hover
|
||
|
||
example : Type 0 := Nat
|
||
--^ textDocument/hover
|
||
|
||
def foo.bar : Nat := 1
|
||
--^ textDocument/hover
|
||
--^ textDocument/hover
|
||
|
||
end Bar
|
||
|
||
example : Nat → Nat → Nat :=
|
||
fun x y =>
|
||
--^ textDocument/hover
|
||
--v textDocument/definition
|
||
x
|
||
--^ textDocument/hover
|
||
|
||
-- textDocument/definition -- removed because the result is platform-dependent
|
||
set_option linter.unusedVariables false in
|
||
--^ textDocument/hover
|
||
example : Nat → Nat → Nat := by
|
||
intro x y
|
||
--^ textDocument/hover
|
||
--v textDocument/definition
|
||
exact x
|
||
--^ textDocument/hover
|
||
|
||
def g (n : Nat) : Nat := g 0
|
||
termination_by n
|
||
decreasing_by have n' := n; admit
|
||
--^ textDocument/hover
|
||
|
||
@[inline]
|
||
--^ textDocument/hover
|
||
def one := 1
|
||
|
||
example : True ∧ False := by
|
||
constructor
|
||
· constructor
|
||
--^ textDocument/hover
|
||
|
||
example : Nat := Id.run do (← 1)
|
||
--^ textDocument/hover
|
||
|
||
#check (· + ·)
|
||
--^ textDocument/hover
|
||
--^ textDocument/hover
|
||
/-- my_intro tactic -/
|
||
macro "my_intro" x:(ident <|> "_") : tactic =>
|
||
match x with
|
||
| `($x:ident) => `(tactic| intro $x:ident)
|
||
| _ => `(tactic| intro _%$x)
|
||
|
||
example : α → α := by intro x; assumption
|
||
--^ textDocument/hover
|
||
example : α → α := by intro _; assumption
|
||
--^ textDocument/hover
|
||
example : α → α := by my_intro x; assumption
|
||
--^ textDocument/hover
|
||
--v textDocument/hover
|
||
example : α → α := by my_intro _; assumption
|
||
--^ textDocument/hover
|
||
|
||
/-- my_intro term -/
|
||
def my_intro : Nat := 1
|
||
|
||
--v textDocument/hover
|
||
example : α → α := by my_intro _; assumption
|
||
|
||
attribute [simp] my_intro
|
||
--^ textDocument/hover
|
||
|
||
example : Nat → True := by
|
||
intro x
|
||
--^ textDocument/hover
|
||
cases x with
|
||
| zero => trivial
|
||
--^ textDocument/hover
|
||
--v textDocument/hover
|
||
| succ x => trivial
|
||
--^ textDocument/hover
|
||
|
||
example : Nat → True := by
|
||
intro x
|
||
--^ textDocument/hover
|
||
induction x with
|
||
--^ textDocument/hover
|
||
| zero => trivial
|
||
--^ textDocument/hover
|
||
--v textDocument/hover
|
||
| succ _ ih => exact ih
|
||
--^ textDocument/hover
|
||
|
||
example : Nat → Nat
|
||
--v textDocument/hover
|
||
| .zero => .zero
|
||
--^ textDocument/hover
|
||
--v textDocument/hover
|
||
| .succ x => .succ x
|
||
--^ textDocument/hover
|
||
|
||
example : Inhabited Nat := ⟨Nat.zero⟩
|
||
--^ textDocument/hover
|
||
--^ textDocument/hover
|
||
|
||
example : Nat :=
|
||
let x := match 0 with | _ => 0
|
||
_
|
||
--^ textDocument/hover
|
||
|
||
def auto (o : Nat := by exact 1) : Nat := o
|
||
--^ textDocument/hover
|
||
|
||
example : 1 = 1 := by
|
||
--v textDocument/hover
|
||
generalize _e : 1 = x
|
||
--^ textDocument/hover
|
||
exact Eq.refl x
|
||
|
||
example : 1 = 1 := by
|
||
cases _e : 1 with
|
||
--^ textDocument/hover
|
||
| zero => rfl
|
||
| succ x => rfl
|
||
--^ textDocument/hover
|
||
|
||
namespace Foo
|
||
|
||
export List (nil)
|
||
--^ textDocument/hover
|
||
open List (cons)
|
||
--^ textDocument/hover
|
||
open List hiding map
|
||
--^ textDocument/hover
|
||
--v textDocument/hover
|
||
open List renaming zip → zip'
|
||
--^ textDocument/hover
|
||
|
||
end Foo
|