Stream: Coq devs & plugin devs

Topic: Options to coqidetop in VSCoq


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Mar 09 2022 at 10:45):

Hmm, time to try "Coqtop: Args" by hand first...

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Mar 09 2022 at 10:48):

I think in vscoq's config right?

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Mar 09 2022 at 10:50):

and you'll have to make sure to restart coqidetop to confirm

view this post on Zulip Ali Caglayan (Mar 09 2022 at 10:51):

I've split this thread to make the original a bit less cluttered

view this post on Zulip 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".

view this post on Zulip Ali Caglayan (Mar 09 2022 at 10:52):

I also do the reload window workaround

view this post on Zulip Michael Soegtrop (Mar 09 2022 at 10:52):

I guess I will just restart VsCode ...

view this post on Zulip Paolo Giarrusso (Mar 09 2022 at 10:52):

the latter's cool because it keeps even unsaved file contents :-D

view this post on Zulip Ali Caglayan (Mar 09 2022 at 10:53):

One of the reasons I don't like using VSCoq for other stuff

view this post on Zulip Michael Soegtrop (Mar 09 2022 at 17:26):

Paolo Giarrusso said:

yes, I just added "coqtop.args": ["-async-proofs-j", "10"] to settings.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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Mar 09 2022 at 18:31):

I created issue (https://github.com/coq-community/vscoq/issues/284).

view this post on Zulip Paolo Giarrusso (Mar 09 2022 at 21:47):

I totally agree we should have an option :-)

view this post on Zulip Paolo Giarrusso (Mar 09 2022 at 21:58):

and it's easy enough that I'm on it :-)

view this post on Zulip 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: Dec 05 2023 at 04:01 UTC