search

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Other
265 stars 35 forks source link

Fix location of symbol in logs when the object is not found within a tactic #1078

Closed Alidra closed 2 months ago

Alidra commented 2 months ago

Inside a proof, when the user uses a symbol in a tactic that Lambdapi cannot find, Lambdapi show the Object not found. message. this message should be preceded by the location where the symbol has been used. While this is the case in command line, Lambdapi, Lsp fail in showing the location message which results in a misleading information.

This behavior has been described in issue https://github.com/Deducteam/lambdapi/issues/1073

This PR fixes this by displaying the position message as soon as the corresponding exception is caught.

fblanqui commented 2 months ago

Sorry but I don't think that this is the right solution yet. The problem is in the handling of the error. Pure.handle_tactic turns a Fatal error into a Tac_Error with the same data. Lpdoc.process_pstep turns a Tac_Error into a log. Why is the log incorrect or not printed?

Alidra commented 2 months ago

The log is actually printed. However, the log contains the message in the Fatal exception and not its location. That is why the message Unknown object is displayed but not the right location message.

So, we need to add the location to the logs explicitly because in lp_doc line 66, loc is used only to filter the message to be displayed in the console.

fblanqui commented 2 months ago

Thanks Abdelghani!