[VsCoq1] Progress on #134: Use dune coq top (when enabled by a setting) #319

Blaisorblade · 2022-12-12T03:08:19Z

Address #134 for VsCoq1. The first commit fixes coq-community/vscoq-legacy#55.

This is a V0 prototype with some limitations, but it appears somewhat suitable for use.

There's no auto-detection of dune projects, but an explicit setting. Since it can be set per workspace, since most dune projects also have a _CoqProject file, and since dune coq top is probably somewhat experimental, I consider this sufficient for now.
If the build fails, this does not redirect build outputs/errors to some proper log window (beyond "Coq Language Server" logs).
User experience isn't great when dune decides to build code: a standard progress bar appears, but one must view "Coq Language Server" to understand what is happening.

What I tested was my integration branch — https://github.com/Blaisorblade/vscoq/tree/thread-count-option-misc.

Some unexpected messages appeared, but they seem due to the options added by dune coq top.

coqtop-stderr: Warning: Native compiler is disabled, -native-compiler ondemand option
ignored. [native-compiler-disabled,native-compiler]
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]

coqtop-stdout:Skipping rcfile loading.

The last one suggests that .coqrc is not being loaded, but it appears untrue — I used

Test Nested Proofs Allowed.
Test Ltac Backtrace.

to confirm my .coqrc settings were active.

Blaisorblade · 2022-12-12T03:35:35Z

