Stream: VsCoq devs & users

Topic: imported from gitter room coq-community/vscoq


view this post on Zulip Odomontois (Gitter import) (Sep 16 2019 at 08:16):

So there aren't a lot of discussions here

view this post on Zulip Odomontois (Gitter import) (Sep 16 2019 at 08:17):

Can someone guide a noob how to try the plugin locally?

view this post on Zulip Maxime Dénès (Sep 16 2019 at 10:00):

hi! the room is fairly new ;)

view this post on Zulip Maxime Dénès (Sep 16 2019 at 10:00):

for a noob, I'd recommend to wait for a few days that we do a marketplace release

view this post on Zulip Maxime Dénès (Sep 16 2019 at 10:01):

but if you really can't wait, you can build the plugin and use vscode --install-extension on the produced .vsix file

view this post on Zulip Brendan Zabarauskas (Gitter import) (Sep 16 2019 at 10:20):

"wait for a few days" :heart_eyes: :heart_eyes: :heart_eyes:

view this post on Zulip Théo Winterhalter (Sep 18 2019 at 12:50):

Hi, thanks a lot. Are you looking for feedbacks from users? For me the main drawback is that I have to open an instance for each _CoqProject I have in my project to have it at the root.
Otherwise I'm impressed, and in several respects it's better than Proof General, so thanks again.

view this post on Zulip Maxime Dénès (Sep 18 2019 at 14:16):

Are you looking for feedbacks from users?

Sure!

For me the main drawback is that I have to open an instance for each _CoqProject I have in my project to have it at the root.

Good point. I believe VsCode has a notion of multi root projects, but I still haven't explored it.

view this post on Zulip Théo Winterhalter (Sep 18 2019 at 14:17):

Ok, good to know. :)

view this post on Zulip Maxime Dénès (Sep 18 2019 at 14:27):

Thanks for the feedback!

view this post on Zulip Théo Winterhalter (Sep 18 2019 at 15:44):

Also, whenever I use the shortcuts to compile, I get a motherboard beep, even when it succeeds.

view this post on Zulip Maxime Dénès (Sep 18 2019 at 15:45):

oh! which shortcuts do you mean?

view this post on Zulip Théo Winterhalter (Sep 18 2019 at 15:48):

"Interpret to point" and "Step forward" (maybe it's only on macOS where they are ctrl + command + arrow).

view this post on Zulip Maxime Dénès (Sep 18 2019 at 15:54):

ah! yeah, it must be platform-dependent, I don't have this problem under Linux

view this post on Zulip Maxime Dénès (Sep 18 2019 at 15:54):

we should probably change the default bindings on macOS then

view this post on Zulip Maxime Dénès (Sep 18 2019 at 15:54):

don't hesitate to open a PR, if you find some keybindings that work better

view this post on Zulip Maxime Dénès (Sep 18 2019 at 15:55):

they are defined around here: https://github.com/coq-community/vscoq/blob/d298a4ef686a0f69060ad16ef4a058717d20c8e7/client/package.json#L342

view this post on Zulip Théo Winterhalter (Sep 18 2019 at 15:55):

Yeah, I'll think about it. What is the bindng on linux where there is no command?

view this post on Zulip Théo Winterhalter (Sep 18 2019 at 15:55):

Ok!

view this post on Zulip Maxime Dénès (Sep 18 2019 at 15:56):

on Linux, it's ALT instead of command

view this post on Zulip Maxime Dénès (Sep 18 2019 at 15:56):

although the navigation ones are just ALT + key (no CTRL), otherwise it clashes with some desktop environments like gnome

view this post on Zulip Théo Winterhalter (Sep 18 2019 at 15:58):

Yeah, there's that to think about. I don't think ctrl + alt + arrow does much on macOS so that might be an option.

view this post on Zulip Maxime Dénès (Sep 18 2019 at 16:01):

but as you can see in the file, we can define each binding per platform

view this post on Zulip Maxime Dénès (Sep 18 2019 at 16:01):

so we are quite free in the choice

view this post on Zulip Théo Winterhalter (Sep 19 2019 at 13:26):

It might be related to your issue, but where is the information about remaining obligations supposed to be displayed?

view this post on Zulip Maxime Dénès (Sep 19 2019 at 13:29):

you mean when using Program?

view this post on Zulip Théo Winterhalter (Sep 19 2019 at 13:29):

Yes (or Equations in my case).

view this post on Zulip Maxime Dénès (Sep 19 2019 at 13:29):

hmm not sure, let me test it

view this post on Zulip Théo Winterhalter (Sep 19 2019 at 13:29):

I can blindly type Next Obligation.

view this post on Zulip Théo Winterhalter (Sep 19 2019 at 13:30):

Thanks.

view this post on Zulip Maxime Dénès (Sep 19 2019 at 13:32):

indeed I don't see them

view this post on Zulip Maxime Dénès (Sep 19 2019 at 13:32):

would you mind opening an issue? I'll try to fix it.

view this post on Zulip Théo Winterhalter (Sep 19 2019 at 13:32):

Ok!

view this post on Zulip Matthieu Sozeau (Sep 23 2019 at 11:57):

@Théo Winterhalter How did you call vscode under OS X (I installed the .app, I suppose you did as well)

view this post on Zulip Matthieu Sozeau (Sep 23 2019 at 12:20):

Found it: using option "install code in PATH"

view this post on Zulip vlj (Sep 23 2019 at 17:13):

Is vscoq still maintained ? Last commit is from 2 years ago, and pr seems not examinated

view this post on Zulip Maxime Dénès (Sep 23 2019 at 17:49):

it is maintained here: https://github.com/coq-community/vscoq

view this post on Zulip vlj (Sep 23 2019 at 17:50):

Thanks !

view this post on Zulip Maxime Dénès (Sep 23 2019 at 17:50):

we haven't released a new version based on this fork, though

view this post on Zulip Maxime Dénès (Sep 23 2019 at 17:51):

hopefully this week!

view this post on Zulip Paolo Giarrusso (Sep 24 2019 at 15:45):

@Maxime Dénès It seems 'Open proof view" doesn't reopen the view any more, once I close it...

view this post on Zulip Maxime Dénès (Sep 24 2019 at 16:04):

ah! it is true that I haven't tested in since the switch to webview

view this post on Zulip Maxime Dénès (Sep 24 2019 at 16:04):

would you mind opening an issue? I'll try to fix it

view this post on Zulip vlj (Sep 24 2019 at 17:51):

@Maxime Dénès do you have some build instruction ? Or are they the same as previously ? I tried to hack the extension last year but I had to remove/upgrade some things in the package.yml before

view this post on Zulip vlj (Sep 24 2019 at 20:04):

client code seems compatible with typescript 3+, but not the ones in html_views and server

view this post on Zulip Matthieu Sozeau (Sep 24 2019 at 20:14):

I'm quite impressed with the editor and functionality, great job @Maxime Dénès (and Christian J. Bell before)

view this post on Zulip Paolo Giarrusso (Sep 24 2019 at 20:34):

@vlj make seems to do the job here

view this post on Zulip Paolo Giarrusso (Sep 24 2019 at 20:35):

You'll then need https://code.visualstudio.com/docs/editor/extension-gallery#_install-from-a-vsix for installing @vlj

view this post on Zulip vlj (Sep 24 2019 at 20:50):

ok thanks

view this post on Zulip vlj (Sep 24 2019 at 20:50):

do you know how to run the tests ?

view this post on Zulip Paolo Giarrusso (Sep 25 2019 at 11:22):

No, but I'd look into running npm test, maybe in the folders with a test directory? npm test in server does something, but seems to fail very early?

view this post on Zulip Paolo Giarrusso (Sep 25 2019 at 11:23):

Error: Connection input stream is not set. Use arguments of createConnection or set command line parameters: '--node-ipc', '--stdio' or '--socket={number}'

view this post on Zulip Maxime Dénès (Sep 25 2019 at 11:37):

I'm quite impressed with the editor and functionality, great job Maxime Dénès (and Christian J. Bell before)

Thanks a lot, @Matthieu Sozeau. Hopefully, this is just the beginning ;)

view this post on Zulip Maxime Dénès (Sep 25 2019 at 11:37):

do you know how to run the tests ?

I haven't updated the tests, so I imagine they must be completely outdated.

view this post on Zulip Maxime Dénès (Sep 25 2019 at 11:39):

I don't think we want to invest energy there at this time, at least not for the server-side, since we are going to re-architect a lot of things including inside Coq.

view this post on Zulip Théo Winterhalter (Sep 25 2019 at 11:41):

I'm experiencing a new problem on my side, in one of my files, stepping forward/backward or to point takes some time after I started writing something. It only happens in this one file (other files of the project don't seem to have this problem).
It's a bit hard to identify though…

view this post on Zulip Matthieu Sozeau (Sep 25 2019 at 13:17):

Are there a lot of Equations / Program in between the points ?

view this post on Zulip Matthieu Sozeau (Sep 25 2019 at 13:18):

It might be that the STM has more trouble handling these (just a guess)

view this post on Zulip Théo Winterhalter (Sep 25 2019 at 13:40):

No, it's not this.
The only thing I see is that I'm close to heavy unicode character expressions. Now that I'm working further in the file, the issue no longer appears.

view this post on Zulip vlj (Sep 25 2019 at 19:47):

@Maxime Dénès is it ok to submit a PR that port the code to typescript 3 ? With typescript 3 you can have a single "main" project and client, html_views, servers behaving as subproject, which in turn simplify the dev dependencies/ scripts/... since they are shared

view this post on Zulip Maxime Dénès (Sep 26 2019 at 07:25):

@vlj sounds very good, I had also planned to use webpack for the main project, instead of just html_views

view this post on Zulip Maxime Dénès (Sep 26 2019 at 07:28):

I'm experiencing a new problem on my side, in one of my files, stepping forward/backward or to point takes some time after I started writing something. It only happens in this one file (other files of the project don't seem to have this problem).
It's a bit hard to identify though…

If it is reproducible, even with some dependencies, feel free to open an issue, I can investigate.

view this post on Zulip Théo Winterhalter (Sep 26 2019 at 08:07):

@Maxime Dénès I'll try to make a smaller example than metacoq. :)

