What if type-checking does not terminate in LSP? How to interrupt?

[amelieled]

I've got a problem between the CPU and the lambdapi. I don't know why, but when I opened the file "tp2. lp" (see below), automatically, this process uses 100% of my CPU. After a backup, this process stops and if I try to kill it, it'll duplicate itself. . . So the only way to kill the emacs window is to shut down my computer.

// Property type
constant symbol Prop : TYPE
injective symbol P : Prop ⇒ TYPE
set declared "π"
definition π ≔ P
set builtin "P" ≔ π

// Set type
constant symbol Set : TYPE
injective symbol T : Set ⇒ TYPE
set declared "τ"
definition τ ≔ T
set builtin "T" ≔ τ

// Boolean type
constant symbol bool : Set
definition B ≔ τ bool
rule T bool       → B
constant symbol true : B
constant symbol false : B

// Nat type
constant symbol nat  : Set
definition N ≔ τ nat
rule T nat        → N
constant symbol zero : N
constant symbol succ : N ⇒ N
set builtin "0"  ≔ zero
set builtin "+1" ≔ succ

// Leibniz equality
constant symbol eq {a} : τ a ⇒ τ a ⇒ Prop
set infix 1 "=" ≔ eq
constant symbol eq_refl {a} (x:τ a) : P (x = x)
constant symbol eq_ind {a} (x y:τ a) :
       P (x = y) ⇒ ∀p, P (p y) ⇒ P (p x)

////////////////////////////////////
// Avant de prendre la route...
////////////////////////////////////

// Inductive route : Type :=
// | departementale : route
// | nationale : route
// | autoroute : route.                                  

constant symbol route          : Set // FB mieux ?
definition R ≔ τ route
constant symbol departementale : R
constant symbol nationale      : R
constant symbol autoroute      : R

// Definition agrandir (r : route) := 
//   match r with
//  | departementale => nationale
//  | nationale => autoroute
//  | autoroute => autoroute
//  end.

symbol agrandir : R ⇒ R
rule agrandir departementale → nationale
 and agrandir nationale      → autoroute
 and agrandir autoroute      → autoroute

// Eval compute in (agrandir (agrandir nationale)).
compute (agrandir (agrandir nationale))

theorem agrandir_test :
π ((agrandir (agrandir nationale)) = autoroute)
proof
 simpl
 refine eq_refl autoroute
qed

//Inductive terrain : Type :=
//| t_terre : terrain
//| t_route : route -> terrain
//| t_batiment : terrain.

constant symbol terrain    : Set // FB mieux ?
definition Ter ≔ τ terrain
constant symbol t_terre    : Ter
constant symbol t_route    : R ⇒ Ter
constant symbol t_batiment : Ter

//Check (t_route nationale).
type (t_route nationale)

/////////////////////////////
// Exercice 1. - Booléen
/////////////////////////////

require open tests.preuves_Ledein.myLib.Bool
constant symbol true : B
constant symbol false : B

//Check true.
type true

//Print bool.
// ??

//Definition negb b :=
//  match b with
//  | true => false
//  | false => true
//  end.

symbol negb : B ⇒ B
rule negb true → false
 and negb false → true

// Définir les fonctions [andb] et [orb] sur les booléens

// Definition andb b1 b2 :=
//  match b1 with
//  | true => b2
//  | false => false
//  end.

symbol andb : B ⇒ B
rule andb false _  → false
 and andb _ false  → false
 and andb &b1 true → &b1
 and andb true &b2 → &b2

// Definition orb b1 b2 :=
//   match b1 with
//   | true => true
//   | false => b2
//   end.

symbol orb : B ⇒ B
rule orb true _  → true
 and orb _ true  → true
 and orb &b1 false → &b1
 and orb false &b2 → &b2 

[amelieled]

