Stream: Coq users

Topic: Stop processing a file in the middle?


view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:07):

Is there an equivalent of the lean #exit command in Coq? This command (prints a warning and) stops file processing, as if the rest of the file had been commented out. I see things like Abort but they seem to be about stopping proofs, not full file processing.

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:08):

(* seems to work but it leaves coq rather upset about an unclosed block comment

view this post on Zulip Gaëtan Gilbert (Dec 13 2023 at 14:13):

there's Quit. for coqtop but it's not supported by coqc

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:13):

ah perfect, that works in vscoq as well

view this post on Zulip Gaëtan Gilbert (Dec 13 2023 at 14:14):

what's the use case?

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:15):

to stop heating up my computer while debugging/logging something in the middle of a big file

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:15):

I suppose this is not a problem with the older style with manual running of commands

view this post on Zulip Gaëtan Gilbert (Dec 13 2023 at 14:19):

I wonder what vscoq does with Quit
the only reference I can find with https://github.com/search?q=repo%3Acoq-community%2Fvscoq%20Quit&type=code seems like it's for code highlighting or some such thing
maybe it's failing to recover from the parse error on an unknown command and any syntax error would work? I don't know if it has parse error recovery
(I don't have vscode so no testing myself)

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:19):

oh actually no it does nothing

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:20):

the highlighting and very slow refresh was fooling me

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:21):

it says Command not supported (No proof-editing in progress).

view this post on Zulip Gaëtan Gilbert (Dec 13 2023 at 14:21):

this feature probably needs to be handled on the vscoq side not coq-core
if we had a regular command that called exit it would kill the worker which isn't what you want (AFAICT), so vscoq needs to handle it specially

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:22):

why wouldn't it be handled by the core (e.g. coqc as well)?

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:22):

It shouldn't literally quit the program, it should just not run the rest of the commands

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:23):

at least that's how #exit works

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:23):

it's more or less equivalent to just truncating the file after the keyword

view this post on Zulip Gaëtan Gilbert (Dec 13 2023 at 14:23):

for coqc "not run the rest of the commands" means process termination, but for interactive UI you still want to be able to backtrack without rerunning everything

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:24):

doesn't coqc also have cleanup actions after all commands are processed? e.g. writing .vo

view this post on Zulip Gaëtan Gilbert (Dec 13 2023 at 14:24):

that's true

view this post on Zulip Gaëtan Gilbert (Dec 13 2023 at 14:25):

I still think it needs per-UI handling

view this post on Zulip Gaëtan Gilbert (Dec 13 2023 at 14:26):

also not sure how useful it is when you can just actually truncate or comment the rest of the file

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:26):

commenting is annoying though since you have to put something at the end of the file

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:27):

At least in lean I use #exit all the time when writing proofs in a large existing file to keep lean responsive

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:28):

it works well with snapshotting, lean will remember the state after each command so only the command being touched gets reprocessed on each edit if you have an #exit after the command, rather than the whole rest of the file

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:29):

I'm not sure to what extent vscoq or other document-model UIs for Coq do snapshotting

view this post on Zulip Pierre Roux (Dec 13 2023 at 14:31):

In proofgeneral, it doesn't make much sense because the model is "compile to cursor" so we can workout 30000 lines long files without issue (other than it can initially take a bit of time to get to the point to edit).

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:31):

right, this is a problem unique to document model UIs

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:32):

although the concept of a Quit command applies regardless of whether it's coqc or proofgeneral or vscoq handling it

view this post on Zulip Pierre Roux (Dec 13 2023 at 14:33):

Sure, it's just unneeded (I usually just put some random text like "HERE" where I stopped working then comile to the end and it stops by failing on the random text).

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:35):

I think that trick doesn't work in vscoq, it will fail to parse HERE Lemma ... but it will continue parsing commands after the next dot

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:35):

I haven't tried it in coqc

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:36):

so far (* is the only thing I have found which works

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:36):

but it is very obviously a hack

view this post on Zulip Gaëtan Gilbert (Dec 13 2023 at 14:37):

if you want coqc to actually produce the .vo making a fully closed comment or deleting text is the only thing that will work I think
(* is no more a hack than HERE

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:37):

true, HERE is also a hack. It just doesn't work in this case

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:37):

Quit. is the non-hack option

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:37):

but it sounds like support for it is spotty

view this post on Zulip Gaëtan Gilbert (Dec 13 2023 at 14:38):

Quit. isn't the right semantics though
using it in proofgeneral instead of HERE will kill the coq process when it's reached

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:39):

hm yeah actually killing the process is not a great option

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:40):

for an lsp server that's obviously bad

view this post on Zulip Gaëtan Gilbert (Dec 13 2023 at 14:40):

Quit. is really just designed for the ancient model of using coqtop in a terminal emulator for people who don't know about control-d

view this post on Zulip Mario Carneiro (Dec 13 2023 at 14:47):

