Ali Caglayan (Mar 09 2022 at 10:42): Ali Caglayan (Mar 09 2022 at 10:42):I just found out that the stm takes its own command line arguments https://github.com/coq/coq/blob/92b9d3ca9928e8332ac81175272e8e4489961d71/stm/stmargs.ml
Ali Caglayan (Mar 09 2022 at 10:43):Michael's message confused me because I recently updated the help screen for CoqIDE and I don't remember seeing the async stuff.
Ali Caglayan (Mar 09 2022 at 10:44):So CoqIDE has a -coqtop-flags flag for passing options to the subprocess. Does VSCoq have something similar?
Paolo Giarrusso (Mar 09 2022 at 10:44):@Michael Soegtrop VsCoq just passes -async-proofs on, I didn't know about this -j option. But do we just need to add a setting and slap the option in?
Michael Soegtrop (Mar 09 2022 at 10:44):@Ali Caglayan : it might be that it was removed from the docs because it was quite unstable for a long time (at least on Windows due to a bug in GtkSourceView which killed global data structures on each thread kill).
Paolo Giarrusso (Mar 09 2022 at 10:45):Hmm, time to try "Coqtop: Args" by hand first...
Michael Soegtrop (Mar 09 2022 at 10:47):@Paolo Giarrusso : I guess so, but Enrico is the expert.
Where would I put "Coqtop: Args"? In _CoqProject?
Ali Caglayan (Mar 09 2022 at 10:48):I think in vscoq's config right?
Paolo Giarrusso (Mar 09 2022 at 10:49):yes, I just added "coqtop.args": ["-async-proofs-j", "10"] to settings.json, and it passes a smoke test
Michael Soegtrop (Mar 09 2022 at 10:50):Cool - I will try it right away ... (after I finished the test suggested by Guillaume with CoqIDE 8.12..8.15 and VsCoq).
Paolo Giarrusso (Mar 09 2022 at 10:50):and you'll have to make sure to restart coqidetop to confirm
Ali Caglayan (Mar 09 2022 at 10:51):I've split this thread to make the original a bit less cluttered
Paolo Giarrusso (Mar 09 2022 at 10:52):Coq: Reset (often?) doesn't restart the process, so my usual options killall coqidetop.opt, or Cmd-Shift-P"Developer: Reload Window".
Ali Caglayan (Mar 09 2022 at 10:52):I also do the reload window workaround
Michael Soegtrop (Mar 09 2022 at 10:52):I guess I will just restart VsCode ...
Paolo Giarrusso (Mar 09 2022 at 10:52):the latter's cool because it keeps even unsaved file contents :-D
Ali Caglayan (Mar 09 2022 at 10:53):One of the reasons I don't like using VSCoq for other stuff
Michael Soegtrop (Mar 09 2022 at 17:26):Paolo Giarrusso said:
yes, I just added
"coqtop.args": ["-async-proofs-j", "10"]tosettings.json, and it passes a smoke test
I tested this and indeed I get the expected speed up. Very nice! I would suggest to add an explicit "threads" option to the UI settings.
It is interesting that this very nice feature apparently ended up in oblivion - I guess cause of the initial stability issues. For me the parallel proof feature really saves quite a bit of time.
So right now for me (that is from the very subjective view point of my work) the only reason for using CoqIDE is the Ltac debugger, but I don't use it that regularly, so I will probably stick with VsCoq.
Maxime Dénès (Mar 09 2022 at 17:40):Thanks a lot for the feedback, Michael! Do not hesitate to open an issue on the VsCoq repo for the threads configurability improvement.
Michael Soegtrop (Mar 09 2022 at 18:31):I created issue (https://github.com/coq-community/vscoq/issues/284).
Paolo Giarrusso (Mar 09 2022 at 21:47):I totally agree we should have an option :-)
Paolo Giarrusso (Mar 09 2022 at 21:58):and it's easy enough that I'm on it :-)
Paolo Giarrusso (Mar 09 2022 at 22:21):I don't really know what I'm doing, but things like this seem easy to add, also thanks to VSCode's IDE support: https://github.com/coq-community/vscoq/pull/285
Last updated: Apr 20 2024 at 15:01 UTC