view this post on Zulip Théo Winterhalter (Sep 26 2019 at 17:06):

I’m wondering if it might be related to autocomplete/suggestions.
It seems to be waiting for the window to popup before stepping.

Unrelated, there is nothing that displays when goals are shelved. Only the error at Qed time.

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 12:55):

It seems vscode does not work with 8.9.0, is that expected?

view this post on Zulip Maxime Dénès (Sep 27 2019 at 14:15):

it is not expected, but it hasn't been tested much

view this post on Zulip Maxime Dénès (Sep 27 2019 at 14:15):

do you get an error message ?

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 14:33):

Nope, I couldn't gather anything. the coqidetop and proof worker are apparently running but nothing happens in the UI

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 14:33):

No problems with 8.8.2 that I've been using (and @Théo Winterhalter as well)

view this post on Zulip Maxime Dénès (Sep 27 2019 at 14:40):

I can make 8.9.1 work here

view this post on Zulip Maxime Dénès (Sep 27 2019 at 14:40):

I can try 8.9.0

view this post on Zulip Maxime Dénès (Sep 27 2019 at 14:41):

if you look at the "output" tab and select "Coq Language Server", do you see anything?

view this post on Zulip Maxime Dénès (Sep 27 2019 at 14:50):

ah no but wait, my test was wrong

view this post on Zulip Maxime Dénès (Sep 27 2019 at 14:52):

this time, I confirm it works for me even with 8.9.0

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 15:08):

Ok, I'll try again

view this post on Zulip Paolo Giarrusso (Sep 27 2019 at 15:34):

Fwiw, the released vscoq works up to 8.8 (with old vscode), any chance that's what you installed?

view this post on Zulip Maxime Dénès (Sep 27 2019 at 15:36):

good point!

view this post on Zulip Maxime Dénès (Sep 27 2019 at 16:25):

it's probably time to make a release to avoid this confusion

view this post on Zulip Maxime Dénès (Sep 27 2019 at 16:25):

we can fix the remaining problems afterwards

view this post on Zulip vlj (Sep 28 2019 at 16:21):

do you have any idea how to retrieve the os in typescript ? using maybe vscode api

view this post on Zulip vlj (Sep 28 2019 at 18:14):

actually it's not necessary, vscode launch .exe even without extension on windows which is nice

view this post on Zulip vlj (Sep 28 2019 at 21:10):

@Maxime Dénès I opened a PR : https://github.com/coq-community/vscoq/pull/64 feel free to add comments so that I can update the code before merging

view this post on Zulip Matthieu Sozeau (Sep 29 2019 at 11:16):

Coq cannot find coqidetop when only coqidetop.opt and coqidetop.bc are installed (when building Coq locally using dune). I don't see how to configure that

view this post on Zulip Matthieu Sozeau (Sep 29 2019 at 11:16):

The workaround I use is to ln -s coqidetop.opt coqidetop but that's quickly getting old :)

view this post on Zulip vlj (Sep 29 2019 at 14:23):

@Maxime Dénès about https://github.com/coq-community/vscoq/pull/64#pullrequestreview-294671858 I changed the way we generate the css and js path, it uses the uri + .with scheme, I saw in the webview sample git history that it was the previous way of doing (https://github.com/microsoft/vscode-extension-samples/commit/708bc3090845be767c92b0fe53fe855a0fdca985), the .AsWebviewUri function was apparently added quite recently to the vscode api.

view this post on Zulip vlj (Sep 29 2019 at 14:24):

with previous way it seems to work

view this post on Zulip vlj (Sep 29 2019 at 21:11):

when webpacking client I think I hit this issue : https://github.com/Microsoft/vscode/issues/70308 (ie error code 1 when starting server)

view this post on Zulip vlj (Sep 29 2019 at 21:15):

another info https://github.com/microsoft/vscode-extension-samples/issues/191

view this post on Zulip Maxime Dénès (Sep 30 2019 at 06:45):

@vlj I see, wasn't aware of it. Maybe we should wait to get an upstream update on this issue, then.

view this post on Zulip vlj (Sep 30 2019 at 18:51):

the README.md files are the same in root directory and client ones ?

view this post on Zulip vlj (Sep 30 2019 at 19:41):

is there a way to ask coqtop to dump all the theorem/definition it has currently in its context ?

view this post on Zulip Maxime Dénès (Oct 03 2019 at 08:54):

@Matthieu Sozeau VsCoq should now work fine with a Dune-built Coq

view this post on Zulip Maxime Dénès (Oct 03 2019 at 11:58):

I just did a marketplace release. It is my first one, so I'm expecting some issues. Feedback is very welcome: https://marketplace.visualstudio.com/items?itemName=maximedenes.vscoq

view this post on Zulip Anton Trunov (Oct 03 2019 at 11:58):

Hooray!

view this post on Zulip Jad Hamza (Gitter import) (Oct 03 2019 at 12:58):

@Maxime Dénès Thanks for the release! I'm eager to try it, however I'm having an issue: https://gist.github.com/jad-hamza/133698e142367e805025be85c440380b

view this post on Zulip Jad Hamza (Gitter import) (Oct 03 2019 at 12:59):

(I also tried compiling the extension from master)

view this post on Zulip Brendan Zabarauskas (Gitter import) (Oct 03 2019 at 13:18):

Woo, congratulations on the release! :tada:

view this post on Zulip Maxime Dénès (Oct 03 2019 at 14:08):

@Brendan Zabarauskas Thanks!

view this post on Zulip Maxime Dénès (Oct 03 2019 at 14:09):

@Jad Hamza do you have a coqidetop.opt in the same directory as coqtop?

view this post on Zulip Jad Hamza (Gitter import) (Oct 03 2019 at 14:15):

@Maxime Dénès I'm now trying with a fresh install with coq dev (from opam), and I have both of these in my path. However now I'm getting coqtop is not running in the status bar

view this post on Zulip Jad Hamza (Gitter import) (Oct 03 2019 at 14:27):

@Maxime Dénès In the console, now I see it's calling coqidetop.opt -main-channel 127.0.0.1:port1:port2 -control-channel 127.0.0.1:port3:port4 -async-proofs on -Q . MyProject -R . Top, and then an error saying coqtop-stderr: Don't know what to do with -R . Top

view this post on Zulip Jad Hamza (Gitter import) (Oct 03 2019 at 14:51):

I reinstalled the extension and I'm not having this last error with coqtop is not running, but still having the original one with Message: Request textDocument/documentSymbol failed unexpectedly without providing any details.

view this post on Zulip Maxime Dénès (Oct 03 2019 at 15:03):

and then an error saying coqtop-stderr: Don't know what to do with -R . Top

This looks like the real problem, but it is super strange

view this post on Zulip Maxime Dénès (Oct 03 2019 at 15:03):

why would Coq not recognize a -R flag?

view this post on Zulip Maxime Dénès (Oct 03 2019 at 15:04):

what do you have in your _CoqProject?

view this post on Zulip Jad Hamza (Gitter import) (Oct 03 2019 at 15:13):

I have the -Q . MyProject

view this post on Zulip Jad Hamza (Gitter import) (Oct 03 2019 at 16:49):

I guess it recognizes the -R flag but doesn't know what to do with it because there is already -Q

view this post on Zulip Maxime Dénès (Oct 03 2019 at 18:21):

I can't reproduce it, though. coqtop accepts -Q followed by -R

view this post on Zulip Maxime Dénès (Oct 03 2019 at 18:24):

could you post the full content of your _CoqProject file in a gist?

view this post on Zulip Jad Hamza (Gitter import) (Oct 04 2019 at 05:18):

@Maxime Dénès it is just one line, with -Q . MyProject. To be clear I also cannot reproduce the error with -R . Top at the moment, the only error I get is this now: https://gist.github.com/jad-hamza/133698e142367e805025be85c440380b

view this post on Zulip Maxime Dénès (Oct 04 2019 at 06:32):

@Jad Hamza could it be a permission error? it seems that vscode can't launch coqidetop.opt (see the EACCES error)

view this post on Zulip Maxime Dénès (Oct 04 2019 at 06:33):

do you have a coqidetop.opt in the same directory as coqtop?

can you confirm it is the case?

view this post on Zulip Maxime Dénès (Oct 04 2019 at 06:37):

could it be that coqidetop.opt is installed only by the coqide package? This would make no sense, as coqidetop is really part of Coq, but...

view this post on Zulip Jad Hamza (Gitter import) (Oct 04 2019 at 06:56):

@Maxime Dénès Here they're in the same directory:

user@pc:~/path$ eval $(opam env)
user@pc:~/path$ coqtop --version
The Coq Proof Assistant, version 8.10+alpha (October 2019)
compiled on Oct 3 2019 15:54:54 with OCaml 4.09.0
user@pc:~/path$ coqidetop.opt --version
The Coq Proof Assistant, version 8.10+alpha (October 2019)
compiled on Oct 3 2019 15:54:54 with OCaml 4.09.0
user@pc:~/path$ which coqtop
/home/user/.opam/ocaml-4.09.0-coq-dev/bin/coqtop
user@pc:~/path$ which coqidetop.opt
/home/user/.opam/ocaml-4.09.0-coq-dev/bin/coqidetop.opt
user@pc:~/path$ ls -l /home/user/.opam/ocaml-4.09.0-coq-dev/bin/coqidetop.opt
-rwxr-xr-x 1 user user 26692368 oct.   3 16:02 /home/user/.opam/ocaml-4.09.0-coq-dev/bin/coqidetop.opt

It seems coqidetop.opt was installed when I installed the coq package in opam, should I also install the coqide package?

view this post on Zulip Maxime Dénès (Oct 04 2019 at 06:58):

I'm trying it now, to see if I can reproduce

view this post on Zulip Maxime Dénès (Oct 04 2019 at 06:58):

(I'm not using opam usually)

view this post on Zulip Maxime Dénès (Oct 04 2019 at 06:58):

I would hope that installing the coqide package is not necessary

view this post on Zulip Jad Hamza (Gitter import) (Oct 04 2019 at 06:59):

Thanks! Do you install from source?

view this post on Zulip Maxime Dénès (Oct 04 2019 at 06:59):

no, I use nix usually

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:00):