it seems plausible that you could still get the right behavior in coqtop if Quit. terminates the file, and of course it's always still a possibility to have UIs include custom support for this keyword (IIUC) if they want to implement editor-specific behavior

view this post on Zulip Paolo Giarrusso (Dec 13 2023 at 16:52):

Vscoq 2 supports (old-style) manual checking. For coq-lsp, there's some support now, but @Emilio Jesús Gallego Arias prefers Isabelle's model where this is handled intelligently behind the user's back. However, everybody pointed to Isabelle and Lean as evidence that manual control isn't needed?

view this post on Zulip Paolo Giarrusso (Dec 13 2023 at 16:53):

Either way, based on what Emilio writes/what I see, the Isabelle heuristics aren't implemented fully in either coq-lsp, or especially vscoq2.

view this post on Zulip Mario Carneiro (Dec 13 2023 at 16:53):

Oh, in case it wasn't clear I'm very much in favor of the document model and would not go back. But it does encourage a slightly different use of existing features

view this post on Zulip Mario Carneiro (Dec 13 2023 at 16:54):

in particular, "manual checking" is definitely not what I want

view this post on Zulip Mario Carneiro (Dec 13 2023 at 16:54):

but maybe "don't check stuff which is off screen" is an okay low-input alternative solution

view this post on Zulip Paolo Giarrusso (Dec 13 2023 at 16:55):

That's indeed one of Isabelle's heuristics, from what Emilio says

view this post on Zulip Paolo Giarrusso (Dec 13 2023 at 16:56):

I think you usually want to check offscreen stuff too, but with lower priority — and expensive logging raises challenges.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2023 at 16:56):

@Mario Carneiro you may be interesting in trying coq-lsp or VsCoq1; I have found very large differences between files, for example VsCoq 2 takes 3 minutes on TLC files, whereas coq-lsp or coqc take 3 seconds. I think there are some more bug fixes to come for VsCoq 2. I tried it Monday and indeed it quickly became unusable taking 100% CPU time

view this post on Zulip Mario Carneiro (Dec 13 2023 at 16:57):

the biggest issue with processing the rest of the file is if it causes a delay in responsiveness to further edits

view this post on Zulip Mario Carneiro (Dec 13 2023 at 16:58):

I have noticed some significant delays between editing and seeing updated info, unsure whether this is a factor

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2023 at 16:58):

Isabelle heurisitics are like 2h job if someone would like to implement them.

I didn't do that right away as I requested the LSP devs to add native support for it to the protocol; however that's gonna take a while, as my preferred standard setup for that is Pull Diags + Progress + extension for viewRange, clients are very far from supporting the first 2 in the combo

Mario Carneiro said:

the biggest issue with processing the rest of the file is if it causes a delay in responsiveness to further edits

Yes that was my problem, coq-lsp should not have that problem.

view this post on Zulip Paolo Giarrusso (Dec 13 2023 at 16:58):

but does coq-lsp have working interruption on OCaml 4?

view this post on Zulip Mario Carneiro (Dec 13 2023 at 16:59):

Is there any coq ide with go to definition yet? This is really important for me and it seems like the necessary support infrastructure doesn't even exist yet

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2023 at 17:03):

On VsCode? I am not sure, coq-lsp has jump to definition but only in the same file, full project support is almost done.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2023 at 17:04):

Paolo Giarrusso said:

but does coq-lsp have working interruption on OCaml 4?

Depends on you define working, happy to expand more on that, but maybe in the coq-lsp forum.

But yes, anything not interrupted in OCaml 4 is a bug (actually the runtime interrupt method is _not_ available in OCaml 5, so OCaml 4 has very very good support, but the newer method is in a PR, but working pretty well if you need it)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2023 at 17:06):

Let me know @Mario Carneiro if you need any help with coq-lsp, and if it works well for your use case.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2023 at 17:07):

For MetaCoq from sources, you need to use the multiple workspaces setup, happy to provide you a working file if you need it.

view this post on Zulip Mario Carneiro (Dec 13 2023 at 17:07):

is that another extension or the backend of vscoq (1? 2?)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2023 at 17:07):

VsCoq 1 , VsCoq 2, and coq-lsp are as of today tollay disjoint projects, code wise, both on client and server

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2023 at 17:09):

Tho the very first version of VsCoq 2 was based on coq-lsp first code (Coq's PR 12461)

view this post on Zulip Maxime Dénès (Dec 14 2023 at 08:16):

Emilio Jesús Gallego Arias said:

Tho the very first version of VsCoq 2 was based on coq-lsp first code (Coq's PR 12461)

Discussions on coq-lsp's first code were of inspiration for VsCoq 2. AFAIK, they never shared any significant piece of code, beyond a few trivial lines for jsonrpc printing. In particular, in the PR you point to, all the core logic such as the document representation, state invalidation, task scheduling and delegation, etc, were all newly implemented (and are still what VsCoq 2 is based on today).


Last updated: Jun 18 2024 at 22:01 UTC