Code is removed on save!!!

[lukaszcz]

If you type in

module Bug;
end;

save, then change it to

module Bug;

f : Nat -> Nat;
f x := x;

end;

and save, then the module body disappears with no error message and you get

module Bug;
end;

back again.

[lukaszcz]

Well, it actually happens even with well-typed code. Adding open import Stdlib.Prelude doesn't help. You need to manually click on the "typecheck" button first.

[lukaszcz]

And then your code gets automatically reformatted! This alone should be considered a bug - not everyone wants their code reformatted on every save.

[lukaszcz]

The VSCode extension is practically unusable. Now it sometimes randomly replaces the newly written code with the old version!

[jonaprieto]

Do you have the option "Format on save?"

[jonaprieto]

I suspect this issue has to be with the Juvix formatting. Did you experience this issue before 0.1.22?

[lukaszcz]

No. I use default options, didn't change anything, only updated the extension.

On Fri, Jan 27, 2023 at 7:04 PM Jonathan Cubides @.***> wrote:

I suspect this issue has to be with the Juvix formatting. Did you experience this issue before 0.1.22?

— Reply to this email directly, view it on GitHub https://github.com/anoma/vscode-juvix/issues/34#issuecomment-1406896515, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAAPKH4MXNSAVZ2DZLA5PKDWUQE3XANCNFSM6AAAAAAUI6TJ64 . You are receiving this because you authored the thread.Message ID: @.***>

[lukaszcz]

Maybe I have global "format on save". I'll check that.

On Fri, Jan 27, 2023 at 7:05 PM Lukasz Czajka @.***> wrote:

No. I use default options, didn't change anything, only updated the extension.

On Fri, Jan 27, 2023 at 7:04 PM Jonathan Cubides @.***> wrote:

I suspect this issue has to be with the Juvix formatting. Did you experience this issue before 0.1.22?

— Reply to this email directly, view it on GitHub https://github.com/anoma/vscode-juvix/issues/34#issuecomment-1406896515, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAAPKH4MXNSAVZ2DZLA5PKDWUQE3XANCNFSM6AAAAAAUI6TJ64 . You are receiving this because you authored the thread.Message ID: @.***>

[jonaprieto]

Let me see if I can experience the same in the Github codespaces, because I can't locally.

[jonaprieto]

I couldn't reproduce the behavior you described. :(

[lukaszcz]

I have "format on save" turned on. You can't change it locally, it seems, and I don't want to turn it off globally. The Juvix formatter doesn't work the way it should, removing text it cannot parse. The easiest fix is to just print out the input if there is a parse error.

[lukaszcz]

And it's not only incorrect code. Sometimes perfectly valid code gets removed by the formatter. See my second comment above.

[jonaprieto]

It was fixed in v0.1.24. Reopen if you experience the same behaviour.