btw, we should also check what's stored in the preferences

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:00):

if you open the vscode preferences, and look in the vscoq ones, more precisely: "Coqtop: bin path"

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:01):

is anything set there?

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:01):

(file > preferences > settings then you can type coqtop in the filter)

view this post on Zulip Jad Hamza (Gitter import) (Oct 04 2019 at 07:02):

No it's empty

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:02):

hmmm

view this post on Zulip Jad Hamza (Gitter import) (Oct 04 2019 at 07:03):

I'll try to set it to the above folder

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:03):

so indeed, coqidetop.opt is installed by the coq opam package

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:04):

unfortunately, I can't reproduce your problem

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:05):

I just launched Coq 8.9.1 from VsCoq, after installing it using opam

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:05):

and it worked fine

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:05):

let's try coq.dev maybe

view this post on Zulip Jad Hamza (Gitter import) (Oct 04 2019 at 07:08):

I found where the -R . Top was coming from (I had set it in the preferences in coq.args from an old attempt at using vscoq :(

view this post on Zulip Jad Hamza (Gitter import) (Oct 04 2019 at 07:08):

Seems to be working fine now! Sorry for the wasted time

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:09):

still, the message was a bit strange, maybe there's something to improve there

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:09):

were the arguments incorrectly parsed?

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:11):

do you mean coqtop.args?

view this post on Zulip Jad Hamza (Gitter import) (Oct 04 2019 at 07:12):

Hm I closed vs code and cannot ctrl+z to see what was there, but I think I had: "coqtop.args": [ "-R . Top" ]. Instead should have been [ "-R", ".", "Top" ] maybe?

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:13):

I think so, yes

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:13):

I tried with the first value, and indeed coq does not start, although the error message is not exactly the same

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:13):

I get "coqtop-stderr: Unknown option -R . Top"

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:14):

which is clearer than the one you were getting, so still something strange going on

view this post on Zulip Jad Hamza (Gitter import) (Oct 04 2019 at 07:15):

Have you tried in conjunction with a -Q . MyProject from _CoqProject?

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:15):

ah no, right!

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:17):

still the same error message

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:17):

but ok, never mind I guess

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:17):

at least it works ;)

view this post on Zulip Jad Hamza (Gitter import) (Oct 04 2019 at 07:18):

:)

view this post on Zulip Jad Hamza (Gitter import) (Oct 04 2019 at 07:18):

Yes thanks!

view this post on Zulip Jad Hamza (Gitter import) (Oct 04 2019 at 07:19):

I'm looking at key bindings now, I see duplicate Step forward, Step backward, etc. (with different When conditions), is that normal?

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:19):

I'm not completely sure. They were there before (in the original VsCoq). I've noticed it, but not investigated (because there were more pressing issues to fix).

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:20):

Feedback welcome if you figure out why they are here :)

view this post on Zulip Jad Hamza (Gitter import) (Oct 04 2019 at 07:23):

Alright :) And one last thing, the steps forward and backward are working but not interpret to point (nothing happens when I press the corresponding key combinations, which I have tried to change)

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:24):

oh, that's again strange

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:25):

when you right click and use "interpret to point" in the menu, does it work?

view this post on Zulip Jad Hamza (Gitter import) (Oct 04 2019 at 07:28):

I tried once and it didn't work, then I tried again and it worked, and now the binding is working again (even after restarting code). Thanks!

view this post on Zulip Maxime Dénès (Oct 04 2019 at 07:28):

you're welcome!

view this post on Zulip vlj (Oct 06 2019 at 14:30):

is it possible to ask coqtop for the definition/theorem not loaded by an Import ? To fill the "outline" view of vscode

view this post on Zulip vlj (Oct 06 2019 at 14:30):

it's likely possible with some regex but I fear some corner cases

view this post on Zulip Paolo Giarrusso (Oct 06 2019 at 15:11):

@vlj Require foo. Print foo. does it without an import, but Require has still side effects, so _at least_ you'd want to do it in a separate coqtop

view this post on Zulip Paolo Giarrusso (Oct 06 2019 at 15:12):

(side effects: foo is in scope, and some declaration in foo have effects — like typeclass instances from it)

view this post on Zulip vlj (Oct 06 2019 at 15:26):

ok

view this post on Zulip Paolo Giarrusso (Oct 06 2019 at 15:27):

also I'm just a fellow user, maybe there's a smarter way? but it's more robust than regexes for sure

view this post on Zulip vlj (Oct 06 2019 at 20:21):

@Paolo G. Giarrusso but it doesn't list the symbol currently in the environment ?

view this post on Zulip vlj (Oct 06 2019 at 20:21):

I mean to Require and Print a symbol you must know that it exists

view this post on Zulip vlj (Oct 06 2019 at 20:30):

coq source code is a bit hard to read without experience in ocaml

view this post on Zulip Paolo Giarrusso (Oct 07 2019 at 15:24):

@vlj oh, you want to know all theorems in some codebase. Ask on https://coq.discourse.group/.
I fear you’d have to find all .vo files in some directory, and require each of them. At least, I think you would get every Gallina definition in submodules. (Not sure you get non-Gallina definitions like Ltac etc.)

view this post on Zulip Paolo Giarrusso (Oct 07 2019 at 15:25):

@vlj also, maybe https://github.com/Karmaki/coq-dpdgraph has useful code — that computes a dependency graph, but it must first find all theorems.

view this post on Zulip Paolo Giarrusso (Oct 07 2019 at 15:25):

Still, > Advice: you need to use Require to load the module that you want to explore, but don't use any Import/Export command because the tool is then unable to properly group the nodes by modules.

view this post on Zulip vlj (Oct 08 2019 at 19:14):

hmm it looks like the parser of coq code in server doesn't work to retrieve symbols

view this post on Zulip vlj (Oct 08 2019 at 19:15):

@Maxime Dénès I have a webpacked version of server (not of client unfortunatly) : https://github.com/coq-community/vscoq/pull/69

view this post on Zulip Maxime Dénès (Oct 08 2019 at 20:42):

parsing coq code on the vscode side is impossible

view this post on Zulip Maxime Dénès (Oct 08 2019 at 20:42):

Coq's parsing is extensible

view this post on Zulip Maxime Dénès (Oct 08 2019 at 20:43):

that's why I'm working on the separation of parsing and execution in Coq, so that IDEs can use Coq to parse documents

view this post on Zulip Maxime Dénès (Oct 08 2019 at 20:43):

parsing coq code on the vscode side is impossible

(without reimplementing half of Coq in vscode)

view this post on Zulip Théo Zimmermann (Oct 08 2019 at 21:30):

:sparkling_heart:

view this post on Zulip Paolo Giarrusso (Oct 08 2019 at 22:20):

(also it'd be great if functionality were kept on the coq side and shared across editors, tho I'm aware working on coq is hard)

view this post on Zulip Paolo Giarrusso (Oct 08 2019 at 22:21):

OT: also based on the experience in Scala 2, it feels like typecheckers are the best argument for limiting mutable state

view this post on Zulip Théo Winterhalter (Oct 09 2019 at 07:09):

I get a lot of « Anomaly "cannot find Ascii in module Coq.Strings.Ascii."
Please report at http://coq.inria.fr/bugs/. » at random places.

view this post on Zulip Théo Winterhalter (Oct 09 2019 at 07:11):

Triggers here for instance https://github.com/MetaCoq/metacoq/blob/tauto/examples/tauto.v#L78 but also at several points in the file (this is the first occurrence).

view this post on Zulip Théo Winterhalter (Oct 09 2019 at 07:12):

It only happens if I interpret to point somewhere later in the file. If I go step by step I get no error.

view this post on Zulip Matthieu Sozeau (Oct 09 2019 at 07:51):

What if you import ascii explicitely?

view this post on Zulip Maxime Dénès (Oct 09 2019 at 08:12):

@Théo Winterhalter would you mind trying the same thing in CoqIDE?

view this post on Zulip Maxime Dénès (Oct 09 2019 at 08:12):

it should be a good indicator of whether the bug is on the Coq side or the VsCoq side

view this post on Zulip Théo Winterhalter (Oct 09 2019 at 08:25):

I have to install it then.

view this post on Zulip Maxime Dénès (Oct 09 2019 at 08:26):

ah ah :) sorry about that

view this post on Zulip Théo Winterhalter (Oct 09 2019 at 09:28):

I can’t really manage to make coqIDE work. But at least I was able to pinpoint the problem from the sole From MetaCoq.Template Require Import All. (the problem appears when I only import this, and it doesn’t without).

The problem still happens with Require Import Ascii.

view this post on Zulip Théo Winterhalter (Oct 09 2019 at 09:29):

(I installed the CoqIDE dmg for the same version of coq I have but it still complains about inconsistent assumptions when loading metacoq.)

view this post on Zulip Matthieu Sozeau (Oct 09 2019 at 09:40):

Ate you sure your install is consistent? E.g you don’t have an old MetaCoq somewhere in user-contrib or so?

view this post on Zulip Théo Winterhalter (Oct 09 2019 at 09:41):

Don’t think so. Even so, if proof-general and vscoq manage to import metacoq, so should coqide.
It might not like that I didn’t install coqide together with coq.

view this post on Zulip Matthieu Sozeau (Oct 09 2019 at 09:45):

Yes, probably a version incompatibility

view this post on Zulip Théo Winterhalter (Oct 09 2019 at 09:46):

I don’t really want to debug coqide for this. Does jscoq support asynchronous compiling?

view this post on Zulip Matthieu Sozeau (Oct 09 2019 at 09:46):

Oh it could be wrong initialization of ML-side references in the MetaCoq plugin

view this post on Zulip Matthieu Sozeau (Oct 09 2019 at 09:47):

If we load (and use?) the plugin before importing ascii

view this post on Zulip Matthieu Sozeau (Oct 09 2019 at 09:48):

Switching to coqlib would fix this

view this post on Zulip Paolo Giarrusso (Oct 09 2019 at 14:51):

@Théo Winterhalter indeed the CoqIDE dmg has its own Coq and doesn't find libraries installed for the default one. Maybe share a minimized example?

