Odomontois (Gitter import) (Sep 16 2019 at 08:16): Odomontois (Gitter import) (Sep 16 2019 at 08:16):So there aren't a lot of discussions here
Odomontois (Gitter import) (Sep 16 2019 at 08:17):Can someone guide a noob how to try the plugin locally?
Maxime Dénès (Sep 16 2019 at 10:00):hi! the room is fairly new ;)
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
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
Brendan Zabarauskas (Gitter import) (Sep 16 2019 at 10:20):"wait for a few days" :heart_eyes: :heart_eyes: :heart_eyes:
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.
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.
Théo Winterhalter (Sep 18 2019 at 14:17):Ok, good to know. :)
Maxime Dénès (Sep 18 2019 at 14:27):Thanks for the feedback!
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.
Maxime Dénès (Sep 18 2019 at 15:45):oh! which shortcuts do you mean?
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).
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
Maxime Dénès (Sep 18 2019 at 15:54):we should probably change the default bindings on macOS then
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
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
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?
Théo Winterhalter (Sep 18 2019 at 15:55):Ok!
Maxime Dénès (Sep 18 2019 at 15:56):on Linux, it's ALT instead of command
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
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.
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
Maxime Dénès (Sep 18 2019 at 16:01):so we are quite free in the choice
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?
Maxime Dénès (Sep 19 2019 at 13:29):you mean when using Program?
Théo Winterhalter (Sep 19 2019 at 13:29):Yes (or Equations in my case).
Maxime Dénès (Sep 19 2019 at 13:29):hmm not sure, let me test it
Théo Winterhalter (Sep 19 2019 at 13:29):I can blindly type Next Obligation.
Théo Winterhalter (Sep 19 2019 at 13:30):Thanks.
Maxime Dénès (Sep 19 2019 at 13:32):indeed I don't see them
Maxime Dénès (Sep 19 2019 at 13:32):would you mind opening an issue? I'll try to fix it.
Théo Winterhalter (Sep 19 2019 at 13:32):Ok!
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)
Matthieu Sozeau (Sep 23 2019 at 12:20):Found it: using option "install code in PATH"
vlj (Sep 23 2019 at 17:13):Is vscoq still maintained ? Last commit is from 2 years ago, and pr seems not examinated
Maxime Dénès (Sep 23 2019 at 17:49):it is maintained here: https://github.com/coq-community/vscoq
vlj (Sep 23 2019 at 17:50):Thanks !
Maxime Dénès (Sep 23 2019 at 17:50):we haven't released a new version based on this fork, though
Maxime Dénès (Sep 23 2019 at 17:51):hopefully this week!
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...
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
Maxime Dénès (Sep 24 2019 at 16:04):would you mind opening an issue? I'll try to fix it
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
vlj (Sep 24 2019 at 20:04):client code seems compatible with typescript 3+, but not the ones in html_views and server
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)
Paolo Giarrusso (Sep 24 2019 at 20:34):@vlj make seems to do the job here
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
vlj (Sep 24 2019 at 20:50):ok thanks
vlj (Sep 24 2019 at 20:50):do you know how to run the tests ?
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?
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}'
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 ;)
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.
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.
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…
Matthieu Sozeau (Sep 25 2019 at 13:17):Are there a lot of Equations / Program in between the points ?
Matthieu Sozeau (Sep 25 2019 at 13:18):It might be that the STM has more trouble handling these (just a guess)
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.
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
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
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.
Théo Winterhalter (Sep 26 2019 at 08:07):@Maxime Dénès I'll try to make a smaller example than metacoq. :)
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.
Matthieu Sozeau (Sep 27 2019 at 12:55):It seems vscode does not work with 8.9.0, is that expected?
Maxime Dénès (Sep 27 2019 at 14:15):it is not expected, but it hasn't been tested much
Maxime Dénès (Sep 27 2019 at 14:15):do you get an error message ?
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
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)
Maxime Dénès (Sep 27 2019 at 14:40):I can make 8.9.1 work here
Maxime Dénès (Sep 27 2019 at 14:40):I can try 8.9.0
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?
Maxime Dénès (Sep 27 2019 at 14:50):ah no but wait, my test was wrong
Maxime Dénès (Sep 27 2019 at 14:52):this time, I confirm it works for me even with 8.9.0
Matthieu Sozeau (Sep 27 2019 at 15:08):Ok, I'll try again
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?
Maxime Dénès (Sep 27 2019 at 15:36):good point!
Maxime Dénès (Sep 27 2019 at 16:25):it's probably time to make a release to avoid this confusion
Maxime Dénès (Sep 27 2019 at 16:25):we can fix the remaining problems afterwards
vlj (Sep 28 2019 at 16:21):do you have any idea how to retrieve the os in typescript ? using maybe vscode api
vlj (Sep 28 2019 at 18:14):actually it's not necessary, vscode launch .exe even without extension on windows which is nice
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
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
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 :)
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.
vlj (Sep 29 2019 at 14:24):with previous way it seems to work
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)
vlj (Sep 29 2019 at 21:15):another info https://github.com/microsoft/vscode-extension-samples/issues/191
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.
vlj (Sep 30 2019 at 18:51):the README.md files are the same in root directory and client ones ?
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 ?
Maxime Dénès (Oct 03 2019 at 08:54):@Matthieu Sozeau VsCoq should now work fine with a Dune-built Coq
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
Anton Trunov (Oct 03 2019 at 11:58):Hooray!
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
Jad Hamza (Gitter import) (Oct 03 2019 at 12:59):(I also tried compiling the extension from master)
Brendan Zabarauskas (Gitter import) (Oct 03 2019 at 13:18):Woo, congratulations on the release! :tada:
Maxime Dénès (Oct 03 2019 at 14:08):@Brendan Zabarauskas Thanks!
Maxime Dénès (Oct 03 2019 at 14:09):@Jad Hamza do you have a coqidetop.opt in the same directory as coqtop?
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
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
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.
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
Maxime Dénès (Oct 03 2019 at 15:03):why would Coq not recognize a -R flag?
Maxime Dénès (Oct 03 2019 at 15:04):what do you have in your _CoqProject?
Jad Hamza (Gitter import) (Oct 03 2019 at 15:13):I have the -Q . MyProject
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
Maxime Dénès (Oct 03 2019 at 18:21):I can't reproduce it, though. coqtop accepts -Q followed by -R
Maxime Dénès (Oct 03 2019 at 18:24):could you post the full content of your _CoqProject file in a gist?
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
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)
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?
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...
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?
Maxime Dénès (Oct 04 2019 at 06:58):I'm trying it now, to see if I can reproduce
Maxime Dénès (Oct 04 2019 at 06:58):(I'm not using opam usually)
Maxime Dénès (Oct 04 2019 at 06:58):I would hope that installing the coqide package is not necessary
Jad Hamza (Gitter import) (Oct 04 2019 at 06:59):Thanks! Do you install from source?
Maxime Dénès (Oct 04 2019 at 06:59):no, I use nix usually
Maxime Dénès (Oct 04 2019 at 07:00):btw, we should also check what's stored in the preferences
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"
Maxime Dénès (Oct 04 2019 at 07:01):is anything set there?
Maxime Dénès (Oct 04 2019 at 07:01):(file > preferences > settings then you can type coqtop in the filter)
Jad Hamza (Gitter import) (Oct 04 2019 at 07:02):No it's empty
Maxime Dénès (Oct 04 2019 at 07:02):hmmm
Jad Hamza (Gitter import) (Oct 04 2019 at 07:03):I'll try to set it to the above folder
Maxime Dénès (Oct 04 2019 at 07:03):so indeed, coqidetop.opt is installed by the coq opam package
Maxime Dénès (Oct 04 2019 at 07:04):unfortunately, I can't reproduce your problem
Maxime Dénès (Oct 04 2019 at 07:05):I just launched Coq 8.9.1 from VsCoq, after installing it using opam
Maxime Dénès (Oct 04 2019 at 07:05):and it worked fine
Maxime Dénès (Oct 04 2019 at 07:05):let's try coq.dev maybe
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 :(
Jad Hamza (Gitter import) (Oct 04 2019 at 07:08):Seems to be working fine now! Sorry for the wasted time
Maxime Dénès (Oct 04 2019 at 07:09):still, the message was a bit strange, maybe there's something to improve there
Maxime Dénès (Oct 04 2019 at 07:09):were the arguments incorrectly parsed?
Maxime Dénès (Oct 04 2019 at 07:11):do you mean coqtop.args?
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?
Maxime Dénès (Oct 04 2019 at 07:13):I think so, yes
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
Maxime Dénès (Oct 04 2019 at 07:13):I get "coqtop-stderr: Unknown option -R . Top"
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
Jad Hamza (Gitter import) (Oct 04 2019 at 07:15):Have you tried in conjunction with a -Q . MyProject from _CoqProject?
Maxime Dénès (Oct 04 2019 at 07:15):ah no, right!
Maxime Dénès (Oct 04 2019 at 07:17):still the same error message
Maxime Dénès (Oct 04 2019 at 07:17):but ok, never mind I guess
Maxime Dénès (Oct 04 2019 at 07:17):at least it works ;)
Jad Hamza (Gitter import) (Oct 04 2019 at 07:18)::)
Jad Hamza (Gitter import) (Oct 04 2019 at 07:18):Yes thanks!
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?
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).
Maxime Dénès (Oct 04 2019 at 07:20):Feedback welcome if you figure out why they are here :)
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)
Maxime Dénès (Oct 04 2019 at 07:24):oh, that's again strange
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?
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!
Maxime Dénès (Oct 04 2019 at 07:28):you're welcome!
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
vlj (Oct 06 2019 at 14:30):it's likely possible with some regex but I fear some corner cases
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
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)
vlj (Oct 06 2019 at 15:26):ok
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
vlj (Oct 06 2019 at 20:21):@Paolo G. Giarrusso but it doesn't list the symbol currently in the environment ?
vlj (Oct 06 2019 at 20:21):I mean to Require and Print a symbol you must know that it exists
vlj (Oct 06 2019 at 20:30):coq source code is a bit hard to read without experience in ocaml
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.)
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.
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.
vlj (Oct 08 2019 at 19:14):hmm it looks like the parser of coq code in server doesn't work to retrieve symbols
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
Maxime Dénès (Oct 08 2019 at 20:42):parsing coq code on the vscode side is impossible
Maxime Dénès (Oct 08 2019 at 20:42):Coq's parsing is extensible
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
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)
Théo Zimmermann (Oct 08 2019 at 21:30)::sparkling_heart:
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)
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
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.
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).
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.
Matthieu Sozeau (Oct 09 2019 at 07:51):What if you import ascii explicitely?
Maxime Dénès (Oct 09 2019 at 08:12):@Théo Winterhalter would you mind trying the same thing in CoqIDE?
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
Théo Winterhalter (Oct 09 2019 at 08:25):I have to install it then.
Maxime Dénès (Oct 09 2019 at 08:26):ah ah :) sorry about that
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.
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.)
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?
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.
Matthieu Sozeau (Oct 09 2019 at 09:45):Yes, probably a version incompatibility
Théo Winterhalter (Oct 09 2019 at 09:46):I don’t really want to debug coqide for this. Does jscoq support asynchronous compiling?
Matthieu Sozeau (Oct 09 2019 at 09:46):Oh it could be wrong initialization of ML-side references in the MetaCoq plugin
Matthieu Sozeau (Oct 09 2019 at 09:47):If we load (and use?) the plugin before importing ascii
Matthieu Sozeau (Oct 09 2019 at 09:48):Switching to coqlib would fix this
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?
Théo Winterhalter (Oct 09 2019 at 14:52):It’s going to be hard since it seems metacoq has to be involved.
Paolo Giarrusso (Oct 09 2019 at 14:55):@Théo Winterhalter the alternative is opam install coqide (if coq is opam-installed) :-|
Théo Winterhalter (Oct 09 2019 at 14:56):Yeah I’ll do that.
Théo Winterhalter (Oct 09 2019 at 15:28):Alright, the error is also present in coqide, sorry for bringing it up here.
Maxime Dénès (Oct 09 2019 at 15:29):no worries!
Maxime Dénès (Oct 09 2019 at 15:29):thanks for testing
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 ?
Maxime Dénès (Oct 16 2019 at 17:39):oh, it's not a split from the main codebase
Maxime Dénès (Oct 16 2019 at 17:39):it's a phase separation, rather
vlj (Oct 16 2019 at 20:46):what do you mean by phase separation ?
Théo Zimmermann (Oct 17 2019 at 08:19):So that one can request Coq to parse a document without executing it.
Maxime Dénès (Oct 17 2019 at 09:03):exactly
Sequencer (Gitter import) (Oct 17 2019 at 09:28):I heard that original author went to Facebook and never use coq after graduation. LOL
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.
vlj (Oct 17 2019 at 10:40):Thanks for the precision.
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
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.
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
Maxime Dénès (Oct 17 2019 at 21:37):you can "open workspace settings"
Maxime Dénès (Oct 17 2019 at 21:37):then use workbench.colorCustomizations
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
Maxime Dénès (Oct 17 2019 at 21:39):if you're proud of your setup, you can even contribute VsCoq themes :)
Matthieu Sozeau (Oct 17 2019 at 21:51):Yep, I figured it out!
Matthieu Sozeau (Oct 17 2019 at 21:52):Not proud yet :)
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!
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.
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
Matthieu Sozeau (Oct 18 2019 at 11:52):Typing (* inserts (**)) (two ending parens)
Maxime Dénès (Oct 18 2019 at 11:53):can you open issues? so that we don't forget
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
Matthieu Sozeau (Oct 18 2019 at 11:53):After I finish preparing my lecture :)
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.
Matthieu Sozeau (Oct 18 2019 at 11:55):Nice one
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.
Matthieu Sozeau (Oct 18 2019 at 13:23):Nevermind, found it, Selection Highlight
Matthieu Sozeau (Oct 18 2019 at 13:26):And Occurrences Highlight
Paolo Giarrusso (Oct 18 2019 at 16:32):@Matthieu Sozeau the speed issue is indeed why I gave up on Proof General
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
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
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
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
vlj (Oct 18 2019 at 17:12):And pegjs parser almost never return anything useful, there is no symbole listing at all
Maxime Dénès (Oct 18 2019 at 17:13):yeah, we can probably simplify a lot the logic
Maxime Dénès (Oct 18 2019 at 17:13):if you have an example large file, don't hesitate to open an issue
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 ?
vlj (Oct 18 2019 at 17:14):Ok
Maxime Dénès (Oct 18 2019 at 17:14):you still need to parse sentences for now
Maxime Dénès (Oct 18 2019 at 17:14):but yeah, we can probably do it very efficiently
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?
Maxime Dénès (Oct 18 2019 at 17:24):why do we want them in coqide and PG?
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...
Maxime Dénès (Oct 18 2019 at 17:25):because the thing keeps jumping to the other tab
Paolo Giarrusso (Oct 18 2019 at 17:25):@Maxime Dénès I also think we want those
Maxime Dénès (Oct 18 2019 at 17:26):what's the use case?
Paolo Giarrusso (Oct 18 2019 at 17:26):first, "multiple tab" isn't convincing in practice
Paolo Giarrusso (Oct 18 2019 at 17:27):Proof General has only one, and it's better than what we have today in vscoq
Maxime Dénès (Oct 18 2019 at 17:27):I agree, but that doesn't explain why we need these info feedback
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.
Maxime Dénès (Oct 18 2019 at 17:27):the rare case?
Paolo Giarrusso (Oct 18 2019 at 17:27):well, "rare" is provocative, but I'm typing some examples
Paolo Giarrusso (Oct 18 2019 at 17:28):Inductive foo := . is the first counterexample
Maxime Dénès (Oct 18 2019 at 17:28):I'm lost
Maxime Dénès (Oct 18 2019 at 17:28):I'm pretty sure I can read foo in your example
Pierre-Marie Pédrot (Oct 18 2019 at 17:28):it generates foo_ind and whatsnot
Maxime Dénès (Oct 18 2019 at 17:29):ah lol ok
Pierre-Marie Pédrot (Oct 18 2019 at 17:29):depending on the sort
Maxime Dénès (Oct 18 2019 at 17:29):so I think calling literal occurrences rare case is just wrong
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}.
second, you still didn't say what was the use case for the "foo_ind is defined" message
Paolo Giarrusso (Oct 18 2019 at 17:30):that's honestly how I first learned about those things
Paolo Giarrusso (Oct 18 2019 at 17:30):similarly, in my example, I get Reflexive0 is declared
Maxime Dénès (Oct 18 2019 at 17:30):lol
Maxime Dénès (Oct 18 2019 at 17:31):I still think the outline would be better than these messages
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
Maxime Dénès (Oct 18 2019 at 17:32):yeah, this we can talk about, we may want some kind of temporary measure
Maxime Dénès (Oct 18 2019 at 17:33):the Reflexive0 foo example, I'm really not convinced btw
Maxime Dénès (Oct 18 2019 at 17:33):either the name matters, and it should be written by the user
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?
Maxime Dénès (Oct 18 2019 at 17:33):or it doesn't and you wouldn't care about the message
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
Maxime Dénès (Oct 18 2019 at 17:33):ah, good question
Pierre-Marie Pédrot (Oct 18 2019 at 17:33):which lets me a bit clueless
Paolo Giarrusso (Oct 18 2019 at 17:33):the "temporary measure" is the most important part anyway :-)
Paolo Giarrusso (Oct 18 2019 at 17:34):on to Pierre's Q :-)
Maxime Dénès (Oct 18 2019 at 17:34):maybe the first question is why you want a VsCoq specific flag
Pierre-Marie Pédrot (Oct 18 2019 at 17:34):?
Maxime Dénès (Oct 18 2019 at 17:34):i.e. why not put it in _CoqProject
Pierre-Marie Pédrot (Oct 18 2019 at 17:34):oh
Pierre-Marie Pédrot (Oct 18 2019 at 17:34):because I don't believe in the neoliberal project bullshit paradigm
Maxime Dénès (Oct 18 2019 at 17:34):not saying there are no use case
Pierre-Marie Pédrot (Oct 18 2019 at 17:34):open quote close quote
Maxime Dénès (Oct 18 2019 at 17:35):sorry?
Pierre-Marie Pédrot (Oct 18 2019 at 17:35):like, I want a scratchpad
Pierre-Marie Pédrot (Oct 18 2019 at 17:35):to quickly typecheck stuff
Pierre-Marie Pédrot (Oct 18 2019 at 17:35):usually I just fire up coqIDE
Maxime Dénès (Oct 18 2019 at 17:35):I'm afraid we support mainly project-centered stuff
Pierre-Marie Pédrot (Oct 18 2019 at 17:35):and there is a neat option to change the flags
Pierre-Marie Pédrot (Oct 18 2019 at 17:35):ga
Pierre-Marie Pédrot (Oct 18 2019 at 17:35):even PG lets you do that -_-
Paolo Giarrusso (Oct 18 2019 at 17:36):@Pierre-Marie Pédrot seems you want sth. like "coqtop.args": []
Pierre-Marie Pédrot (Oct 18 2019 at 17:36):plus, there are use cases even inside a project
Maxime Dénès (Oct 18 2019 at 17:36):yeah yeah, I'm not saying there are none, I
Pierre-Marie Pédrot (Oct 18 2019 at 17:36):e.g. selectively enabling type-in-type
Maxime Dénès (Oct 18 2019 at 17:36):I'm explaining the state of affairs
Pierre-Marie Pédrot (Oct 18 2019 at 17:36):ok
Paolo Giarrusso (Oct 18 2019 at 17:36):(I just did "Copy Settings as JSON")
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?
Pierre-Marie Pédrot (Oct 18 2019 at 17:36):wdym?
Paolo Giarrusso (Oct 18 2019 at 17:37):is "coqtop.args": ["-type-in-type"] the right syntax?
Maxime Dénès (Oct 18 2019 at 17:37):I think so
Pierre-Marie Pédrot (Oct 18 2019 at 17:37):AFAIK there is no way to selectively compile a file with some flag
Maxime Dénès (Oct 18 2019 at 17:37):now I remember using it
Pierre-Marie Pédrot (Oct 18 2019 at 17:37):using _CoqProject
Maxime Dénès (Oct 18 2019 at 17:37):ah!
Maxime Dénès (Oct 18 2019 at 17:37):nice XY problem, that's actually a good point
Maxime Dénès (Oct 18 2019 at 17:37):is there an open issue about it?
Pierre-Marie Pédrot (Oct 18 2019 at 17:37):not that I know of
Maxime Dénès (Oct 18 2019 at 17:38):type-in-type has become local, right?
Pierre-Marie Pédrot (Oct 18 2019 at 17:38):yes-ish
Pierre-Marie Pédrot (Oct 18 2019 at 17:38):the kind of broken SR local
Maxime Dénès (Oct 18 2019 at 17:38):oh?!
Pierre-Marie Pédrot (Oct 18 2019 at 17:38):well that's expected
Maxime Dénès (Oct 18 2019 at 17:38):like you do foo := bar
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
Maxime Dénès (Oct 18 2019 at 17:39):where bar has been compiled with type-in-type
Pierre-Marie Pédrot (Oct 18 2019 at 17:39):yes
Pierre-Marie Pédrot (Oct 18 2019 at 17:39):that breaks if you unfold
Maxime Dénès (Oct 18 2019 at 17:39):then when you unfold foo you get in trouble
Maxime Dénès (Oct 18 2019 at 17:39):I hadn't realized that when I merged it
Pierre-Marie Pédrot (Oct 18 2019 at 17:39):which is why the unimath people should be using well-scoped resize rules
Pierre-Marie Pédrot (Oct 18 2019 at 17:39):but that's another story
Maxime Dénès (Oct 18 2019 at 17:39):you also didn't say it on the PR, did you?
Pierre-Marie Pédrot (Oct 18 2019 at 17:40):didn't I?
Pierre-Marie Pédrot (Oct 18 2019 at 17:40):at least we track it
Maxime Dénès (Oct 18 2019 at 17:40):maybe I preferred the global behavior then
Pierre-Marie Pédrot (Oct 18 2019 at 17:40):the same issue goes for fixpoint checking
Maxime Dénès (Oct 18 2019 at 17:40):argh
Pierre-Marie Pédrot (Oct 18 2019 at 17:40):it should be stored in the fixpoint, not in the definition
Maxime Dénès (Oct 18 2019 at 17:40):yeah, right
Pierre-Marie Pédrot (Oct 18 2019 at 17:40):this is nonsense
Pierre-Marie Pédrot (Oct 18 2019 at 17:40):like Private Inductive also
Pierre-Marie Pédrot (Oct 18 2019 at 17:40):but it's the kind of broken-by-design feature
Maxime Dénès (Oct 18 2019 at 17:40):yeah
Paolo Giarrusso (Oct 18 2019 at 17:41):(people on coq/coq might also be interested ;-)
Pierre-Marie Pédrot (Oct 18 2019 at 17:41):so, I'm not waging a lost in advance war
Pierre-Marie Pédrot (Oct 18 2019 at 17:41):anyways
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
Maxime Dénès (Oct 18 2019 at 17:41):lol yeah, wrong channel :D
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
Maxime Dénès (Oct 18 2019 at 17:41):you can edit coqtop.args in the JSON
Maxime Dénès (Oct 18 2019 at 17:41):as suggested, right?
Pierre-Marie Pédrot (Oct 18 2019 at 17:41):mkay
Pierre-Marie Pédrot (Oct 18 2019 at 17:42):not super user-friendly but I can live with that
Pierre-Marie Pédrot (Oct 18 2019 at 17:42):thx
Pierre-Marie Pédrot (Oct 18 2019 at 17:42):let's try
Maxime Dénès (Oct 18 2019 at 17:42):it's fairly typical in the vscode world
Maxime Dénès (Oct 18 2019 at 17:42):AFAIK it's like PG where you edit the lisp...
Pierre-Marie Pédrot (Oct 18 2019 at 17:42):screaming "JSON" running around is not going to convince me
Pierre-Marie Pédrot (Oct 18 2019 at 17:42):neither does "ELISP!"
Pierre-Marie Pédrot (Oct 18 2019 at 17:43):(... at least in CoqIDE we have a buffer-local set of values for that)
Paolo Giarrusso (Oct 18 2019 at 17:43):more concretely, there's IDE support for JSON editing which makes it less bad
Paolo Giarrusso (Oct 18 2019 at 17:44):(but I guess a PR for a nicer widget would be accepted)
Pierre-Marie Pédrot (Oct 18 2019 at 17:45):(I have to learn typescript for that first)
Pierre-Marie Pédrot (Oct 18 2019 at 17:45):(btw I thought that the OCaml folks had written BuckleScript bindings for VSCode)
Pierre-Marie Pédrot (Oct 18 2019 at 17:46):(that would allow for the use of some more reasonable language)
Maxime Dénès (Oct 18 2019 at 17:47):for the client part, I think the language doesn't matter so much
Maxime Dénès (Oct 18 2019 at 17:47):for the server, though, I would definitely prefer a saner language
Maxime Dénès (Oct 18 2019 at 17:55):@Pierre-Marie Pédrot let us know if you succeeded in passing the flags
Pierre-Marie Pédrot (Oct 18 2019 at 17:55):yep that worked thanks
vlj (Oct 18 2019 at 18:39):I think it's possible to have on memory buffer in vscode
Paolo Giarrusso (Oct 18 2019 at 19:30):@vlj how do you mean?
Paolo Giarrusso (Oct 18 2019 at 19:57):@Maxime Dénès anyway, thanks a lot for your work here
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)
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?
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
vlj (Oct 24 2019 at 19:34):But the doc is always in sync with coq features
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.
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
Maxime Dénès (Oct 31 2019 at 22:02):@Matthieu Sozeau good point, feel free to open an issue
Maxime Dénès (Oct 31 2019 at 22:02):is there a hoqidetop.opt installed by coq-hott?
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
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
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?
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
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?
Maxime Dénès (Nov 07 2019 at 10:45):it should be easy, yes
Maxime Dénès (Nov 07 2019 at 10:45):it's TS, not JS ;)
Matthieu Sozeau (Nov 08 2019 at 13:19):Right
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 ?
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
Rehan MALAK (Gitter import) (Nov 22 2019 at 16:26):retried today without more success ... (changing coqtop.binPath or coqtop.args in package.json)
Maxime Dénès (Nov 22 2019 at 22:05):what do you get?
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.
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)
Ramkumar Ramachandra (Gitter import) (Jan 06 2020 at 16:19):I've tested it, and can confirm that it works.
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.
Théo Winterhalter (Jan 08 2020 at 10:14):Is it normal?
Maxime Dénès (Jan 08 2020 at 12:40):@Théo Winterhalter not really, do you have a repro case?
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).
Maxime Dénès (Jan 08 2020 at 13:01):it must depend on the kind of tactics you use
Maxime Dénès (Jan 08 2020 at 13:01):or the commands inside a proof, I don't remember
Théo Winterhalter (Jan 08 2020 at 13:01):Oh. I’ll try to see which ones do it.
Maxime Dénès (Jan 08 2020 at 13:01):maybe abstract?
Théo Winterhalter (Jan 08 2020 at 13:01):I don’t use it.
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
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
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.
Maxime Dénès (Jan 08 2020 at 13:08):STM is the Coq component which handles async proofs ;)
Théo Winterhalter (Jan 08 2020 at 13:09):Ok
Théo Winterhalter (Jan 08 2020 at 13:16):I can’t manage to pinpoint where it comes from.
Matthieu Sozeau (Jan 08 2020 at 20:48):@Ramkumar Ramachandra nice!
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.
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) ?
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?
Maxime Dénès (Jan 09 2020 at 15:41):are the various folders corresponding to different projects?
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.
Maxime Dénès (Jan 09 2020 at 15:44):I didn't now this was supported on the Coq side, TBH
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
Maxime Dénès (Jan 09 2020 at 15:45):where is the multiple project files layout documented?
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)
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.
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
Théo Winterhalter (Jan 09 2020 at 16:05):Note that PG already handles this (I don’t know how though).
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)
Maxime Dénès (Jan 09 2020 at 16:06):I think from the VsCoq perspective, we'd need to support multi project workspaces
Maxime Dénès (Jan 09 2020 at 16:06):https://code.visualstudio.com/docs/editor/multi-root-workspaces
Matthieu Sozeau (Jan 09 2020 at 16:07):Yep, that's another way
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?
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?
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
Maxime Dénès (Jan 09 2020 at 16:12):if it doesn't, I guess we can consider it a VsCoq bug
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
Maxime Dénès (Jan 09 2020 at 16:13):why wouldn't it work for the submodule case?
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)
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...
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
Maxime Dénès (Jan 09 2020 at 17:25):well, the submodule is usually another project, really, no?
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
Matthieu Sozeau (Jan 09 2020 at 17:26):The coqtop will point to the enclosing Coq though...
Matthieu Sozeau (Jan 09 2020 at 17:26):Yep, not sure either
Maxime Dénès (Jan 09 2020 at 17:26):coqtop?
Maxime Dénès (Jan 09 2020 at 17:26):do you use several copies of coq?
Matthieu Sozeau (Jan 09 2020 at 17:26):The coqtop with which you will want to run the submodule code
Maxime Dénès (Jan 09 2020 at 17:27):I'm a bit lost, what does coqtop have anything to do with this?
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?
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/
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.
Théo Winterhalter (Jan 15 2020 at 16:56):Anyway there are serious synchronisation problems when files are large.
Théo Winterhalter (Jan 15 2020 at 18:45): 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!)
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
Paolo Giarrusso (Jan 15 2020 at 20:14):(but restarting vscoq still seems faster than using proof general :-| )
Paolo Giarrusso (Jan 15 2020 at 20:14):(but let’s see if that’s the same issue I have)
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.
Maxime Dénès (Jan 15 2020 at 22:07):there were a lot of modifications recently
not really, were there?
Maxime Dénès (Jan 15 2020 at 22:07):but yeah, master has an important fix related to sync issues
Maxime Dénès (Jan 15 2020 at 22:07):so expect a release very soon
Maxime Dénès (Jan 15 2020 at 22:14):but the fixed issue is only when you use vscode's undo
Maxime Dénès (Jan 15 2020 at 22:15):so I'm not sure if it is your problem
Maxime Dénès (Jan 15 2020 at 22:15):I've also made significant progress on the document manager
Maxime Dénès (Jan 15 2020 at 22:15):getting rid of the server in VsCoq should fix a lot of these issues
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).
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.
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.
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
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
Ramkumar Ramachandra (Gitter import) (Jan 16 2020 at 07:52):Oh, nice! Can you point me to the branch or PR?
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
Théo Winterhalter (Jan 16 2020 at 07:55):Ok cool! I’m looking forward to this. Thanks a lot!
Ramkumar Ramachandra (Gitter import) (Jan 16 2020 at 07:57):Cool. Looks like it's going to take a while.
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.
Maxime Dénès (Jan 16 2020 at 08:01):well, that's not LSP, it's LSP + extension
Maxime Dénès (Jan 16 2020 at 08:02):but yeah, the idea is to make the life of all IDEs easier
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.
Maxime Dénès (Jan 16 2020 at 08:04):well, it is more or less the protocol that the VsCoq client speaks already
Ramkumar Ramachandra (Gitter import) (Jan 16 2020 at 08:04):Right.
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.
Maxime Dénès (Jan 16 2020 at 08:06):yeah, I'll try to have a look quickly
Maxime Dénès (Jan 16 2020 at 08:06):like this week
Ramkumar Ramachandra (Gitter import) (Jan 16 2020 at 08:06):Okay.
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?
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
Maxime Dénès (Jan 29 2020 at 09:53):would you mind opening an issue?
Théo Winterhalter (Jan 29 2020 at 09:53):Ok!
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.
Paolo Giarrusso (Feb 10 2020 at 21:32):@Narek Asadorian some of the data for completion lives in data files in the plugin
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.
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.
Narek Asadorian (Gitter import) (Feb 10 2020 at 22:15):Automated does sound a lot nicer though.
Narek Asadorian (Gitter import) (Feb 10 2020 at 22:19):Does the case split thing sound feasible at all?
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.
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.
Narek Asadorian (Gitter import) (Feb 10 2020 at 23:08):Have not tried Proof General either, but I'm not an emacs person :)
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.
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
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
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?
Maxime Dénès (Feb 13 2020 at 09:53):I would be surprised if reinstalling fixes it
Maxime Dénès (Feb 13 2020 at 09:53):But it probably isn't really random
Maxime Dénès (Feb 13 2020 at 09:53):maybe triggered by a complex chain of actions
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.
Maxime Dénès (Feb 13 2020 at 09:55):Sorry for the inconvenience
Enzo Crance (Gitter import) (Feb 13 2020 at 09:56):One cannot solve every single bug
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.
Enzo Crance (Gitter import) (Feb 13 2020 at 09:57):I’ll keep you updated! :)
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
Maxime Dénès (Feb 13 2020 at 16:34):Thanks, I'll try to have a look when I can
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.
Maxime Dénès (Feb 28 2020 at 10:53):sure, I was planning to do one today
Maxime Dénès (Feb 28 2020 at 10:53):sorry for the delay
Théo Winterhalter (Feb 28 2020 at 10:53):Nice!
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 :)
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
Maxime Dénès (Feb 28 2020 at 14:25):@Matthieu Sozeau see https://github.com/coq-community/vscoq/pull/97
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.
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
Maxime Dénès (Feb 28 2020 at 14:46):not sure what the difference is between the two
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.
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
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.
Maxime Dénès (Feb 28 2020 at 14:55):I'm afraid there's a fundamental problem
Maxime Dénès (Feb 28 2020 at 14:56):Coq's interaction model assumes some regions are untouchable
Maxime Dénès (Feb 28 2020 at 14:56):i.e. cannot be edited, in certain states
Théo Winterhalter (Feb 28 2020 at 14:56):I’m trying to pintpoint the problem again.
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.
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.
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
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)
Maxime Dénès (Feb 28 2020 at 15:01):I started to work on it, but I need more time to complete it
Théo Winterhalter (Feb 28 2020 at 15:02):Yeah I know.
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
Maxime Dénès (Feb 28 2020 at 15:02):we can anyway make a new release soon
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…
Maxime Dénès (Feb 28 2020 at 15:50):I also failed to reproduce it :(
Maxime Dénès (Feb 28 2020 at 15:51):it does occur in https://github.com/coq-community/vscoq/issues/116 though
Maxime Dénès (Feb 28 2020 at 15:51):fairly reliably
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
Théo Winterhalter (Feb 28 2020 at 15:52):It might be the same kind of problem yes.
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?
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.
Maxime Dénès (Feb 28 2020 at 18:37):(I did one today for the important undo-related fix)
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.)
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.
Paolo Giarrusso (Feb 28 2020 at 20:45):does any of you have code where Coq: Reset works?
Théo Winterhalter (Feb 28 2020 at 21:17):Not really…
Paolo Giarrusso (Feb 28 2020 at 21:47):okay, so @Maxime Dénès must have such an example.
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
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.
Théo Winterhalter (Feb 29 2020 at 09:43):(They’re on Ubutun/Debian)
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.
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
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
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?
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
Paolo Giarrusso (Mar 11 2020 at 16:49):but the comment suggests that's not intended so you're right
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
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
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
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.
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
Jad Hamza (Gitter import) (Mar 13 2020 at 12:58):@Théo Winterhalter Ah cool! How does it work in Proof General and CoqIde?
Théo Winterhalter (Mar 13 2020 at 13:25):I don’t know. :-/
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?
Jad Hamza (Gitter import) (Mar 13 2020 at 13:38):(or here: https://github.com/coq/coq/blob/3449c8a088e9a902ebc73478667f4f25d6c08d2a/vernac/himsg.ml#L1373)
Jad Hamza (Gitter import) (Mar 13 2020 at 14:26):Hmm VsCoq does send a SIGINT signal to coqtop
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.
Paolo Giarrusso (Mar 13 2020 at 15:33):I know by heart because it’s a regular part of my workflow.
Paolo Giarrusso (Mar 13 2020 at 15:57)::worried:
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)
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?
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
Paolo Giarrusso (Mar 13 2020 at 18:15):@Jad Hamza wat
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)
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)
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?
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
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
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
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.
Paolo Giarrusso (Apr 12 2020 at 21:14):It does work under some minimal testing.
Jad Hamza (Gitter import) (Apr 13 2020 at 06:43):Thanks :)
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?
Alex Gryzlov (Gitter import) (Apr 23 2020 at 22:58):what's the zulip server?
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: Jun 04 2023 at 23:30 UTC