fix issue#638 : show log message when symbol is defined

[Alidra]

As described in issue#638, log messages are sometimes not shown at the right moment when a symbol is defined and proofs are navigated. This PR fixes this issue.

TODO:

• [x] make sure that make sanity_check passes

[fblanqui]

Hi Abdelghani. From your PR, I understand that the function pdata_finalize should not print anything because it interferes with interfaces. It would be interesting to understand why. But it means that it should not emit warnings too. And indeed, if we add at the end of the file

symbol l:A ≔
begin
abort;

we get 2 new problems in Emacs (I didn't test VSCode):

1. The abort warning is printed first, before the other messages, while it should be written only when we reach the proof.

2. The green zone disappears and I have an error: eglot--lsp-position-to-point: Symbol’s function definition is void: eglot-move-to-column. Can be fixed by merging https://github.com/Deducteam/lambdapi/pull/977?

[fblanqui]

The problems mentioned are solved by #977.

[fblanqui]

Hi. The last commit is better but there is still something wrong. Warnings and messages should not be printed when the pdata_finalize function is created but at the very end of the command.ml file after the evaluation of pdata_finalize itself. One solution is to extend the proof_data record type with a new field pdata_print: unit -> unit, corresponding to your print_fct, and executed at the end of command.ml after pdata_finalize.

[Alidra]

Thanks Frédéric, It seems to me that messages now are printed at the right place. The same should be done to warnings. Actually, Warnings and messages were printed when the pdata_finalize function is evaluated which was giving the issue we are trying to solve. Am I wrong? I will push new code, please check again and tell me.

[fblanqui]

You should merge origin/master and fix make sanity_check first.

[fblanqui]

The messages are not written in the right order yet. Take for instance:

symbol A:TYPE;
symbol l:A ≔
begin
assume x; // fails
abort; // warning

The error should appear before the warning. As explained in my previous message: One solution is to extend the proof_data record type with a new field pdata_print: unit -> unit, corresponding to your print_fct, and executed at the end of command.ml after pdata_finalize.

[fblanqui]

After discussion offline, changes to do in lp_doc.ml:

    let st, dg_proof, logs =
      match end_proof pst with
      | Cmd_OK (st, qres)   ->
        let qres = match qres with None -> "OK" | Some x -> x in
        let pg = qed_loc, 4, qres, None in
(* line to add: *)
let logs = ((3, buf_get_and_clear lp_logger), cmd_loc) :: logs in
        st, pg :: dg_proof, logs

[Alidra]

Hi Frédéric, The issue described in 638 seems fixed. It worth mentioning though that navigating the proofs before the proof is completed (ended, aborted or admitted) prevents any logs from being displayed. This behavior is prior to the current fix. Does this seem fine to you?

[fblanqui]

Could you please provide an example?

[Alidra]

Here is an example :

verbose 3;
symbol T : TYPE;
symbol trivial : T → T → T → T
≔ begin
  assume _ _ x;
  refine x;

In this case, navigating the proofs doesn't show any log. putting end at the end of the proof show the logs again. Note also that logs are shown when the check is run in the command line :

lambdapi check tests/OK/anonymous2.lp 
Checking "/home/abdelghani/Repos/forksLambdapi/lambdapi/tests/OK/anonymous2.lp" ...
verbose 3
/home/abdelghani/Repos/forksLambdapi/lambdapi/tests/OK/anonymous2.lp:2:0-16
symbol T : TYPE
[/home/abdelghani/Repos/forksLambdapi/lambdapi/tests/OK/anonymous2.lp:8:0] Unexpected token: "".

[fblanqui]

This is because there is no terminator to your begin. Or did you forget it in your example? If you had abort, it works fine. But an error should be omitted if there is no terminator, like on command line:

11:40 ~/src/lambdapi (fix/logMessages) lambdapi check tmp/638b.lp 
Checking "/home/blanqui/src/lambdapi/tmp/638b.lp" ...
verbose 3
/home/blanqui/src/lambdapi/tmp/638b.lp:2:0-16
symbol T : TYPE
[/home/blanqui/src/lambdapi/tmp/638b.lp:7:0] Unexpected token: "".

But even on command line, the error message is incorrect. It should complain that there is no end/admitted/abort. Please create a new issue for this.

[fblanqui]

make sanity_check fails:

11:41 ~/src/lambdapi (fix/logMessages) make sanity_check
In src/handle/command.ml, line 498 more than 78 characters...
In src/handle/command.ml, line 524 more than 78 characters...
In src/handle/command.ml, line 538 more than 78 characters...
In src/handle/command.ml, line 540 has trailing spaces...

[Alidra]

This is because there is no terminator to your begin. Or did you forget it in your example? If you had abort, it works fine. Yes. But running Lambdapi in command line with the same file shows the log messages. Shouldn't it be the same with LSP.

But an error should be omitted if there is no terminator, like on command line:

11:40 ~/src/lambdapi (fix/logMessages) lambdapi check tmp/638b.lp 
Checking "/home/blanqui/src/lambdapi/tmp/638b.lp" ...
verbose 3
/home/blanqui/src/lambdapi/tmp/638b.lp:2:0-16
symbol T : TYPE
[/home/blanqui/src/lambdapi/tmp/638b.lp:7:0] Unexpected token: "".

But even on command line, the error message is incorrect. It should complain that there is no end/admitted/abort. Please create a new issue for this. Ok.

[Alidra]

make sanity_check fails:

11:41 ~/src/lambdapi (fix/logMessages) make sanity_check
In src/handle/command.ml, line 498 more than 78 characters...
In src/handle/command.ml, line 524 more than 78 characters...
In src/handle/command.ml, line 538 more than 78 characters...
In src/handle/command.ml, line 540 has trailing spaces...

I dont see these errors in my side (for instance line 498 in command.ml is 59 characters long only)

[fblanqui]

My branch was not update. Sorry.