view this post on Zulip Théo Winterhalter (Oct 09 2019 at 14:52):

It’s going to be hard since it seems metacoq has to be involved.

view this post on Zulip Paolo Giarrusso (Oct 09 2019 at 14:55):

@Théo Winterhalter the alternative is opam install coqide (if coq is opam-installed) :-|

view this post on Zulip Théo Winterhalter (Oct 09 2019 at 14:56):

Yeah I’ll do that.

view this post on Zulip Théo Winterhalter (Oct 09 2019 at 15:28):

Alright, the error is also present in coqide, sorry for bringing it up here.

view this post on Zulip Maxime Dénès (Oct 09 2019 at 15:29):

no worries!

view this post on Zulip Maxime Dénès (Oct 09 2019 at 15:29):

thanks for testing

view this post on Zulip vlj (Oct 16 2019 at 16:45):

@Maxime Dénès where does the coq parser split from main codebase happen ? I mean us there a branch ?

view this post on Zulip Maxime Dénès (Oct 16 2019 at 17:39):

oh, it's not a split from the main codebase

view this post on Zulip Maxime Dénès (Oct 16 2019 at 17:39):

it's a phase separation, rather

view this post on Zulip vlj (Oct 16 2019 at 20:46):

what do you mean by phase separation ?

view this post on Zulip Théo Zimmermann (Oct 17 2019 at 08:19):

So that one can request Coq to parse a document without executing it.

view this post on Zulip Maxime Dénès (Oct 17 2019 at 09:03):

exactly

view this post on Zulip Sequencer (Gitter import) (Oct 17 2019 at 09:28):

I heard that original author went to Facebook and never use coq after graduation. LOL

view this post on Zulip Théo Zimmermann (Oct 17 2019 at 09:30):

Things like this happen all the time. I'm not sure what exactly you find funny. Some people wish they could find a job related to Coq after graduation but do not always have such luck, while some others want to switch to other topics.

view this post on Zulip vlj (Oct 17 2019 at 10:40):

Thanks for the precision.

view this post on Zulip Matthieu Sozeau (Oct 17 2019 at 17:17):

I'd like to change the highlighting colors in my vscoq, how do I know how to modify e.g. the text in the ProofView pane? All my hyps are flashy green which is a bit too flashy for me

view this post on Zulip Sequencer (Gitter import) (Oct 17 2019 at 18:00):

No offence. Sorry about my word. I didn’t mean it’s funny. I think it’s a pity that great contributors will leave for such reasons. I hope coq(or such great things) could be, at least, a part time hobby, even without that luck.

view this post on Zulip Maxime Dénès (Oct 17 2019 at 21:33):

@Matthieu Sozeau I made all colors themable, so if I didn't forget any, you should be able to customize them

view this post on Zulip Maxime Dénès (Oct 17 2019 at 21:37):

you can "open workspace settings"

view this post on Zulip Maxime Dénès (Oct 17 2019 at 21:37):

then use workbench.colorCustomizations

view this post on Zulip Maxime Dénès (Oct 17 2019 at 21:39):

the color names are here: https://github.com/coq-community/vscoq/blob/d36f1b55e4ce19b7e55c129fa767cdb4a2976321/package.json#L524

view this post on Zulip Maxime Dénès (Oct 17 2019 at 21:39):

if you're proud of your setup, you can even contribute VsCoq themes :)

view this post on Zulip Matthieu Sozeau (Oct 17 2019 at 21:51):

Yep, I figured it out!

view this post on Zulip Matthieu Sozeau (Oct 17 2019 at 21:52):

Not proud yet :)

view this post on Zulip Matthieu Sozeau (Oct 18 2019 at 00:20):

I'm really starting to seriously wonder if people were saying Coq was slow in comparison to e.g. Lean just because the Emacs interface was SO slow. Developing proofs in VSCoq is a real breeze!

view this post on Zulip Théo Zimmermann (Oct 18 2019 at 11:34):

No offence. Sorry about my word. I didn’t mean it’s funny. I think it’s a pity that great contributors will leave for such reasons. I hope coq(or such great things) could be, at least, a part time hobby, even without that luck.

None taken. Indeed, for many people Coq continues to be a hobby after graduation, even when they cannot find a job around it either in research or industry. And fortunately, Coq is becoming more and more popular in industry which means that more and more people can actually find a job related to it, sometimes after having spent a few years on other topics. But in the case of C.J., I wouldn't be able to tell you, because I have never met them or talked to them personally.

view this post on Zulip Matthieu Sozeau (Oct 18 2019 at 11:46):

@Maxime Dénès Fail Check foo bar doesn't display the error in the output / notices buffer, strangely

view this post on Zulip Matthieu Sozeau (Oct 18 2019 at 11:52):

Typing (* inserts (**)) (two ending parens)

view this post on Zulip Maxime Dénès (Oct 18 2019 at 11:53):

can you open issues? so that we don't forget

view this post on Zulip Maxime Dénès (Oct 18 2019 at 11:53):

I've been fixing some in the past days, so it's really worth reporting

view this post on Zulip Matthieu Sozeau (Oct 18 2019 at 11:53):

After I finish preparing my lecture :)

view this post on Zulip Théo Winterhalter (Oct 18 2019 at 11:54):

@Matthieu Sozeau For the second one, just type Cmd + / to comment a line, and Alt + Shift + A to comment selection.
The first will just open (* *) on a new line.

view this post on Zulip Matthieu Sozeau (Oct 18 2019 at 11:55):

Nice one

view this post on Zulip Matthieu Sozeau (Oct 18 2019 at 13:20):

Anyone knows how to avoid the editor from highliting similar words when my cursor is on something. E.g. if my cursor is on Type, all Types in the document are highlighted and this is distracting.

view this post on Zulip Matthieu Sozeau (Oct 18 2019 at 13:23):

Nevermind, found it, Selection Highlight

view this post on Zulip Matthieu Sozeau (Oct 18 2019 at 13:26):

And Occurrences Highlight

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 16:32):

@Matthieu Sozeau the speed issue is indeed why I gave up on Proof General

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 16:34):

@Matthieu Sozeau re the missing output, it should be in the Info view, but that's not shown automatically because of https://github.com/coq-community/vscoq/issues/55

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 16:44):

@Maxime Dénès btw, while Matthieu run into https://github.com/coq-community/vscoq/issues/55, I'd like to gently plead for it if possible

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 16:46):

and as I mention there, it's not clear the plans you describe are related/needed for fixing the more urgent UX issues

view this post on Zulip vlj (Oct 18 2019 at 17:12):

About speed issues, for large proof (like gappa generated one) it looks like vscoq struggle when opening file because it triés to par se it via pegjs

view this post on Zulip vlj (Oct 18 2019 at 17:12):

And pegjs parser almost never return anything useful, there is no symbole listing at all

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:13):

yeah, we can probably simplify a lot the logic

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:13):

if you have an example large file, don't hesitate to open an issue

view this post on Zulip vlj (Oct 18 2019 at 17:14):

Since it Will be superseeded by some coqtop feedback anyways does it make sense to remove pegjs parser completly ?

view this post on Zulip vlj (Oct 18 2019 at 17:14):

Ok

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:14):

you still need to parse sentences for now

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:14):

but yeah, we can probably do it very efficiently

view this post on Zulip Théo Winterhalter (Oct 18 2019 at 17:21):

I’m wondering again, why do we not want foo is defined in vscoq if we want them in coqide and proof general?

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:24):

why do we want them in coqide and PG?

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:24):

in CoqIDE, it even prevents you from reading the error feedback while processing async proofs...

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:25):

because the thing keeps jumping to the other tab

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:25):

@Maxime Dénès I also think we want those

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:26):

what's the use case?

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:26):

first, "multiple tab" isn't convincing in practice

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:27):

Proof General has only one, and it's better than what we have today in vscoq

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:27):

I agree, but that doesn't explain why we need these info feedback

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:27):

second, "foo is defined" is only redundant in the rare case where foo literally appears in the source.

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:27):

the rare case?

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:27):

well, "rare" is provocative, but I'm typing some examples

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:28):

Inductive foo := . is the first counterexample

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:28):

I'm lost

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:28):

I'm pretty sure I can read foo in your example

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:28):

it generates foo_ind and whatsnot

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:29):

ah lol ok

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:29):

depending on the sort

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:29):

so I think calling literal occurrences rare case is just wrong

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:30):

that's provocative, but another example is coming...
For a better one, take:

Require Import stdpp.base.
Inductive foo := .
Section foo.
Context `(R: relation A) `{!Reflexive R}.

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:30):

second, you still didn't say what was the use case for the "foo_ind is defined" message

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:30):

that's honestly how I first learned about those things

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:30):

similarly, in my example, I get Reflexive0 is declared

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:30):

lol

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:31):

I still think the outline would be better than these messages

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:32):

maybe. But third, my actual worry is about using vscoq today, before the Info are reclassified as Notice or whatever

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:32):

yeah, this we can talk about, we may want some kind of temporary measure

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:33):

the Reflexive0 foo example, I'm really not convinced btw

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:33):

either the name matters, and it should be written by the user

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:33):

can I hijack this bikeshedding thread to ask how to actually add arguments to the coqtop invocation?

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:33):

or it doesn't and you wouldn't care about the message

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:33):

there is an option in the list but it only lets me edit the JSON

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:33):

ah, good question

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:33):

which lets me a bit clueless

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:33):

the "temporary measure" is the most important part anyway :-)

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:34):

on to Pierre's Q :-)

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:34):

maybe the first question is why you want a VsCoq specific flag

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:34):

?

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:34):

i.e. why not put it in _CoqProject

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:34):

oh

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:34):

because I don't believe in the neoliberal project bullshit paradigm

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:34):

not saying there are no use case

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:34):

open quote close quote

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:35):

sorry?

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:35):

like, I want a scratchpad

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:35):

to quickly typecheck stuff

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:35):

usually I just fire up coqIDE

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:35):

I'm afraid we support mainly project-centered stuff

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:35):

and there is a neat option to change the flags

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:35):

ga

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:35):

even PG lets you do that -_-

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:36):

@Pierre-Marie Pédrot seems you want sth. like "coqtop.args": []

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:36):

