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.