Displaying subgoals on VS Code

[thomastraversie]

On VS Code, when writing a proof, subgoals are correctly displayed on the Goals window. But once the proof is written, the subgoals do not appear anymore if we move the green cursor. For instance, with

constant symbol Prop : TYPE;
injective symbol Prf : Prop → TYPE;

constant symbol ∧ : Prop → Prop → Prop; notation ∧ infix right 30;
symbol and_i : Π p : Prop, Prf p → Π q : Prop, Prf q → Prf (p ∧ q);

opaque symbol prop_ad : Π A : Prop, Prf A → Π B : Prop, Prf B → Prf (A ∧ B) ≔ 
begin
    assume A pA B pB;
    refine and_i A _ B _ 
    {}
    {}
end;

the 2 subgoals are correctly displayed when the cursor is at the end of the line refine and_i A _ B _. Once we have the complete proof:

opaque symbol prop_ad : Π A : Prop, Prf A → Π B : Prop, Prf B → Prf (A ∧ B) ≔ 
begin
    assume A pA B pB;
    refine and_i A _ B _ 
    {refine pA} 
    {refine pB}
end;

if we move the cursor one step further the line assume A pA B pB;, the cursor goes at the first bracket (instead of being at the end of the line refine and_i A _ B _) and only the second subgoal is displayed.

[Alidra]

Hi @thomastraversie ,
With @fblanqui, we tried to reproduce the issue with the code you provided above but we couldn't.
The subgoals seem to be displayed correctly. Would you please check again and update the code if needed?

[thomastraversie]

Hi @Alidra, I can reproduce the issue (on version 2.5.0 of Lambdapi and v0.2.1 of the VSCode extension).
When the green cursor is at the end of line assume A pA B pB; the goal is correctly Prf (A ∧ B). At the next step the cursor is at the first bracket of line {refine pA} and the goal is Prf B, so the step where we have the two goals Prf A and Prf B is missing.

[Alidra]

Hi @thomas,
On my side, I just upgraded lambda to version 2.5.0 and tried again. It seems to work (see attached screenshot)

Can you attach a screenshot with the problem please.

[thomastraversie]

Hi @Alidra, I get these two successive steps:


I can't reproduce your screenshot.

[fblanqui]

I can reproduce Thomas problem with:

constant symbol Prop:TYPE;
injective symbol Prf:Prop → TYPE;
constant symbol ∧ : Prop → Prop → Prop;
notation ∧ infix right 30;
symbol and_i p: Prf p → Π q, Prf q → Prf(p ∧ q);
opaque symbol prop_ad : Π A : Prop, Prf A → Π B : Prop, Prf B → Prf (A ∧ B) ≔ 
begin
    assume A pA B pB;
    refine and_i A _ B _ 
    {refine pA} 
    {refine pB}
end;

by doing:

• open file
• click on the first line
• do Ctrl-Right-Arrow until the green zone reaches the first curly bracket
  then the second goal (B) is printed instead of the first goal (A).

[Alidra]

Thanks Thomas,
Thanks Frédéric,
Actually the problem seems to be due to cursor position calculation. Depending on how one navigates the proof (ctrl+enter or ctrl+right arrow) the position is calculated differently and gives inconsistent goals and console messages.