plus, there are use cases even inside a project

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:36):

yeah yeah, I'm not saying there are none, I

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:36):

e.g. selectively enabling type-in-type

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:36):

I'm explaining the state of affairs

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:36):

ok

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:36):

(I just did "Copy Settings as JSON")

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:36):

well, having your IDE pass type in type but not coqc is a bit strange, no?

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:36):

wdym?

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:37):

is "coqtop.args": ["-type-in-type"] the right syntax?

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:37):

I think so

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:37):

AFAIK there is no way to selectively compile a file with some flag

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:37):

now I remember using it

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:37):

using _CoqProject

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:37):

ah!

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:37):

nice XY problem, that's actually a good point

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:37):

is there an open issue about it?

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:37):

not that I know of

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:38):

type-in-type has become local, right?

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:38):

yes-ish

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:38):

the kind of broken SR local

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:38):

oh?!

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:38):

well that's expected

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:38):

like you do foo := bar

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:39):

you can't just break locally the invariants of a type theory and expect that everything is fine

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:39):

where bar has been compiled with type-in-type

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:39):

yes

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:39):

that breaks if you unfold

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:39):

then when you unfold foo you get in trouble

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:39):

I hadn't realized that when I merged it

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:39):

which is why the unimath people should be using well-scoped resize rules

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:39):

but that's another story

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:39):

you also didn't say it on the PR, did you?

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:40):

didn't I?

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:40):

at least we track it

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:40):

maybe I preferred the global behavior then

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:40):

the same issue goes for fixpoint checking

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:40):

argh

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:40):

it should be stored in the fixpoint, not in the definition

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:40):

yeah, right

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:40):

this is nonsense

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:40):

like Private Inductive also

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:40):

but it's the kind of broken-by-design feature

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:40):

yeah

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:41):

(people on coq/coq might also be interested ;-)

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:41):

so, I'm not waging a lost in advance war

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:41):

anyways

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:41):

although the type-in-type à la impredicative-set was a bit better in this respect

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:41):

lol yeah, wrong channel :D

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:41):

back to my question, the answer is that there is currently no neat way to have specific flags

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:41):

you can edit coqtop.args in the JSON

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:41):

as suggested, right?

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:41):

mkay

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:42):

not super user-friendly but I can live with that

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:42):

thx

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:42):

let's try

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:42):

it's fairly typical in the vscode world

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:42):

AFAIK it's like PG where you edit the lisp...

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:42):

screaming "JSON" running around is not going to convince me

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:42):

neither does "ELISP!"

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:43):

(... at least in CoqIDE we have a buffer-local set of values for that)

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:43):

more concretely, there's IDE support for JSON editing which makes it less bad

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 17:44):

(but I guess a PR for a nicer widget would be accepted)

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:45):

(I have to learn typescript for that first)

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:45):

(btw I thought that the OCaml folks had written BuckleScript bindings for VSCode)

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:46):

(that would allow for the use of some more reasonable language)

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:47):

for the client part, I think the language doesn't matter so much

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:47):

for the server, though, I would definitely prefer a saner language

view this post on Zulip Maxime Dénès (Oct 18 2019 at 17:55):

@Pierre-Marie Pédrot let us know if you succeeded in passing the flags

view this post on Zulip Pierre-Marie Pédrot (Oct 18 2019 at 17:55):

yep that worked thanks

view this post on Zulip vlj (Oct 18 2019 at 18:39):

I think it's possible to have on memory buffer in vscode

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 19:30):

@vlj how do you mean?

view this post on Zulip Paolo Giarrusso (Oct 18 2019 at 19:57):

@Maxime Dénès anyway, thanks a lot for your work here

view this post on Zulip vlj (Oct 18 2019 at 20:35):

There is this extension that seems to let you have scratch buffer https://marketplace.visualstudio.com/items?itemName=awesomektvn.scratchpad and there is a "virtual document" sample (but it's read only)

view this post on Zulip larsr (Gitter import) (Oct 24 2019 at 14:49):

Hi, I've been using proof-general and company-coq in emacs, and am tryingout VSCoq. Very nice work so far! Something I'm missing is the ability to read the documentation like one does with company-coq with ctrl-h. Is this on the horizon or does one get that functionality in some other way in VSCode?

view this post on Zulip vlj (Oct 24 2019 at 19:33):

No idea, afaik company coq generate thé help file by running sphinx on coq doc and then par se thé html which is a bit complicated

view this post on Zulip vlj (Oct 24 2019 at 19:34):

But the doc is always in sync with coq features

view this post on Zulip Théo Zimmermann (Oct 25 2019 at 08:40):

@larsr Feel free to open a feature request. Maybe someone can contribute some feature like this. Maybe the interesting company-coq parts can be ported to VsCoq.

view this post on Zulip Matthieu Sozeau (Oct 31 2019 at 17:40):

Hmm, I need an option to configure the coqtop called by vscoq to use hoqtop instead for coq-hott

view this post on Zulip Maxime Dénès (Oct 31 2019 at 22:02):

@Matthieu Sozeau good point, feel free to open an issue

view this post on Zulip Maxime Dénès (Oct 31 2019 at 22:02):

is there a hoqidetop.opt installed by coq-hott?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 31 2019 at 22:54):

hoqc is just a script that sets -coqlib and a few options, I understand because coq_makefile is not so flexible?

would be better to actually detect the right settings for the project instead of the current hackery

view this post on Zulip Paolo Giarrusso (Oct 31 2019 at 23:07):

@Matthieu Sozeau as a quick hack, you can create another folder with binaries with standard names, and change the PATH through existing vscode settings

view this post on Zulip Matthieu Sozeau (Nov 06 2019 at 08:17):

Any idea what are the color names associated to the "processed" part of the .v file, I'd like to change the background?

view this post on Zulip Maxime Dénès (Nov 07 2019 at 10:13):

@Matthieu Sozeau unfortunately, this color seems to be hardcoded: https://github.com/coq-community/vscoq/blob/379e4fc9ef11af6f55165710cb7d5c3a8ce3097c/client/src/Decorations.ts#L59

view this post on Zulip Matthieu Sozeau (Nov 07 2019 at 10:45):

I see, I don't know enough JS yet to try and make it configurable. Should not be impossible though, right?

view this post on Zulip Maxime Dénès (Nov 07 2019 at 10:45):

it should be easy, yes

view this post on Zulip Maxime Dénès (Nov 07 2019 at 10:45):

it's TS, not JS ;)

view this post on Zulip Matthieu Sozeau (Nov 08 2019 at 13:19):

Right

view this post on Zulip Rehan MALAK (Gitter import) (Nov 21 2019 at 13:26):

Did someone succeed with vscoq + copies of hoq\* executables renamed in coq\* in the PATH ?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 21 2019 at 14:10):

@Rehan MALAK I'd suggest just to set vscoq to call coqc -coqlib $hotts_stdlib

view this post on Zulip Rehan MALAK (Gitter import) (Nov 22 2019 at 16:26):

retried today without more success ... (changing coqtop.binPath or coqtop.args in package.json)

view this post on Zulip Maxime Dénès (Nov 22 2019 at 22:05):

what do you get?

view this post on Zulip Rehan MALAK (Gitter import) (Nov 25 2019 at 10:25):

@Maxime Dénès

It works with a coqidetop.opt in the PATH which mimics the hoqtop hoqchk hoqdep hoqc scripts...
:point_up: October 31, 2019 11:02 PM

Modifying coqtop.args in package.json made the plugin entirely unusable but I don't want to modify the plugin configuration anyway.

view this post on Zulip Ramkumar Ramachandra (Gitter import) (Jan 06 2020 at 16:18):

@Matthieu Sozeau Have a look at https://github.com/coq-community/vscoq/pull/97 -- HoTT now ships with hoqidetop (https://github.com/HoTT/HoTT/pull/1176)

view this post on Zulip Ramkumar Ramachandra (Gitter import) (Jan 06 2020 at 16:19):

I've tested it, and can confirm that it works.

view this post on Zulip Théo Winterhalter (Jan 08 2020 at 10:14):

I’ve been wondering, the output window often opens with 61288:proofworker:35:0 STM: sending back a fat state and it’s fairly annoying, especially since it overwrites what I might have been reading in the output window.

view this post on Zulip Théo Winterhalter (Jan 08 2020 at 10:14):

Is it normal?

view this post on Zulip Maxime Dénès (Jan 08 2020 at 12:40):

@Théo Winterhalter not really, do you have a repro case?

view this post on Zulip Théo Winterhalter (Jan 08 2020 at 13:00):

I think it happens every time I’m working in a big file, and it fills the Output window with them (10 or so sometimes).

view this post on Zulip Maxime Dénès (Jan 08 2020 at 13:01):

it must depend on the kind of tactics you use

view this post on Zulip Maxime Dénès (Jan 08 2020 at 13:01):

or the commands inside a proof, I don't remember

view this post on Zulip Théo Winterhalter (Jan 08 2020 at 13:01):

Oh. I’ll try to see which ones do it.

view this post on Zulip Maxime Dénès (Jan 08 2020 at 13:01):

maybe abstract?

view this post on Zulip Théo Winterhalter (Jan 08 2020 at 13:01):

I don’t use it.

view this post on Zulip Maxime Dénès (Jan 08 2020 at 13:01):

the message is emitted by the STM, but it is a bit surprising that it does so in non-debug mode

view this post on Zulip Maxime Dénès (Jan 08 2020 at 13:02):

and anyway, we should handle it in a way that does not disturb the user, on the VsCoq side

view this post on Zulip Théo Winterhalter (Jan 08 2020 at 13:08):

I don’t know what STM stands for. Anyway, it doesn’t happen when I go through the script sequentially, it only works asynchronously it seems.

view this post on Zulip Maxime Dénès (Jan 08 2020 at 13:08):

STM is the Coq component which handles async proofs ;)

view this post on Zulip Théo Winterhalter (Jan 08 2020 at 13:09):

Ok

view this post on Zulip Théo Winterhalter (Jan 08 2020 at 13:16):

I can’t manage to pinpoint where it comes from.

view this post on Zulip Matthieu Sozeau (Jan 08 2020 at 20:48):

@Ramkumar Ramachandra nice!

