Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Goal not updating after intros #197

Closed
Alizter opened this issue Jan 19, 2023 · 1 comment · Fixed by #200 or ocaml/opam-repository#23181
Closed

Goal not updating after intros #197

Alizter opened this issue Jan 19, 2023 · 1 comment · Fixed by #200 or ocaml/opam-repository#23181
Milestone
0.1.4

Comments

@Alizter
Copy link
Collaborator

Alizter commented Jan 19, 2023

Here is an example of the goal not updating after an intros statement together with some unicode characters.

Axiom P : nat -> Prop.
Axiom foo : forall {n}, P (S n) -> P n.
Ltac foo := apply foo.
Infix "⊆" := lt (at level 10).

Goal forall Γ Δ, Γ ⊆ Δ -> P Γ.
intros Γ Δ s.
foo.

Cursor is first before the intros.
image

Cursor is after the terminating . and the goal has not updated.
image

Next line the goal updates.
image

Notice the correct behaviour when the cursor is after the terminating . for foo.
image
@ejgallego
Copy link
Owner

That's the same than #193, thanks. The server is not translating Coq locations to LSP locations properly.

In particular, once we store Range.t (properly converted) in Fleche.Doc.t, then things will work fine automatically.

@ejgallego ejgallego added this to the 0.1.4 milestone Jan 19, 2023
@ejgallego ejgallego mentioned this issue Jan 19, 2023
Merged
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Beginnings of Unicode Support
7aa5160 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Should fix #193 and #197

TODO:

- more principled conversion on `Coq.Protect
- see what is going on with the loc-independent cache (seems already
  broken in terms of space shifting)?
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Beginnings of Unicode Support
c93dff0 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Should fix #193 and #197

TODO:

- more principled conversion on `Coq.Protect
- see what is going on with the loc-independent cache (seems already
  broken in terms of space shifting)?
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Beginnings of Unicode Support
83f0129 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Should fix #193 and #197

TODO:

- more principled conversion on `Coq.Protect
- see what is going on with the loc-independent cache (seems already
  broken in terms of space shifting)?
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Beginnings of Unicode Support
e786b66 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Should fix #193 and #197

TODO:

- more principled conversion on `Coq.Protect
- see what is going on with the loc-independent cache (seems already
  broken in terms of space shifting)?
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Beginnings of Unicode Support
83c7cdd 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Should fix #193 and #197

TODO:

