Ability to stop, or restart, typechecking somehow

UlfNorell commented 10 years ago

From stevan.a...@gmail.com on June 21, 2012 16:42:26

Back when typechecking was non-interactive, one used to be able to interrupt it by hitting C-g. With the new interactive typechecking one has to wait or restart Agda. I quite often start the typechecker, realise that something is obviously wrong and would like to be able to stop the typechecker.

Original issue: http://code.google.com/p/agda/issues/detail?id=668

UlfNorell commented 10 years ago

From nils.anders.danielsson on June 21, 2012 15:54:51

Things haven't really changed much:

C-g has never interrupted the background process.
C-c C-x C-r (still) interrupts and restarts the process.
Now you can interrupt /highlighting/ by modifying the buffer.

I don't think we should change the meaning of C-g. Perhaps the present interface should be more discoverable. Do you have any suggestions?

Status: InfoNeeded

UlfNorell commented 10 years ago

From stevan.a...@gmail.com on June 22, 2012 05:36:49

Here is a concrete example. Say that you do something stupid like:

loop : Bool loop = loop

bad : loop == true bad = refl

And you start the typechecker. After a second you realise that this isn't the smartest program you written and you want to stop the typechecker. Before typechecking was interactive, C-g would let you interrupt the typechecker. Nowadays you have to restart Agda (C-c C-x C-r).

So I reckon C-g's meaning has changed? I like the new interactive checking, but could we have the old C-g behaviour with it?

UlfNorell commented 10 years ago

From nils.anders.danielsson on June 22, 2012 11:22:29

Before typechecking was interactive, C-g would let you interrupt the typechecker.

No, it unlocked Emacs, but the type-checker was still running in the background.

UlfNorell commented 10 years ago

From stevan.a...@gmail.com on June 26, 2012 07:10:16

I see. I suppose that unlocking Emacs and then issuing C-c C-l again made it feel like you interrupted it, and then restarted it. While now it says that another command is already running when you try to hit C-c C-l again.

What about prompting the user if she wants to restart typechecking, if she hits C-c C-l while the checker is already running?

Summary: Ability to stop, or restart, typechecking somehow

UlfNorell commented 10 years ago

From nils.anders.danielsson on June 26, 2012 07:17:00

What about prompting the user if she wants to restart typechecking, if she hits C-c C-l while the checker is already running?

Why not just let the user restart Agda?

UlfNorell commented 10 years ago

From stevan.a...@gmail.com on June 26, 2012 12:21:30

I dunno, but to me it feels like it takes a lot longer to restart Agda and then restart typechecking now than C-g and restarting typechecking used to take.

Aren't all imported modules rechecked after a restart? They will be skipped, but still.

UlfNorell commented 10 years ago

From nils.anders.danielsson on June 27, 2012 02:22:14

If you did C-g + reload previously, then the following happened (unless I'm completely mistaken):

1) The initial command (that you thought you aborted) ran to completion.

2) The module was reloaded.

There is currently no way to abort a running command without restarting Agda.

UlfNorell commented 10 years ago

From guillaum...@gmail.com on July 05, 2012 00:33:45

I can confirm what Stevan says.

With Agda 2.3.0 I had often the following workflow:

Type C-t in a goal to know what I have to prove
Notice that the type of the goal will take too much time to normalize, so type C-g to interrupt the normalization process
And then type C-u C-t to have the unnormalized form instead

Now I can’t do this anymore and if I need to restart Agda with C-c C-x C-r, or even only reload the module, this will take much more time. Nothing was reloaded before, I could just interrupt normalization of the goal and get the unnormalized form immediately after.

Perhaps that the agda process was not physically interrupted, I don’t remember, but at least from a user point of view I can’t tell the difference and the previous behaviour was more convenient.

UlfNorell commented 10 years ago

From nils.anders.danielsson on July 05, 2012 04:59:06

Perhaps that the agda process was not physically interrupted, I don’t remember, but at least from a user point of view I can’t tell the difference and the previous behaviour was more convenient.

My understanding was that, even if you "interrupted" the first command, it would still run to completion before the second command was run. Did you experience a delay after invoking the second command?

Anyway, it doesn't really matter what the old behaviour was, it is clear that you both want to have the ability to interrupt a command without restarting Agda. Perhaps this could be accomplished by having a separate thread (in the Agda process) which interprets user commands. I don't plan to implement something like this in the near future, but patches are welcome.

Status: Accepted
Labels: Type-Enhancement Priority-Low

UlfNorell commented 10 years ago

From andreas....@gmail.com on October 23, 2012 03:58:19

Issue 725 has been merged into this issue.

Cc: div...@gmail.com

UlfNorell commented 10 years ago

From andreas....@gmail.com on October 23, 2012 03:59:24

Note: there is some discussion on a transactional interaction model on issue 725 .

UlfNorell commented 10 years ago

From nils.anders.danielsson on October 23, 2012 04:09:01

Issue 725 has been merged into this issue.

UlfNorell commented 10 years ago

From andreas....@gmail.com on October 24, 2012 00:18:59

Issue 725 has been merged into this issue.

UlfNorell / agda-test

Ability to stop, or restart, typechecking somehow #668