view this post on Zulip Ramkumar Ramachandra (Gitter import) (Jan 09 2020 at 08:46):

@Matthieu Sozeau Unfortunately, I made a mess of https://github.com/coq-community/vscoq/pull/89, which my branch depends on. @Maxime Dénès is currently cleaning it up so it's suitable to merge (progress: https://github.com/coq-community/vscoq/pull/100). So, it'll be a while before https://github.com/coq-community/vscoq/pull/97 is rebased and merged: if you don't want to wait, I recommend you just use my branch for now.

view this post on Zulip Matthieu Sozeau (Jan 09 2020 at 15:27):

@Maxime Dénès how hard would it be to handle multiple _CoqProject files (just being able to configure the _CoqProject to use per folder would be enough in my case) ?

view this post on Zulip Maxime Dénès (Jan 09 2020 at 15:41):

not sure what this would mean, aren't we supposed to have one _CoqProject file per project?

view this post on Zulip Maxime Dénès (Jan 09 2020 at 15:41):

are the various folders corresponding to different projects?

view this post on Zulip Théo Winterhalter (Jan 09 2020 at 15:42):

For metacoq we build several stuff and each have its own _CoqProject in different folders yes.

view this post on Zulip Maxime Dénès (Jan 09 2020 at 15:44):

I didn't now this was supported on the Coq side, TBH

view this post on Zulip Maxime Dénès (Jan 09 2020 at 15:45):

the documentation seems to be written assuming there's only one such file per project, no? https://coq.inria.fr/distrib/current/refman/practical-tools/utilities.html?highlight=_coqproject

view this post on Zulip Maxime Dénès (Jan 09 2020 at 15:45):

where is the multiple project files layout documented?

view this post on Zulip Maxime Dénès (Jan 09 2020 at 15:46):

(it doesn't seem too hard to support, but of course I need a spec of which settings apply where)

view this post on Zulip Matthieu Sozeau (Jan 09 2020 at 15:56):

You can just think of it as having one repository with two folders each with its own _CoqProject file. The same issue already appears when you want to process files in _build_ci in Coq: each project might have its own _CoqProject.

view this post on Zulip Matthieu Sozeau (Jan 09 2020 at 15:57):

What I would like is that when I open a file in folder foo/ I get the options in foo/_CoqProject. Basically taking the "closest" _CoqProject file would do

view this post on Zulip Théo Winterhalter (Jan 09 2020 at 16:05):

Note that PG already handles this (I don’t know how though).

view this post on Zulip Matthieu Sozeau (Jan 09 2020 at 16:06):

I also would like to have this for projects that use submodules (certicoq uses that for example)

view this post on Zulip Maxime Dénès (Jan 09 2020 at 16:06):

I think from the VsCoq perspective, we'd need to support multi project workspaces

view this post on Zulip Maxime Dénès (Jan 09 2020 at 16:06):

https://code.visualstudio.com/docs/editor/multi-root-workspaces

view this post on Zulip Matthieu Sozeau (Jan 09 2020 at 16:07):

Yep, that's another way

view this post on Zulip Maxime Dénès (Jan 09 2020 at 16:11):

well, from the name, I imagine _CoqProject was intended as a description of a project, no?

view this post on Zulip Maxime Dénès (Jan 09 2020 at 16:11):

@Matthieu Sozeau did you try to open one of the folders, and then add the other to your workspace?

view this post on Zulip Maxime Dénès (Jan 09 2020 at 16:12):

maybe this way it picks up the right _CoqProject for each file, depending on which project it belongs to

view this post on Zulip Maxime Dénès (Jan 09 2020 at 16:12):

if it doesn't, I guess we can consider it a VsCoq bug

view this post on Zulip Matthieu Sozeau (Jan 09 2020 at 16:12):

What I mean is: if you were to look for _CoqProject at the root of each project in a multi-root workspace it could work too. But that wouldn't handle the submodule case

view this post on Zulip Maxime Dénès (Jan 09 2020 at 16:13):

why wouldn't it work for the submodule case?

view this post on Zulip Maxime Dénès (Jan 09 2020 at 16:14):

(I'm not very familiar with all this stuff, and I've always found the Coq documentation very sparse on it, so sorry if my questions are naive)

view this post on Zulip Théo Zimmermann (Jan 09 2020 at 17:16):

The documentation has always been severly lacking indeed. And all of this might go away soon with Dune...

view this post on Zulip Matthieu Sozeau (Jan 09 2020 at 17:23):

In the submodule case I was thinking we would not use multi-root workspaces, but allow to get the closest _CoqProject instead

view this post on Zulip Maxime Dénès (Jan 09 2020 at 17:25):

well, the submodule is usually another project, really, no?

view this post on Zulip Maxime Dénès (Jan 09 2020 at 17:26):

but I don't know if vscode would allow adding it to the workspace as an independent project

view this post on Zulip Matthieu Sozeau (Jan 09 2020 at 17:26):

The coqtop will point to the enclosing Coq though...

view this post on Zulip Matthieu Sozeau (Jan 09 2020 at 17:26):

Yep, not sure either

view this post on Zulip Maxime Dénès (Jan 09 2020 at 17:26):

coqtop?

view this post on Zulip Maxime Dénès (Jan 09 2020 at 17:26):

do you use several copies of coq?

view this post on Zulip Matthieu Sozeau (Jan 09 2020 at 17:26):

The coqtop with which you will want to run the submodule code

view this post on Zulip Maxime Dénès (Jan 09 2020 at 17:27):

I'm a bit lost, what does coqtop have anything to do with this?

view this post on Zulip Maxime Dénès (Jan 09 2020 at 17:28):

you mean vscoqtop? and do you really have different copies, or do you simply mean the options that should be passed to it?

view this post on Zulip Matthieu Sozeau (Jan 09 2020 at 17:28):

I'm just saying the two projects are linked somehow. If I want to build/run interactively something in _build_ci/ with the coqtop that is in _build/

view this post on Zulip Théo Winterhalter (Jan 15 2020 at 16:44):

Hi, I was wondering what is the planned release schedule or whatever, it seems there were a lot of modifications recently so I wondered if you planned on releasing them soonish.

view this post on Zulip Théo Winterhalter (Jan 15 2020 at 16:56):

Anyway there are serious synchronisation problems when files are large.

view this post on Zulip Théo Winterhalter (Jan 15 2020 at 18:45):

vscoq-slow.mov

view this post on Zulip Théo Winterhalter (Jan 15 2020 at 18:48):

(This is a video showing the problem, because I don’t know how to reproduce it, I think it’s linked to synchronisation because the problem only occurs after edits of the text. Most of the time it’s faster to reload vscoq entierly!)

view this post on Zulip Paolo Giarrusso (Jan 15 2020 at 20:13):

yeah, I also restart vscoq periodically; it’s hard to tell which issues are due to async proofs, and which are due to vscoq specifically

view this post on Zulip Paolo Giarrusso (Jan 15 2020 at 20:14):

(but restarting vscoq still seems faster than using proof general :-| )

view this post on Zulip Paolo Giarrusso (Jan 15 2020 at 20:14):

(but let’s see if that’s the same issue I have)

view this post on Zulip Théo Winterhalter (Jan 15 2020 at 21:40):

Yeah it’s still faster than PG haha. But that means there is potential for something much much faster.

view this post on Zulip Maxime Dénès (Jan 15 2020 at 22:07):

there were a lot of modifications recently

not really, were there?

view this post on Zulip Maxime Dénès (Jan 15 2020 at 22:07):

but yeah, master has an important fix related to sync issues

view this post on Zulip Maxime Dénès (Jan 15 2020 at 22:07):

so expect a release very soon

view this post on Zulip Maxime Dénès (Jan 15 2020 at 22:14):

but the fixed issue is only when you use vscode's undo

view this post on Zulip Maxime Dénès (Jan 15 2020 at 22:15):

so I'm not sure if it is your problem

view this post on Zulip Maxime Dénès (Jan 15 2020 at 22:15):

I've also made significant progress on the document manager

view this post on Zulip Maxime Dénès (Jan 15 2020 at 22:15):

getting rid of the server in VsCoq should fix a lot of these issues

view this post on Zulip Paolo Giarrusso (Jan 16 2020 at 03:45):

Well I use vscode's undo often, so hurrah! (In fact, I also use the undo from a vim emulation plugin, which seems visibly separate).

view this post on Zulip Ramkumar Ramachandra (Gitter import) (Jan 16 2020 at 07:39):

prettify-symbols-mode often malfunctions for me, although reloading the window often fixes the issue.

view this post on Zulip Ramkumar Ramachandra (Gitter import) (Jan 16 2020 at 07:44):

How can we get rid of the VsCoq server though? IIUC, coqidetop doesn't speak LSP.

view this post on Zulip Maxime Dénès (Jan 16 2020 at 07:51):

I also use the undo from a vim emulation plugin

Yeah, this one did not have the bug, that's why I didn't notice it initially

view this post on Zulip Maxime Dénès (Jan 16 2020 at 07:51):

How can we get rid of the VsCoq server though? IIUC, coqidetop doesn't speak LSP.

I'm implementing another toplevel on the Coq side, based on a document manager, which speaks LSP

view this post on Zulip Ramkumar Ramachandra (Gitter import) (Jan 16 2020 at 07:52):

Oh, nice! Can you point me to the branch or PR?

view this post on Zulip Maxime Dénès (Jan 16 2020 at 07:53):

it's not usable yet, and the code is unreadable https://github.com/maximedenes/coq/tree/document-manager

view this post on Zulip Théo Winterhalter (Jan 16 2020 at 07:55):

Ok cool! I’m looking forward to this. Thanks a lot!

view this post on Zulip Ramkumar Ramachandra (Gitter import) (Jan 16 2020 at 07:57):

Cool. Looks like it's going to take a while.

view this post on Zulip Ramkumar Ramachandra (Gitter import) (Jan 16 2020 at 08:01):

So there are going to be four toplevels: coqtop, coqtop -emacs, codeidetop, and vscoqtop. After the merge, I hope more users move to vscoqtop -- all editors have lsp support (some via packages), and it's a well-designed protocol.

view this post on Zulip Maxime Dénès (Jan 16 2020 at 08:01):

well, that's not LSP, it's LSP + extension

view this post on Zulip Maxime Dénès (Jan 16 2020 at 08:02):

but yeah, the idea is to make the life of all IDEs easier

view this post on Zulip Ramkumar Ramachandra (Gitter import) (Jan 16 2020 at 08:03):

IIUC, you'll need to augment LSP with some extra commands for ProofState and the like.

view this post on Zulip Maxime Dénès (Jan 16 2020 at 08:04):

well, it is more or less the protocol that the VsCoq client speaks already

view this post on Zulip Ramkumar Ramachandra (Gitter import) (Jan 16 2020 at 08:04):

Right.

view this post on Zulip Ramkumar Ramachandra (Gitter import) (Jan 16 2020 at 08:06):

Btw, I cleaned up a few of my PRs, and they should be easy to review. Let me know when you get around to them: I can clean up the build-flattening part from #89 too, after #101 is merged.

view this post on Zulip Maxime Dénès (Jan 16 2020 at 08:06):

yeah, I'll try to have a look quickly

view this post on Zulip Maxime Dénès (Jan 16 2020 at 08:06):

like this week

view this post on Zulip Ramkumar Ramachandra (Gitter import) (Jan 16 2020 at 08:06):

Okay.

view this post on Zulip Théo Winterhalter (Jan 29 2020 at 09:51):

Everytime I open a file I get the error:

[Error - 10:50:42 AM] Request textDocument/documentSymbol failed.
  Message: Request textDocument/documentSymbol failed unexpectedly without providing any details.
  Code: -32603

Is this normal?

view this post on Zulip Maxime Dénès (Jan 29 2020 at 09:53):

@Théo Winterhalter I think it is not. Most likely VsCoq fails to declare that it does not support textDocument/documentSymbol

view this post on Zulip Maxime Dénès (Jan 29 2020 at 09:53):

would you mind opening an issue?

view this post on Zulip Théo Winterhalter (Jan 29 2020 at 09:53):

Ok!

view this post on Zulip Narek Asadorian (Gitter import) (Feb 10 2020 at 21:26):

Hi folks! New user coming to Coq from Scala/OCaml/etc. Very happy to be able to develop proofs inside VSCode. I have some questions regarding missing features. I am happy to create as issues and also help work on myself!

Are these features straightforward/mechanical to add? Case split seems to be the only one that requires semantic information.

view this post on Zulip Paolo Giarrusso (Feb 10 2020 at 21:32):

@Narek Asadorian some of the data for completion lives in data files in the plugin

view this post on Zulip Paolo Giarrusso (Feb 10 2020 at 21:33):

IIRC there's an issue about generating them automatically, but I'm not sure how much progress on them there was.

view this post on Zulip Narek Asadorian (Gitter import) (Feb 10 2020 at 22:15):

Thanks @Paolo G. Giarrusso, yes I see the JSON file with the "snippets". I can manually add some and create a PR.

view this post on Zulip Narek Asadorian (Gitter import) (Feb 10 2020 at 22:15):

Automated does sound a lot nicer though.

view this post on Zulip Narek Asadorian (Gitter import) (Feb 10 2020 at 22:19):

Does the case split thing sound feasible at all?

view this post on Zulip Paolo Giarrusso (Feb 10 2020 at 22:36):

Dunno, but luckily I'm not the maintainer. I'm not aware of that feature in CoqIDE either tho.

view this post on Zulip Narek Asadorian (Gitter import) (Feb 10 2020 at 23:08):

I see, I should try out CoqIDE to get a feeling for what's possible.

view this post on Zulip Narek Asadorian (Gitter import) (Feb 10 2020 at 23:08):

Have not tried Proof General either, but I'm not an emacs person :)

view this post on Zulip Enzo Crance (Gitter import) (Feb 13 2020 at 09:45):

Hello everyone. While walking through proofs, after a few minutes, this error appears at the end of lemma declarations, right before Proof.:

coqtop-stderr: 1496:proofworker:1:0] Slave: critical exception: Anomaly
                                                 "cannot find D0 in module Coq.Numbers.Cyclic.Int31.Int31."
                      Please report at http://coq.inria.fr/bugs/.

