Onboarding with tutorial [Mac]

[htzh]

I tried to follow the tutorial after opam install on a Mac. I have observed the following problems:

1. In vscode LSP server would not start until I created the lib_root directory in my opam switch. The plugin did attempt to mkdir so it is possibly a permission issue.

2. Tutorial refers to tests.OK.logic. I resolved the issue by cloning the project and copying the tests package to the lib_root directory. (Just realized that tutorial.lp is part of tests.OK.)

3. On Mac "Ctrl [Arrows]" don't work and there appear no other ways to interact with proof/goals in vscode. I believe the key combinations are captured by the system. E.g. Ctrl-Right-Arrow and Ctrl-Left-Arrow move between system windows.

I understand these are likely not your priorities so I am just reporting them in case it would help.

[fblanqui]

Thank you very much @htzh for reporting these problems. This is very helpful to improve Lambdapi. Perhaps @firewall2142 could provide some workaround for problem 3. In Emacs, it is possible to redefine shortcuts. I am not sure how to do it in VSCode.
Concerning problem 1, could you please precise the Lambdapi version used?

[htzh]

I installed from opam and the version is 2.2.0.

I experimented a little more in vscode. If I cut away the proofs from the examples in tutorial.lp, I get indications of missing goals, unfinished proofs etc in the editor window. After I paste back the proofs these go away. So the basic interaction seems to be intact. However my goal window says No goals throughout.

[mikemull]

I'm not sure if this is still an issue, but there are two workarounds i've found. First, Macos uses the the Ctrl- keys for "Mission Control", so one option is to go into System Settings/Keyboard, go to the Keyboard Shortcuts and either turn off or remap the various commands.

The second option is to change the keyboard shortcuts within VSCode (⌘K ⌘S gets you to the shortcuts). For example, I switched them to Option-h for ^←, Option-j for ^↓, etc to match the VI navigation keys.

[fblanqui]

Thanks @mikemull . Indeed, concerning 3, one solution is to remap shortcuts to keys that are less commonly used both in Linux and in MacOS. @Alidra something to discuss at Fontainebleau on Thursday or Friday.
Concerning 2, the tutorial was not indicating that a file lambdapi.pkg must be created in the folder where you copy your tutorial.lp file. I fixed this a few weeks ago.
Concerning 1, is it still an issue?

[mikemull]

@fblanqui I did not experience the problem in item (1). The only remaining issue i'm having with the vscode extension is that the editor window loses the focus after each command. I hope to debug that this week to see if it's a general issue or just a problem with my setup.

[Alidra]

Hi @mikemull. There is indeed an issue with the Vscode extension making the Goal panel to loose focus.
I will fix it and open an PR soon. I will let you know asap.

[Alidra]

Regarding 3, What already seems to work by default are the following shortcuts :
Ctrl+fn+Right: go one step forward
Ctrl+fn+Left: go one step backward
Ctrl+Enter: go to the position of the cursor
Ctrl+Alt+c: toggle cursor mode (proof highlight follows the cursor or not)
Ctrl+Alt+w: toggle follow mode (proof highlight is always centered in the window when keybindings are pressed)
Shift+Alt+w: center proof highlight in the current window
What does not to work is
Ctrl+Up: go to the previous proof (or the beginning)
Ctrl+Down: go to the next proof (or the end)
There are roughly three options to deal with that:
1- Change the shortcuts for all users (MacOs, Linux and Windows) This has the advantage of working out of the box without the need for the user to customize anything but I find it a bit disruptive.
2- Manually set the shortcuts as in Linux/Windows and replace the one defined by default in MacOs which has the double disadvantage of requiring extra customization and disturb the navigation experience of many MacOs users.
3- Document the conflict and ask the user to define custom shortcuts for go to the previous/next proof and recommend for instance the combination Ctrl+option+Up/down (could also be Ctrl+fn+Up/Down but these already used for scrolling up/down in MacOs)