I've just targeted the problem a bit more: in fact, I've merged my 2 files above. The first one contains the following lines, and they are the problem, because when I comment the "require open" line, the process doesn't use 100% of the CPU anymore. By the way, I'm modifying an error in the code above (which doesn't change the problem).

// Property type
constant symbol Prop : TYPE
injective symbol P : Prop ⇒ TYPE
set declared "π"
definition π ≔ P
set builtin "π" ≔ P

// Set type
constant symbol Set : TYPE
injective symbol T : Set ⇒ TYPE
set declared "τ"
definition τ ≔ T
set builtin "τ" ≔ T

// Boolean type
constant symbol bool : Set
definition B ≔ τ bool
rule T bool       → B
constant symbol true : B
constant symbol false : B

// Nat type
constant symbol nat  : Set
definition N ≔ τ nat
rule T nat        → N
constant symbol zero : N
constant symbol succ : N ⇒ N
set builtin "0"  ≔ zero
set builtin "+1" ≔ succ

[rlepigre]

I'm not sure how to reproduce this, I do not have emacs set up correctly at the moment. @gabrielhdt can you try? All I can say is that the problem does not seem to come from Lambdapi itself since it terminates immediately on this second file. I suspect the issue comes from either the LSP server or from the Emacs plugin we use for LSP.

[fblanqui]

@amelieled what happens if you use https://github.com/Deducteam/lambdapi/pull/308 ?

[gabrielhdt]

@amelieled what happens if you use #308 ?

In fact she already has the new mode, so it might come from it... but I don't think so, since the mode does not introduce any computation related to lambdapi

[gabrielhdt]

It works for me (I use #308)

[amelieled]

Yes I have the new mode of Gabriel but if I add "(load "lambdapi") in .emacs, I have the same problem. In fact, if I try to write a theorem after the short extract of my code (not the large one), it doesn't work.

I should install #308 ?

[fblanqui]

I believe that, in Gabriel's mode, you must not add (load "lambdapi"). @gabrielhdt do you confirm? This is perhaps the reason why it is looping.

[amelieled]

Yes you right @fblanqui , and that's why I add it to disable Gabriel's mode. Is it enough @gabrielhdt ? But I have the same problem with/without this mode.

[fblanqui]

Well, I am not sure anymore because, if I do not add (load "lambdapi"), then it doesn't work.

[gabrielhdt]

For the record, package-delete can be used to remove packages.

[amelieled]

ok maybe the problem comes from a bad use for "set builtin"/"set declared"/"definition". This another version, but I don't understand why the theorem declaration gives me a "error on command" (it doesn't infer the sort for "\forall (n:?854) , pi (eq nat n n)") :

// Property type
constant symbol Prop : TYPE
set declared "π"
injective symbol π : Prop ⇒ TYPE

// Set type
constant symbol Set : TYPE
set declared "τ"
injective symbol τ : Set ⇒ TYPE

// Boolean type
constant symbol bool : Set
definition B ≔ τ bool
rule τ bool        → B
constant symbol true : B
constant symbol false : B

// Nat type
constant symbol nat  : Set
definition N ≔ τ nat
rule τ nat        → N
constant symbol zero : N
constant symbol succ : N ⇒ N
set builtin "0"  ≔ zero
set builtin "+1" ≔ succ

// Leibniz equality
constant symbol eq {a} : τ a ⇒ τ a ⇒ Prop
set infix 1 "=" ≔ eq
constant symbol eq_refl {a} (x:τ a) : π (x = x)
constant symbol eq_ind {a} (x y:τ a) :
                       π (x = y) ⇒ ∀p, π (p y) ⇒ π (p x)

theorem ksf : ∀n, π (eq nat n n)
proof
admit

[gabrielhdt]

Perhaps implicits: the first argument of eq is marked as implicits, so it should be

∀n, π (eq {nat} n n)

shouldn't it?

[fblanqui]

Why should we use package-delete?

[gabrielhdt]

If you want to remove the lambdapi emacs mode.

[amelieled]

I have the same problem after "M-x package-delete RET lambdapi-mode-0". And I have no problem when I wrote (except an error about inference...) :

theorem ksf : ∀n, π (eq nat n n)
proof
admit

but after add { }, the %CPU becomes egal to 100 :

theorem ksf : ∀n, π (eq {nat} n n)
proof
admit

[gabrielhdt]

I can reproduce: lambdapi check <last example> loops with the implicit argument added.

[gabrielhdt]

Ah! I found the culprit,

definition N ≔ τ nat
rule τ nat        → N

The definition is like a rewrite rule, so you have a non terminating rewrite system here.

[fblanqui]

How is it possible to add a rule to a definition? This should generate an error! This is a bug.

[gabrielhdt]

I think you can't add rule N -> ... but I am not sure we want to forbid rewriting terms that are themselves definitions.

[fblanqui]

No, this is not a bug. It's perfectly fine to write this, syntactically, except that it does not terminate.

@amelieled , simply write definition N := \tau nat or symbol N:TYPE rule \tau nat -> N, but not both.

[rlepigre]

So what was the problem in the end? Could someone update the title of the issue accordingly?

[amelieled]

The problem is : I defined a rewriting system which not terminate, because the difference between to syntax. Now, I know that definition N := \tau nat is the same that :

symbol N:TYPE 
rule \tau nat -> N

A correct solution is so :

// Property type
constant symbol Prop : TYPE
set declared "π"
injective symbol π : Prop ⇒ TYPE

// Set type
constant symbol Set : TYPE
set declared "τ"
injective symbol τ : Set ⇒ TYPE

// Boolean type
constant symbol bool : Set
constant symbol B : TYPE
rule τ bool       → B
constant symbol true : B
constant symbol false : B

// Nat type
constant symbol nat  : Set
constant symbol N : TYPE
rule τ nat        → N
constant symbol zero : N
constant symbol succ : N ⇒ N
set builtin "0"  ≔ zero
set builtin "+1" ≔ succ

// Leibniz equality
constant symbol eq {a} : τ a ⇒ τ a ⇒ Prop
set infix 1 "=" ≔ eq
constant symbol eq_refl {a} (x:τ a) : π (x = x)
constant symbol eq_ind {a} (x y:τ a) :
                       π (x = y) ⇒ ∀p, π (p y) ⇒ π (p x)

theorem ksf : ∀n, π (eq {nat} n n)
proof
admit

But, I thing it's very useful to check the terminaison before run a process at 100% CPU.

[rlepigre]

But, I thing it's very useful to check the terminaison before run a process at 100% CPU.

Well, we can't really do that because that is not the main goal of Lambdapi. And this is the same problem you could have with any program, written in any programming language: if your program loops it just loops and it is gonna use up your CPU time. In any case, lambdapi is a use process so it should not take over your machine.

[amelieled]

Yes but a warning about that it'll be very beneficial. In my case, I never managed to turn off emacs, even with "kill -9 ..." because another process was created to take over. The only way to stop the problem was to turn off my machine.

[rlepigre]

That is not normal, you should be able to stop the LSP server somehow. Or at least to tell the LSP mode to stop sending updates for a while. Is there such a thing @gabrielhdt?

[rlepigre]

It is actually important to be able to interrupt the LSP mode manually in case there is potential non-termination going on.

[ejgallego]

Yes, adding an "interrupt" command is in the todo list; this should be easy to do; I'm ultra stomped now guys but here is a few tips:

• in the current architecture, the best choice is to bind the VSCode interrupt command so it sends a signal to the lsp server. OCAml should handle this reasonably well, but we need to be careful to handle the exception properly; in particular if lambdapi still exposes some imperative state this will be tricky to get right.
• in the medium term, you want to have two processes, one for the checking, and one for the LSP control, then you can just use the regular protocol, heuristics, etc...
• another choice we are investigating is using OCaml multicore; this again requires a very strict functional style but would be the long-term solution as the 2 process solution introduces too much overhead for this use case.

The ideal way to handle this similar how Isabelle does; checking runs in their own thread, and when the user provides some input / diff on something that's being checked the thread is killed.

So that's fully transparent by the user, and can be tweaking to be lazier [for example when on battery]

[gabrielhdt]

That is not normal, you should be able to stop the LSP server somehow. Or at least to tell the LSP mode to stop sending updates for a while. Is there such a thing @gabrielhdt?

I think kill-ing -9 emacs should do the trick, although it's a bit brutal. I am not aware of any smoother method.

Edit: I think I misunderstood your question, to inhibit the lsp in emacs, there is "M-x eglot-shutdown" but if everything is running at 100%, it might no be easy to input the command...

[rlepigre]

in the current architecture, the best choice is to bind the VSCode interrupt command so it sends a signal to the lsp server.

@ejgallego do you mean that we have to capture SIGINT and only interrupt the currently running task in the LSP server? Is there anything particular to do on the client side for Emacs (for example)?

[ejgallego]

@ejgallego do you mean that we have to capture SIGINT and only interrupt the currently running task in the LSP server?

Indeed, as of today using Sys.catch_break plus catching Break should work fine in Linux / OSX,

You can catch this in the main loop of the LSP server, and just continue the loop in the proper state.

Is there anything particular to do on the client side for Emacs (for example)?

This is not standard for LSP I think, so indeed you need to add a command that sends the sigint to the lsp server; as the protocol is mostly stateless there is nothing else to do [great advantage of stateless protocols!]

[ejgallego]

Once you move to a two-process architecture, indeed the control process would take care of sending the sigint when needed [maybe a timeout, the user edits that sentence, etc...]

There is no notion of explicit cancellation in LSP, but IMHO it is OK for the proof use case to extend the protocol with a cancel checking command once the control server can actually implement it.

[francoisthire]

A naive remark but why using Lwt would not work instead of waiting for OCaml multicore?

[ejgallego]

A naive remark but why using Lwt would not work instead of waiting for OCaml multicore?

Using Lwt is a bit orthogonal here, it provides library help but doesn't solve any of the fundamental problems in implementing an interrupt command. There is not need to wait for OCaml multicore, the two other proposals do work now, in the short, and medium term.