Does anyone have an idea how to solve this issue? Thanks in advance.

view this post on Zulip Maxime Dénès (Feb 13 2020 at 09:50):

This looks like a Coq bug, but you can open an issue on the VsCoq repo with instructions on how to reproduce

view this post on Zulip Maxime Dénès (Feb 13 2020 at 09:50):

I can have a look and forward to Coq or fix in VsCoq, depending on the nature of the bug

view this post on Zulip Enzo Crance (Gitter import) (Feb 13 2020 at 09:51):

I’m unsure how to reproduce the bug, it just randomly appears when I am opening Coq files. I have tried reinstalling Coq, but that doesn’t fix it. Should I reinstall VSCode too, in your opinion?

view this post on Zulip Maxime Dénès (Feb 13 2020 at 09:53):

I would be surprised if reinstalling fixes it

view this post on Zulip Maxime Dénès (Feb 13 2020 at 09:53):

But it probably isn't really random

view this post on Zulip Maxime Dénès (Feb 13 2020 at 09:53):

maybe triggered by a complex chain of actions

view this post on Zulip Enzo Crance (Gitter import) (Feb 13 2020 at 09:54):

I’ll try on simple proofs first, and might open an issue if I can reproduce the bug correctly. Thanks for the advice.

view this post on Zulip Maxime Dénès (Feb 13 2020 at 09:55):

Sorry for the inconvenience

view this post on Zulip Enzo Crance (Gitter import) (Feb 13 2020 at 09:56):

One cannot solve every single bug

view this post on Zulip Enzo Crance (Gitter import) (Feb 13 2020 at 09:57):

And I asked before even trying to find the source, in case the bug already happened before.

view this post on Zulip Enzo Crance (Gitter import) (Feb 13 2020 at 09:57):

I’ll keep you updated! :)

view this post on Zulip Enzo Crance (Gitter import) (Feb 13 2020 at 16:16):

It is both linked to the SMTCoq library and VSCoq. I submitted an issue about that:
https://github.com/coq-community/vscoq/issues/114

view this post on Zulip Maxime Dénès (Feb 13 2020 at 16:34):

Thanks, I'll try to have a look when I can

view this post on Zulip Théo Winterhalter (Feb 28 2020 at 10:36):

@Maxime Dénès Is there any hope of having a release soon? The sync problem is really annoying. It’s a shame there is no beta channel on the vscode marketplace.

view this post on Zulip Maxime Dénès (Feb 28 2020 at 10:53):

sure, I was planning to do one today

view this post on Zulip Maxime Dénès (Feb 28 2020 at 10:53):

sorry for the delay

view this post on Zulip Théo Winterhalter (Feb 28 2020 at 10:53):

Nice!

view this post on Zulip Matthieu Sozeau (Feb 28 2020 at 12:51):

It would be great to make the coqtop binary configurable and not just its path, e.g. for HoTT :)

view this post on Zulip Maxime Dénès (Feb 28 2020 at 12:56):

there's a PR for that, but I'm afraid it introduces a regression on Windows (not sure), I'll comment there

view this post on Zulip Maxime Dénès (Feb 28 2020 at 14:25):

@Matthieu Sozeau see https://github.com/coq-community/vscoq/pull/97

view this post on Zulip Théo Winterhalter (Feb 28 2020 at 14:44):

Is there a reliable way to quit / kill coqtop from vscoq?
For now the fastest seems to use « Developer: Reload widow ». « Coq: Reset », « Coq: Quit », and « Coq: Finish computations » seem to all wait for some things to finish when I want to interupt because of sync problems.

view this post on Zulip Maxime Dénès (Feb 28 2020 at 14:46):

finish is something else, but I would expect reset and quit to terminate Coq even in the middle of a computation

view this post on Zulip Maxime Dénès (Feb 28 2020 at 14:46):

not sure what the difference is between the two

view this post on Zulip Théo Winterhalter (Feb 28 2020 at 14:47):

Ok well, when I’m waiting for some sync to happen after edit, it seems I have to wait for it to be done before it quits.

view this post on Zulip Maxime Dénès (Feb 28 2020 at 14:49):

I'd be interested in a repro case, if you manage to get one, but I imagine it is difficult

view this post on Zulip Théo Winterhalter (Feb 28 2020 at 14:50):

Maybe it’ll all go away with the next update.
But I still haven’t found out what was the origin of the problem. I used to think it was large files, but that’s not the case, in the same project I have a 8000+ lines file where this problem doesn’t occur.

view this post on Zulip Maxime Dénès (Feb 28 2020 at 14:55):

I'm afraid there's a fundamental problem

view this post on Zulip Maxime Dénès (Feb 28 2020 at 14:56):

Coq's interaction model assumes some regions are untouchable

view this post on Zulip Maxime Dénès (Feb 28 2020 at 14:56):

i.e. cannot be edited, in certain states

view this post on Zulip Théo Winterhalter (Feb 28 2020 at 14:56):

I’m trying to pintpoint the problem again.

view this post on Zulip Théo Winterhalter (Feb 28 2020 at 14:58):

Usually when I have the problem, some regions will be green-coloured for some time before Coq realises they should not. Sometimes it’s old code that is after new editions, sometimes it’s new code that being typed.

view this post on Zulip Théo Winterhalter (Feb 28 2020 at 14:58):

But the main case is when I’m writing a proof, so I’m not editing untouchable region, I’m editing where I should be I think.

view this post on Zulip Maxime Dénès (Feb 28 2020 at 15:00):