- more principled conversion on `Coq.Protect
- see what is going on with the loc-independent cache (seems already
  broken in terms of space shifting)?
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Beginnings of Unicode Support
9549f57 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Should fix #193 and #197

TODO:

- see what is going on with the loc-independent cache (seems already
  broken in terms of space shifting)?
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Beginnings of Unicode Support
e6b8d4e 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq;
we do this in a principled way, but the whole business is often
delicate.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Fixes #193 , fixes #197 .
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Beginnings of Unicode Support
25cf141 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq;
we do this in a principled way, but the whole business is often
delicate.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Fixes #193 , fixes #197 .
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Beginnings of Unicode Support
b961670 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq;
we do this in a principled way, but the whole business is often
delicate.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Fixes #193 , fixes #197 .
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Beginnings of Unicode Support
5742a44 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq;
we do this in a principled way, but the whole business is often
delicate.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Fixes #193 , fixes #197 .
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Beginnings of Unicode Support
c2b1a37 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq;
we do this in a principled way, but the whole business is often
delicate.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Fixes #193 , fixes #197 .
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Beginnings of Unicode Support
f467687 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq;
we do this in a principled way, but the whole business is often
delicate.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Fixes #193 , fixes #197 .
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Unicode Support
52b0fc8 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq;
we do this in a principled way, but the whole business is often
delicate.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Fixes #193 , fixes #197 .
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Unicode Support
07cdb97 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq;
we do this in a principled way, but the whole business is often
delicate.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Fixes #193 , fixes #197 .
ejgallego added a commit that referenced this issue Jan 19, 2023
@ejgallego
[coq] [fleche] Unicode Support
3ed7625 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq;
we do this in a principled way, but the whole business is often
delicate.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Fixes #193 , fixes #197 .
ejgallego added a commit that referenced this issue Jan 20, 2023
@ejgallego
[coq] [fleche] Unicode Support
91a573a 
We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq;
we do this in a principled way, but the whole business is often
delicate.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Fixes #193 , fixes #197 .
@ejgallego ejgallego mentioned this issue Jan 29, 2023
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Jan 29, 2023
@ejgallego
[new release] coq-lsp (0.1.4+v8.16)
e05654b 
CHANGES:

---------------------

 - Support for OCaml 4.11 (@ejgallego, ejgallego/coq-lsp#184)
 - The keybinding alt+enter in VSCode is now correctly scoped to be
   only active on Coq files (@artagnon, ejgallego/coq-lsp#188)
 - Support Unicode files (@ejgallego, ejgallego/coq-lsp#200, fixes ejgallego/coq-lsp#193, fixes ejgallego/coq-lsp#197)
 - The info view is now script enabled and does client-side
   rendering. It is also now bundled with esbuild as part of the build
   process (@artagnon, @ejgallego, ejgallego/coq-lsp#171)
 - The no-op `--std` argument to the `coq-lsp` binary has been
   removed, beware of your setup in the extension settings
   (@ejgallego, ejgallego/coq-lsp#208)
 - Settings for the VSCode extension are now categorized (@Alizter, ejgallego/coq-lsp#212)
 - `GoalAnswer`s now include the proof "stack" and better hypothesis
   information, changes are compatible with 0.1.3 `GoalAnswer` version
   (@ejgallego, ejgallego/coq-lsp#237)
 - Focus is now preserved when the info view pops up (@artagnon, ejgallego/coq-lsp#242,
   fixes ejgallego/coq-lsp#224)
 - In `_CoqProject`, `-impredicative-set` is now parsed correctly
   (@artagnon, ejgallego/coq-lsp#241)
 - InfoView is not written in React (@ejgallego, ejgallego/coq-lsp#223)
 - `debug` option in the client / protocol that will enable Coq's backtraces
   (@Alizter, @ejgallego, ejgallego/coq-lsp#217, ejgallego/coq-lsp#248)
 - Full document stats are now correctly computed on checking
   resumption, still cached sentences will display the cached timing
   tho (@ejgallego, ejgallego/coq-lsp#257)
 - Set Coq library name correctly (@ejgallego, ejgallego/coq-lsp#260)
 - `_CoqProject` file is now detected using LSP client `rootPath`
   (@ejgallego, ejgallego/coq-lsp#261)
 - Press `\` to trigger Unicode completion by the server. This
   behavior is configurable, with "off", "regular", and extended
   settings (@artagnon, @Alizter, ejgallego, ejgallego/coq-lsp#219).
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Jan 29, 2023
@ejgallego
[new release] coq-lsp (0.1.4+v8.16)
6554f83 
CHANGES:

---------------------

 - Support for OCaml 4.11 (@ejgallego, ejgallego/coq-lsp#184)
 - The keybinding alt+enter in VSCode is now correctly scoped to be
   only active on Coq files (@artagnon, ejgallego/coq-lsp#188)
 - Support Unicode files (@ejgallego, ejgallego/coq-lsp#200, fixes ejgallego/coq-lsp#193, fixes ejgallego/coq-lsp#197)
 - The info view is now script enabled and does client-side
   rendering. It is also now bundled with esbuild as part of the build
   process (@artagnon, @ejgallego, ejgallego/coq-lsp#171)
 - The no-op `--std` argument to the `coq-lsp` binary has been
   removed, beware of your setup in the extension settings
   (@ejgallego, ejgallego/coq-lsp#208)
 - Settings for the VSCode extension are now categorized (@Alizter, ejgallego/coq-lsp#212)
 - `GoalAnswer`s now include the proof "stack" and better hypothesis
   information, changes are compatible with 0.1.3 `GoalAnswer` version
   (@ejgallego, ejgallego/coq-lsp#237)
 - Focus is now preserved when the info view pops up (@artagnon, ejgallego/coq-lsp#242,
   fixes ejgallego/coq-lsp#224)
 - In `_CoqProject`, `-impredicative-set` is now parsed correctly
   (@artagnon, ejgallego/coq-lsp#241)
 - InfoView is not written in React (@ejgallego, ejgallego/coq-lsp#223)
 - `debug` option in the client / protocol that will enable Coq's backtraces
   (@Alizter, @ejgallego, ejgallego/coq-lsp#217, ejgallego/coq-lsp#248)
 - Full document stats are now correctly computed on checking
   resumption, still cached sentences will display the cached timing
   tho (@ejgallego, ejgallego/coq-lsp#257)
 - Set Coq library name correctly (@ejgallego, ejgallego/coq-lsp#260)
 - `_CoqProject` file is now detected using LSP client `rootPath`
   (@ejgallego, ejgallego/coq-lsp#261)
 - You can press `\` to trigger Unicode completion by the server. This
   behavior is configurable, with "off", "regular", and "extended"
   settings (@artagnon, @Alizter, ejgallego, ejgallego/coq-lsp#219).
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Jan 29, 2023
@ejgallego
[new release] coq-lsp (0.1.4+v8.16)
1b58197 
CHANGES:

---------------------

 - Support for OCaml 4.11 (@ejgallego, ejgallego/coq-lsp#184)
 - The keybinding alt+enter in VSCode is now correctly scoped to be
   only active on Coq files (@artagnon, ejgallego/coq-lsp#188)
 - Support Unicode files (@ejgallego, ejgallego/coq-lsp#200, fixes ejgallego/coq-lsp#193, fixes ejgallego/coq-lsp#197)
 - The info view is now script enabled and does client-side
   rendering. It is also now bundled with esbuild as part of the build
   process (@artagnon, @ejgallego, ejgallego/coq-lsp#171)
 - The no-op `--std` argument to the `coq-lsp` binary has been
   removed, beware of your setup in the extension settings
   (@ejgallego, ejgallego/coq-lsp#208)
 - Settings for the VSCode extension are now categorized (@Alizter, ejgallego/coq-lsp#212)
 - `GoalAnswer`s now include the proof "stack" and better hypothesis
   information, changes are compatible with 0.1.3 `GoalAnswer` version
   (@ejgallego, ejgallego/coq-lsp#237)
 - Focus is now preserved when the info view pops up (@artagnon, ejgallego/coq-lsp#242,
   fixes ejgallego/coq-lsp#224)
 - In `_CoqProject`, `-impredicative-set` is now parsed correctly
   (@artagnon, ejgallego/coq-lsp#241)
 - InfoView is not written in React (@ejgallego, ejgallego/coq-lsp#223)
 - `debug` option in the client / protocol that will enable Coq's backtraces
   (@Alizter, @ejgallego, ejgallego/coq-lsp#217, ejgallego/coq-lsp#248)
 - Full document stats are now correctly computed on checking
   resumption, still cached sentences will display the cached timing
   tho (@ejgallego, ejgallego/coq-lsp#257)
 - Set Coq library name correctly (@ejgallego, ejgallego/coq-lsp#260)
 - `_CoqProject` file is now detected using LSP client `rootPath`
   (@ejgallego, ejgallego/coq-lsp#261)
 - You can press `\` to trigger Unicode completion by the server. This
   behavior is configurable, with "off", "regular", and "extended"
   settings (@artagnon, @Alizter, ejgallego, ejgallego/coq-lsp#219).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
0.1.4
2 participants
@ejgallego @Alizter