package.json

        "coqtop.binPath": {
          "type": "string",
          "default": "",
-          "description": "Path to coqtop and coqidetop binaries (alternatively, hoqtop and hoqidetop)."
+          "description": "Path to folder with coqtop and coqidetop binaries (alternatively, hoqtop and hoqidetop)."


This is an unrelated message improvement.

package.json

Blaisorblade · 2022-12-17T20:23:00Z

This isn't complete but I've been using it for a while (must still rebase over 0.3.7).

I'd like to ask what would be considered necessary. The lack of a decent progress dialog seems the most annoying problem...

Blaisorblade · 2023-02-10T13:31:54Z

Bug report: this still passes flags from _CoqProject to Coq. That's one I can fix.

4ever2 · 2023-02-10T13:32:44Z

Doesn't this PR also fix coq-community/vscoq-legacy#55?

Blaisorblade · 2023-02-10T13:36:29Z

Yep, thanks @4ever2

thery · 2023-02-10T15:01:59Z

@Blaisorblade tell me when you think it is mergeable

huynhtrankhanh · 2023-02-10T15:07:05Z

This PR is not ready to merge I guess. But one nitpick: why should we continue using var? We should use const and let, and prefer const whenever possible. var is function scoped, not block scoped like the other two keywords. This is very inconsequential for this PR though.

I'll probably review this PR more carefully later.

server/src/coqtop/CoqTop8.ts

Blaisorblade · 2023-02-10T15:24:01Z

server/src/coqtop/CoqTop8.ts

+    if (uri.scheme == "file")
+      return uri.fsPath;
+    else
+      return undefined


This is new since last revision and enables stepping through unsaved files (but only outside dune coq top).

server/src/coqtop/CoqTop8.ts

Blaisorblade · 2023-02-10T15:46:31Z

server/src/coqtop/CoqTop8.ts

+      [this.settings.dunePath, ["coq", "top", "--toplevel=" + coqtopModule,
+        scriptPath, "--", ...coqArgs]] :
+      [coqtopModule, coqArgs]
+


@huynhtrankhanh Since the code relied on var's scoping, this seems the smallest possible change.

Had to lift error checking since TS seems to lack statement expressions, but I guess that's not too bad. I guess function () { ... } () lets you encode them, but I wouldn't know if that's idiomatic.

To be clear, if anything seems silly it's because I'm not really a TypeScript dev and I was following existing idioms.

Blaisorblade · 2023-02-10T16:01:27Z

I've done the main changes I planned, tried to address @huynhtrankhanh's comments, but I'll be retesting more later today.

Blaisorblade · 2023-02-13T09:44:42Z

The latest changes seem to work, and I addressed @huynhtrankhanh 's comments, so I consider this ready for review and merging.

thery · 2023-02-13T10:21:12Z

@Blaisorblade Perfect I will try to have a look at it today. Would be good if @huynhtrankhanh would give his opinion too

thery · 2023-02-13T13:56:23Z

server/src/CoqProject.ts

@@ -86,9 +86,12 @@ export class CoqProject {
      this.coqProjectRoot = newSettings.coq.coqProjectRoot;
      this.console.log("Updated project root to " + this.getCoqProjectRoot());
    }
-    if(newSettings.coq.loadCoqProject ) {
+    if(newSettings.coq.loadCoqProject && !newSettings.coqtop.useDune) {


does this means that if your flag is not set, everything works like as before?

Yes, that was my design goal :-).

thery · 2023-02-13T13:56:51Z

@Blaisorblade I had a look, it seems ok.
As soon as @huynhtrankhanh is ok, we can merge

huynhtrankhanh · 2023-02-13T14:11:15Z

This PR looks perfect. I really appreciate your work. However, there's one issue: the configuration options! There are two options here, which should be mutually exclusive: coqtop.loadCoqProject and coqtop.useDune. I believe having two mutually exclusive options that could be set independently causes problems when we further build upon your work and makes it hard for users to predict the effect of their configuration. Should we have a single option that allows us to choose whether to load _CoqProject, use Dune or ignore both?

thery · 2023-02-13T14:24:36Z

@huynhtrankhanh you would prefer a coqtop.configMode with the options coqproject or dune?

Blaisorblade · 2023-02-13T15:50:05Z

Thanks for the review!

Should we have a single option that allows us to choose whether to load _CoqProject, use Dune or ignore both?

Good idea; that works for me. I'm afraid I can get back to it in a couple days.

Dropping "ignore both" as @thery suggests also seems plausible but has a slightly higher chances of regressions — does any user need to disable loadCoqProject? We should at least test projects with no _CoqProject file.

thery · 2023-02-18T23:19:08Z

@Blaisorblade @huynhtrankhanh I would like to make a new release beginning of march, do you think we can make this PR ready to merge by then?

This also allows stepping through unsaved files; before this patch, we passed `-topfile untitled:Untitled-1`, which failed with: ``` coqtop-stderr: Error: Invalid character ':' in identifier "untitled:Untitled-1". ```

- Add `coqtop.useDune` and dune path to settings. - spawnCoqTop: use dune coq top - Skip `_CoqProject` when `useDune` is set. - Address review: Switch new code to const as requested

Blaisorblade · 2023-04-11T19:53:00Z

Sorry I'm late — I plan to address the comment next week, what I pushed just updates the extension for dune coq top changes (now dune wants relative paths, so we oblige).

thery · 2023-09-28T10:51:59Z

what is the status of this PR?

Blaisorblade · 2023-10-12T03:37:09Z

Sorry this hasn't progressed :-| ... Closing for now.

Blaisorblade commented Dec 12, 2022

View reviewed changes

Blaisorblade marked this pull request as ready for review December 17, 2022 20:14

Blaisorblade force-pushed the dune-coq-top branch from d41bd49 to 18cce19 Compare December 21, 2022 19:54

Blaisorblade force-pushed the dune-coq-top branch from 18cce19 to d900683 Compare January 16, 2023 21:59

Blaisorblade changed the title ~~Use dune coq top (when enabled by a setting)~~ Fix #134 for VsCoq1: Use dune coq top (when enabled by a setting) Feb 10, 2023

Blaisorblade requested review from huynhtrankhanh and thery February 10, 2023 13:16

Blaisorblade changed the title ~~Fix #134 for VsCoq1: Use dune coq top (when enabled by a setting)~~ Progress on #134 for VsCoq1: Use dune coq top (when enabled by a setting) Feb 10, 2023

Blaisorblade force-pushed the dune-coq-top branch 3 times, most recently from ae99c7e to 8564194 Compare February 10, 2023 14:58

huynhtrankhanh suggested changes Feb 10, 2023

View reviewed changes

server/src/coqtop/CoqTop8.ts Outdated Show resolved Hide resolved

Blaisorblade commented Feb 10, 2023

View reviewed changes

server/src/coqtop/CoqTop8.ts Outdated Show resolved Hide resolved

Blaisorblade commented Feb 10, 2023

View reviewed changes

Blaisorblade mentioned this pull request Feb 10, 2023

Error message location messed up in the presence of CRLF #339

Closed

Blaisorblade force-pushed the dune-coq-top branch from faf3152 to eb5e9ec Compare February 11, 2023 18:21

thery approved these changes Feb 13, 2023

View reviewed changes

maximedenes changed the title ~~Progress on #134 for VsCoq1: Use dune coq top (when enabled by a setting)~~ [VsCoq1] Progress on #134: Use dune coq top (when enabled by a setting) Feb 14, 2023

Blaisorblade added 9 commits April 11, 2023 21:45

spawnCoqTop: Move existing code to spread syntax

bd136c3

Fix #278: pass correct -topfile argument

1c99c26

This also allows stepping through unsaved files; before this patch, we passed `-topfile untitled:Untitled-1`, which failed with: ``` coqtop-stderr: Error: Invalid character ':' in identifier "untitled:Untitled-1". ```

coqtop.binPath: Improve description

82edfc6

Dune CoqTop: fix setting loading when skipping _CoqProject

af9df54

Fix coq#134: Use dune coq top when enabled by a setting.

7368bf7

- Add `coqtop.useDune` and dune path to settings. - spawnCoqTop: use dune coq top - Skip `_CoqProject` when `useDune` is set. - Address review: Switch new code to const as requested

spawnCoqTop: refactor pre-existing code to use const

59bf33c

Pass relative path to dune, as required by recent versions

190e2c6

WIP logging

e53304e

WIP New setting (still unused)

5e6ed44

Blaisorblade force-pushed the dune-coq-top branch from 89bba8c to 5e6ed44 Compare April 11, 2023 19:51

4ever2 mentioned this pull request Sep 11, 2023

[VsCoq1] Fix IP issue with VS Code 1.82.0 #614

Merged

Blaisorblade closed this Oct 12, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[VsCoq1] Progress on #134: Use dune coq top (when enabled by a setting) #319

[VsCoq1] Progress on #134: Use dune coq top (when enabled by a setting) #319

Blaisorblade commented Dec 12, 2022 •

edited

Loading

Blaisorblade Dec 12, 2022

Blaisorblade commented Dec 17, 2022

Blaisorblade commented Feb 10, 2023

4ever2 commented Feb 10, 2023

Blaisorblade commented Feb 10, 2023

thery commented Feb 10, 2023

huynhtrankhanh commented Feb 10, 2023

Blaisorblade Feb 10, 2023

Blaisorblade Feb 10, 2023

Blaisorblade Feb 10, 2023

Blaisorblade commented Feb 10, 2023

Blaisorblade commented Feb 13, 2023

thery commented Feb 13, 2023

thery Feb 13, 2023

Blaisorblade Feb 13, 2023

thery commented Feb 13, 2023

huynhtrankhanh commented Feb 13, 2023 •

edited

Loading

thery commented Feb 13, 2023

Blaisorblade commented Feb 13, 2023

thery commented Feb 18, 2023

Blaisorblade commented Apr 11, 2023

thery commented Sep 28, 2023

Blaisorblade commented Oct 12, 2023

[VsCoq1] Progress on #134: Use dune coq top (when enabled by a setting) #319

[VsCoq1] Progress on #134: Use dune coq top (when enabled by a setting) #319

Conversation

Blaisorblade commented Dec 12, 2022 • edited Loading

Blaisorblade Dec 12, 2022

Choose a reason for hiding this comment

Blaisorblade commented Dec 17, 2022

Blaisorblade commented Feb 10, 2023

4ever2 commented Feb 10, 2023

Blaisorblade commented Feb 10, 2023

thery commented Feb 10, 2023

huynhtrankhanh commented Feb 10, 2023

Blaisorblade Feb 10, 2023

Choose a reason for hiding this comment

Blaisorblade Feb 10, 2023

Choose a reason for hiding this comment

Blaisorblade Feb 10, 2023

Choose a reason for hiding this comment

Blaisorblade commented Feb 10, 2023

Blaisorblade commented Feb 13, 2023

thery commented Feb 13, 2023

thery Feb 13, 2023

Choose a reason for hiding this comment

Blaisorblade Feb 13, 2023

Choose a reason for hiding this comment

thery commented Feb 13, 2023

huynhtrankhanh commented Feb 13, 2023 • edited Loading

thery commented Feb 13, 2023

Blaisorblade commented Feb 13, 2023

thery commented Feb 18, 2023

Blaisorblade commented Apr 11, 2023

thery commented Sep 28, 2023

Blaisorblade commented Oct 12, 2023

Blaisorblade commented Dec 12, 2022 •

edited

Loading

huynhtrankhanh commented Feb 13, 2023 •

edited

Loading