I think (but I'm not sure), that in the model there are some states (e.g. Coq computes / parses) where you are supposed to edit nowhere

view this post on Zulip Maxime Dénès (Feb 28 2020 at 15:01):

the clean way to fix this is to lift these restrictions from Coq by implementing a proper document manager (this is what VsCoq's server emulates)

view this post on Zulip Maxime Dénès (Feb 28 2020 at 15:01):

I started to work on it, but I need more time to complete it

view this post on Zulip Théo Winterhalter (Feb 28 2020 at 15:02):

Yeah I know.

view this post on Zulip Maxime Dénès (Feb 28 2020 at 15:02):

meanwhile, I think I'm going to make a release even without #97, since this important sync fix has been waiting for too long already

view this post on Zulip Maxime Dénès (Feb 28 2020 at 15:02):

we can anyway make a new release soon

view this post on Zulip Théo Winterhalter (Feb 28 2020 at 15:18):

I really can’t manage to find a reason for the bug. I tried taking only prefixes of the file to find the smallest with the problem, but I can’t find a clear turning point, there are different degrees of delays…

view this post on Zulip Maxime Dénès (Feb 28 2020 at 15:50):

I also failed to reproduce it :(

view this post on Zulip Maxime Dénès (Feb 28 2020 at 15:51):

it does occur in https://github.com/coq-community/vscoq/issues/116 though

view this post on Zulip Maxime Dénès (Feb 28 2020 at 15:51):

fairly reliably

view this post on Zulip Maxime Dénès (Feb 28 2020 at 15:51):

I'm going to study that performance problem, hoping it could also explain the out-of-sync scenarios

view this post on Zulip Théo Winterhalter (Feb 28 2020 at 15:52):

It might be the same kind of problem yes.

view this post on Zulip Ramkumar Ramachandra (Gitter import) (Feb 28 2020 at 17:42):

@Maxime Dénès I've fixed #97, but don't have a Windows machine to test the changes: would you like to take a look?

view this post on Zulip Maxime Dénès (Feb 28 2020 at 18:37):

@Ramkumar Ramachandra thanks, I'll have a look next week. If it works properly, I'll integrate and make a new release.

view this post on Zulip Maxime Dénès (Feb 28 2020 at 18:37):

(I did one today for the important undo-related fix)

view this post on Zulip Théo Winterhalter (Feb 28 2020 at 20:12):

Thanks for the update! :)
Unfortunately, my problem is still present, stepping forward afer writing idtac. still takes 20s. I guess it’s the same as #116. (But again, I’m not convinced that files being large is the only thing at fault here, I have large files without troubles, and one of my office mates reports having the issue with pretty small files as well, I’ll try to get my hands on such files.)

view this post on Zulip Paolo Giarrusso (Feb 28 2020 at 20:44):

@Maxime Dénès @Théo Winterhalter for me, as soon as Coq diverges, often Coq: Reset will "reset" Coq but leave the old one running — I usually notice when my fan spins up.

view this post on Zulip Paolo Giarrusso (Feb 28 2020 at 20:45):

does any of you have code where Coq: Reset works?

view this post on Zulip Théo Winterhalter (Feb 28 2020 at 21:17):

Not really…

view this post on Zulip Paolo Giarrusso (Feb 28 2020 at 21:47):

okay, so @Maxime Dénès must have such an example.

view this post on Zulip Paolo Giarrusso (Feb 28 2020 at 21:47):

@Théo Winterhalter are you also on Mac? I've seen my share of Mac-specific bugs

view this post on Zulip Théo Winterhalter (Feb 29 2020 at 09:43):

Yeah I’m on macOS.
But my officemates aren’t and they also report issues like this. They seem to complain about it more than I do.

view this post on Zulip Théo Winterhalter (Feb 29 2020 at 09:43):

(They’re on Ubutun/Debian)

view this post on Zulip Paolo Giarrusso (Feb 29 2020 at 13:57):

Actually, is there a way to set a default timeout for tactics, other than by overriding each of them? Right now when a tactic loops and I restart VsCoq, I manually type timeout 1 before trying again.

view this post on Zulip Jad Hamza (Gitter import) (Mar 07 2020 at 11:26):

Hello, how can I find the name of the colors to customize, for instance for the (green) background of the already processed part of the file? I looked in https://github.com/coq-community/vscoq/blob/master/package.json but it doesn't look like this color is defined here

view this post on Zulip Jad Hamza (Gitter import) (Mar 08 2020 at 15:33):

Looks like it's hard-coded? https://github.com/coq-community/vscoq/blob/6123dc9777a7d499f9b75cc0be298918182ade89/client/src/Decorations.ts#L59

view this post on Zulip Jad Hamza (Gitter import) (Mar 11 2020 at 13:24):

Speaking about colors, the Qed keyword sometimes takes the incomplete color from this Decorations.ts file, even when there are no errors, is this a known issue?

view this post on Zulip Paolo Giarrusso (Mar 11 2020 at 16:49):

@Jad Hamza I thought that purple was just "proof checked by a parallel worker", based on its behavior

view this post on Zulip Paolo Giarrusso (Mar 11 2020 at 16:49):

but the comment suggests that's not intended so you're right

view this post on Zulip Jad Hamza (Gitter import) (Mar 12 2020 at 17:36):

Looks like it's hard-coded? https://github.com/coq-community/vscoq/blob/6123dc9777a7d499f9b75cc0be298918182ade89/client/src/Decorations.ts#L59

Modifying this worked for the background color, I also made it highlight the whole line for processed regions (instead of just the text) as in proof general

view this post on Zulip Jad Hamza (Gitter import) (Mar 13 2020 at 10:06):

When a command takes a long time, is there a away to stop/interrupt it without losing the progress in the file? Coq: Interrupt seems to have no effect, and Coq: Reset and Coq: Quit come back to the beginning

view this post on Zulip Matthieu Sozeau (Mar 13 2020 at 11:55):

@Jad Hamza I thought the Qed not changing color was due to the proof not being "joined back" to the main process, but maybe it's a bug

view this post on Zulip Théo Winterhalter (Mar 13 2020 at 12:22):

@Jad Hamza If I understand correctly, currently there is no hook to tell coqtop to interrupt the current computation so vscoq can only kill it. It should be implemented at some point in the future.

view this post on Zulip Jad Hamza (Gitter import) (Mar 13 2020 at 12:56):

@Matthieu Sozeau yes I see it only happen when Qed "finishes" before its proof I think

view this post on Zulip Jad Hamza (Gitter import) (Mar 13 2020 at 12:58):

@Théo Winterhalter Ah cool! How does it work in Proof General and CoqIde?

view this post on Zulip Théo Winterhalter (Mar 13 2020 at 13:25):

I don’t know. :-/

view this post on Zulip Jad Hamza (Gitter import) (Mar 13 2020 at 13:36):

The message which is displayed in Proof General when interrupting ("User interrupt.") comes from here: https://github.com/coq/coq/blob/3449c8a088e9a902ebc73478667f4f25d6c08d2a/checker/checker.ml#L252 so maybe it's enough to send a signal to the coqtop process?

view this post on Zulip Jad Hamza (Gitter import) (Mar 13 2020 at 13:38):

(or here: https://github.com/coq/coq/blob/3449c8a088e9a902ebc73478667f4f25d6c08d2a/vernac/himsg.ml#L1373)

view this post on Zulip Jad Hamza (Gitter import) (Mar 13 2020 at 14:26):

Hmm VsCoq does send a SIGINT signal to coqtop

view this post on Zulip Paolo Giarrusso (Mar 13 2020 at 15:33):

@Jad Hamza I either use timeout first if I know (e.g. Ltac firstorder := timeout 1 firstorder) or “Cmd-Shift-P -> Developer: Reload Window”. You don’t even need to save files.

view this post on Zulip Paolo Giarrusso (Mar 13 2020 at 15:33):

I know by heart because it’s a regular part of my workflow.

view this post on Zulip Paolo Giarrusso (Mar 13 2020 at 15:57):

:worried:

view this post on Zulip Paolo Giarrusso (Mar 13 2020 at 15:58):

(and I still prefer vscoq over proof general because of async proofs, despite vscode's inferior unicode input methods, vim emulation, and vscoq bugs)

view this post on Zulip Jad Hamza (Gitter import) (Mar 13 2020 at 16:28):

Yes reload window works nice, but it loses progress :( What does interrupt do for you?

view this post on Zulip Jad Hamza (Gitter import) (Mar 13 2020 at 16:32):

I have a workaround that works for me: https://github.com/coq-community/vscoq/issues/123

view this post on Zulip Paolo Giarrusso (Mar 13 2020 at 18:15):

@Jad Hamza wat

view this post on Zulip Paolo Giarrusso (Mar 13 2020 at 18:16):

(I’ve only ever tried the red button on the status bar at the bottom, and it never worked)

view this post on Zulip Paolo Giarrusso (Mar 13 2020 at 18:17):

do you know what coqide does? hopefully that’s correct (since coq devs use linux and coqide is apparently usable there)

view this post on Zulip Jad Hamza (Gitter import) (Mar 13 2020 at 19:46):

I also see the "User interrupt." message in CoqIde so probably also a SIGINT signal?

view this post on Zulip Jad Hamza (Gitter import) (Mar 13 2020 at 19:59):

The red button (or the Coq: Interrupt command used with a shortcut) works with this workaround

view this post on Zulip Paolo Giarrusso (Mar 13 2020 at 20:28):

@Jad Hamza send a PR and let's have somebody familiar with CoqIDE review it? If I have time I'll try that soon

view this post on Zulip Jad Hamza (Gitter import) (Mar 13 2020 at 20:39):

I don't think it's the right way to do it, I completely removed the XML part, I thought that could be discussed in the issue

view this post on Zulip Paolo Giarrusso (Apr 12 2020 at 21:14):

on Coq: Interrupt, a month passed, so I took the liberty to file a PR with that fix, since this is a critical major bug in practice: https://github.com/coq-community/vscoq/pull/127.

view this post on Zulip Paolo Giarrusso (Apr 12 2020 at 21:14):

It does work under some minimal testing.

view this post on Zulip Jad Hamza (Gitter import) (Apr 13 2020 at 06:43):

Thanks :)

view this post on Zulip Cyril Cohen (Apr 15 2020 at 14:10):

Hi, I am in the process of exporting gitter channels (public) data to zulip, (it can be done only once, during the creation of the zulip chatroom), do you wish that I export the data of this channel too?

view this post on Zulip Alex Gryzlov (Gitter import) (Apr 23 2020 at 22:58):

what's the zulip server?

view this post on Zulip Maxime Dénès (Apr 26 2020 at 09:42):

@Cyril Cohen why not, I couldn't catch up with the discussion yet


Last updated: Jan 30 2023 at 17:03 UTC