From ad4666da5b44ffaddd8e43c93f3cf7b40bc483c7 Mon Sep 17 00:00:00 2001
From: Alidra <40537601+Alidra@users.noreply.github.com>
Date: Thu, 19 Dec 2024 10:49:09 +0100
Subject: [PATCH 1/5] Change the way lsp server is launched from Vscode
 extension (#1164)

As described in issue #1163 , one may want to launch the `Lambdapi Lsp server` from the `Vscode` extension  using a custom command. This is especially useful when installing the `Lambdapi extension` on `Windows` where `Lambdapi` is launched through `wsl`. This is done in this PR by allowing to read the arguments of the launch command as well as the command it self, from the `package.json` file instead of wiring it in the code.
---
 editors/vscode/CHANGES.md     |  9 +++++++++
 editors/vscode/package.json   | 11 +++++++++--
 editors/vscode/src/browser.ts |  6 +++---
 editors/vscode/src/client.ts  | 11 +++++++----
 4 files changed, 28 insertions(+), 9 deletions(-)

diff --git a/editors/vscode/CHANGES.md b/editors/vscode/CHANGES.md
index bb8d98305..a3afb4099 100644
--- a/editors/vscode/CHANGES.md
+++ b/editors/vscode/CHANGES.md
@@ -3,6 +3,15 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/),
 and this project adheres to [Semantic Versioning](https://semver.org/).
 
+## Unreleased
+
+### Added
+
+### Fixed
+
+### Changed
+- When calling lambdapi to launch the lsp server from the Vscode extension, read the `lsp` argument from `package.json` instead of hard-coding it to allow using a custom command to launch the server especially in Windows as discussed in issue #1163 (Many thanks to Akihisa Yamada)
+
 ## [0.2.2]
 - code refactoring of the client for maintenability.
 - fix the bug that causes the proof navigation to malfunction when the `Goals` panel is closed by the user. Now the panel is recreated whenever needed. If focus is taken away frol the `Goals` panel, focus is given back to it when user starts navigating proofs again.
diff --git a/editors/vscode/package.json b/editors/vscode/package.json
index fb7e5e3e9..292f324cf 100644
--- a/editors/vscode/package.json
+++ b/editors/vscode/package.json
@@ -58,7 +58,14 @@
         "lambdapi.path": {
           "type": "string",
           "default": "lambdapi",
-          "description": "Path to lambdapi binary"
+          "description": "Command to launch lambdapi"
+        },
+        "lambdapi.args": {
+          "type": "list",
+          "default": [
+            "lsp"
+          ],
+          "description": "Arguments to start the Lsp server"
         }
       }
     },
@@ -170,4 +177,4 @@
     "fs-extra": "^9.0.1",
     "vscode-languageclient": "^9.0.1"
   }
-}
+}
\ No newline at end of file
diff --git a/editors/vscode/src/browser.ts b/editors/vscode/src/browser.ts
index 30b764b7b..ee91497e0 100644
--- a/editors/vscode/src/browser.ts
+++ b/editors/vscode/src/browser.ts
@@ -3,10 +3,10 @@ import { LanguageClient } from "vscode-languageclient/node";
 import { activateClientLSP, ClientFactoryType, deactivateClientLSP } from "./client";
 
 export function activate(context: ExtensionContext): void {
-  const cf: ClientFactoryType = (context, clientOptions, wsConfig, lspServerPath) => {
+  const cf: ClientFactoryType = (context, clientOptions, wsConfig, lpLaunchCommand, lspLaunchArgs) => {
     let serverOptions = {
-      command: lspServerPath,
-      args: ['lsp']
+      command: lpLaunchCommand,
+      args: lspLaunchArgs
     };
     return new LanguageClient(
       "lambdapi",
diff --git a/editors/vscode/src/client.ts b/editors/vscode/src/client.ts
index ccf3951c3..e515a9b99 100644
--- a/editors/vscode/src/client.ts
+++ b/editors/vscode/src/client.ts
@@ -62,7 +62,8 @@ export type ClientFactoryType = (
     context: ExtensionContext,
     clientOptions: LanguageClientOptions,
     wsConfig: WorkspaceConfiguration,
-    lspServerPath: any,
+    lpLaunchCommand: any,
+    lspServerArgs: any,
 ) => BaseLanguageClient;
 
 // The implementation of the VSCode lambdapi extension commands.
@@ -354,8 +355,10 @@ export function activateClientLSP(context: ExtensionContext,
     //Following mode : whether the window follows proofState automatically or not
     context.workspaceState.update('follow', true);
 
-    const lspServerPath = workspace.getConfiguration('lambdapi').path;
-    console.log(lspServerPath);
+    const lpLaunchCommand = workspace.getConfiguration('lambdapi').path;
+    const lspLaunchArgs = workspace.getConfiguration('lambdapi').args;
+    console.log(lpLaunchCommand);
+    console.log(lspLaunchArgs);
 
     const wsConfig = workspace.getConfiguration("lambdapi");
 
@@ -380,7 +383,7 @@ export function activateClientLSP(context: ExtensionContext,
 
         let cP = new Promise<BaseLanguageClient>((resolve) => {
             // Create a client using the factory
-            client = clientFactory(context, clientOptions, wsConfig, lspServerPath);
+            client = clientFactory(context, clientOptions, wsConfig, lpLaunchCommand, lspLaunchArgs);
             resolve(client);
         });
 

From 50f02fc636f69a5c797e9ea2fcd9e6473c6cf073 Mon Sep 17 00:00:00 2001
From: Alidra <40537601+Alidra@users.noreply.github.com>
Date: Thu, 19 Dec 2024 11:57:32 +0100
Subject: [PATCH 2/5] Document Macos shortcuts (#1161)

This PR Modifies the README.md of the Vscode extension to document the shortcuts of Lambdapi extension in Mac OS X as discussed in #869
---
 doc/vscode.rst              | 32 +++++++++++++++++++++-----------
 editors/vscode/CHANGES.md   |  1 +
 editors/vscode/README.md    | 13 +++++++++++++
 editors/vscode/package.json | 14 ++++++++++++--
 4 files changed, 47 insertions(+), 13 deletions(-)

diff --git a/doc/vscode.rst b/doc/vscode.rst
index f67936484..bcc958b94 100644
--- a/doc/vscode.rst
+++ b/doc/vscode.rst
@@ -23,17 +23,27 @@ Make sure you have a `lambdapi.pkg <https://lambdapi.readthedocs.io/en/latest/mo
 
 Goals are visualised in a panel on the right side of the editor. You can
 navigate in proof with the following key-bindings:
-
--  ``Ctrl+Right``: go one step forward
--  ``Ctrl+Left``: go one step backward
--  ``Ctrl+Up``: go to the previous proof (or the beginning)
--  ``Ctrl+Down``: go to the next proof (or the end)
--  ``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
+***Linux and Windows***
+- ``Ctrl+Right``: go one step forward
+- ``Ctrl+Left``: go one step backward
+- ``Ctrl+Up``: go to the previous proof (or the beginning)
+- ``Ctrl+Down``: go to the next proof (or the end)
+- ``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 highligsht is always centered in the window when keybindings are pressed)
+- ``Shift+Alt+w``: center proof highlight in the current window
+
+***Mac OS X***
+- ``Ctrl+fn+Right``: go one step forward
+- ``Ctrl+fn+Left``: go one step backward
+- ``Ctrl+Alt+Up``: go to the previous proof (or the beginning)
+- ``Ctrl+Alt+Down``: go to the next proof (or the end)
+- ``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
+
+Please note that these key-bindings can be changed in Code->Preferences->keyboard shortcuts (also reachable with Ctrl+K Ctrl+S or Command+K Command+S in Mac OS X).
 
 **Hover and go-to-definition**
 
diff --git a/editors/vscode/CHANGES.md b/editors/vscode/CHANGES.md
index a3afb4099..16c084b31 100644
--- a/editors/vscode/CHANGES.md
+++ b/editors/vscode/CHANGES.md
@@ -10,6 +10,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 ### Fixed
 
 ### Changed
+- Changed the `go to the previous/next proof` commands shortcuts for Mac OS X operating system because previous ones are used by Mac OS.
 - When calling lambdapi to launch the lsp server from the Vscode extension, read the `lsp` argument from `package.json` instead of hard-coding it to allow using a custom command to launch the server especially in Windows as discussed in issue #1163 (Many thanks to Akihisa Yamada)
 
 ## [0.2.2]
diff --git a/editors/vscode/README.md b/editors/vscode/README.md
index 61694845a..429f45127 100644
--- a/editors/vscode/README.md
+++ b/editors/vscode/README.md
@@ -5,15 +5,28 @@ This extension provides support for the [Lambdapi](https://github.com/Deducteam/
 Goals are visualised in a panel on the right side of the editor.
 You can navigate in proof with the following key-bindings:
 
+***Linux and Windows***
 - ``Ctrl+Right``: go one step forward
 - ``Ctrl+Left``: go one step backward
 - ``Ctrl+Up``: go to the previous proof (or the beginning)
 - ``Ctrl+Down``: go to the next proof (or the end)
 - ``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 highligsht is always centered in the window when keybindings are pressed)
+- ``Shift+Alt+w``: center proof highlight in the current window
+
+***Mac OS X***
+- ``Ctrl+fn+Right``: go one step forward
+- ``Ctrl+fn+Left``: go one step backward
+- ``Ctrl+Alt+Up``: go to the previous proof (or the beginning)
+- ``Ctrl+Alt+Down``: go to the next proof (or the end)
+- ``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
 
+Please note that these key-bindings can be changed in Code->Preferences->keyboard shortcuts (also reachable with Ctrl+K Ctrl+S or Command+K Command+S in Mac OS X).
+
 **Hover and go-to-definition**
 
 Hovering a token will display its type if available.
diff --git a/editors/vscode/package.json b/editors/vscode/package.json
index 292f324cf..a8f43f16a 100644
--- a/editors/vscode/package.json
+++ b/editors/vscode/package.json
@@ -145,12 +145,22 @@
       {
         "key": "ctrl+up",
         "command": "extension.lambdapi.pv",
-        "when": "editorTextFocus && editorLangId == lp"
+        "when": "editorTextFocus && editorLangId == lp && (isWindows || isLinux)"
       },
       {
         "key": "ctrl+down",
         "command": "extension.lambdapi.nx",
-        "when": "editorTextFocus && editorLangId == lp"
+        "when": "editorTextFocus && editorLangId == lp && (isWindows || isLinux)"
+      },
+      {
+        "key": "ctrl+alt+up",
+        "command": "extension.lambdapi.pv",
+        "when": "editorTextFocus && editorLangId == lp && isMac"
+      },
+      {
+        "key": "ctrl+alt+down",
+        "command": "extension.lambdapi.nx",
+        "when": "editorTextFocus && editorLangId == lp && isMac"
       }
     ],
     "snippets": [

From 15d4eeaeefd33f44a8e6258dc905dacdb731cacc Mon Sep 17 00:00:00 2001
From: Alidra <40537601+Alidra@users.noreply.github.com>
Date: Thu, 2 Jan 2025 10:59:17 +0100
Subject: [PATCH 3/5] Minor Fixes in the Emacs extension (#1168)

This PR fixes some minor issues in the `Emacs` extension (package). Specifically :
- The `Goals` panel is recentred to show the first goal in case of many assumptions and avoid having to scroll down.
- When proofs are navigated, if the last command is reached, the navigation continues to the end of file to display the last error messages if any (in particular the issue described in  #1111 where the `end;` token is missing)
- Check that the Goals and Logs buffers are displayed before displaying logs and goals when proofs are navigated

* recentre the goals in case of many assumptions
* emacs : If no next command go to the last line to display the last error message if any
* emacs : fix autoscroll in the presence of many hypothesis
* emacs: bring Goals and Logs buffers before displaying logs and goals
Plus, add CHANGES.md file
---
 editors/emacs/CHANGES.md         | 16 ++++++++++++++++
 editors/emacs/lambdapi-proofs.el | 17 ++++++++++++++---
 2 files changed, 30 insertions(+), 3 deletions(-)
 create mode 100644 editors/emacs/CHANGES.md

diff --git a/editors/emacs/CHANGES.md b/editors/emacs/CHANGES.md
new file mode 100644
index 000000000..d70553640
--- /dev/null
+++ b/editors/emacs/CHANGES.md
@@ -0,0 +1,16 @@
+All notable changes to this project will be documented in this file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/),
+and this project adheres to [Semantic Versioning](https://semver.org/).
+
+## Unreleased
+
+### Added
+- Auto scroll to the first goal in the `Goals` buffer in case of many hypothesis
+- Check that the Goals and Logs buffers are displayed before displaying logs and goals 
+
+### Fixed
+- Show the error at the end of file if any. That was not working because navigation stoped at the location of last command and not further (see issue #1111)
+
+
+### Changed
diff --git a/editors/emacs/lambdapi-proofs.el b/editors/emacs/lambdapi-proofs.el
index 0d9f7226a..944c6d59b 100644
--- a/editors/emacs/lambdapi-proofs.el
+++ b/editors/emacs/lambdapi-proofs.el
@@ -129,10 +129,20 @@ This works for both graphical and text displays."
             (erase-buffer)
             (goto-char (point-max))
             (mapc 'insert hypsstr)
+            (setq saved-point (point))
             (mapc (lambda (gstr)
                     (lp--draw-horizontal-line)
                     (insert gstr))
-                  goalsstr))
+                  goalsstr)
+                  
+            (let ((goalswin (get-buffer-window goalsbuf)))
+              (if goalswin
+                  (with-selected-window goalswin
+                    (goto-char (+ 1 saved-point))
+                    (beginning-of-line)
+                    (recenter -1))))
+
+                  )
         (remove-overlays)
         (erase-buffer)
         (insert "No goals"))
@@ -174,6 +184,7 @@ This works for both graphical and text displays."
         (let ((response (jsonrpc-request server :proof/goals params)))
           (if response
               (progn
+                (lambdapi-refresh-window-layout)
                 (lp-display-goals (plist-get response :goals))
                 (lp-display-logs (plist-get response :logs)))
             (let ((goalsbuf (get-buffer-create "*Goals*"))
@@ -330,7 +341,7 @@ and 0 if there is no previous command."
 
 (defun lp--next-command-pos (&optional pos)
   "Return the position of the next command's terminator
-and POS if there is no next command"
+and (point-max) if there is no next command to display the last error in logs"
   (setq npos (1+ (or pos (point))))
   (save-excursion
     (let ((term-regex
@@ -343,7 +354,7 @@ and POS if there is no next command"
             (setq npos (re-search-forward term-regex nil t))
             (and npos (lp--in-comment-p npos)))
         (goto-char npos))
-      (if npos (max (point-min) (1- npos)) pos))))
+      (if npos (max (point-min) (1- npos)) (point-max)))))
 
 (defun lp--post-self-insert-function ()
   (save-excursion

From 2e32554f7d97616265a3f5d1f3e175f9513dd6c0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?=
 <fblanqui@users.noreply.github.com>
Date: Thu, 2 Jan 2025 15:51:06 +0100
Subject: [PATCH 4/5] LSP server: decode percent-encoded URIs before using them
 as filenames (fix #1169) (#1172)

- fix #1169
-  lsp/lp_doc.ml: decode percent-encoded URIs before using them as filenames
- dune-project: add dependency to uri
- cli/config.ml and common/library.ml: rename log_lib into log
---
 dune-project          |  5 ++++-
 src/cli/config.ml     |  6 +++---
 src/common/library.ml | 13 ++++++-------
 src/lsp/lp_doc.ml     |  1 +
 4 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/dune-project b/dune-project
index 8f51cba77..60a2b88aa 100644
--- a/dune-project
+++ b/dune-project
@@ -41,4 +41,7 @@ systems: Dedukti, Coq, HRS, CPF.")
   (cmdliner (>= 1.1.0))
   (stdlib-shims (>= 0.1.0))
   (lwt_ppx (>= 1.0.0))
-  (dream (>= 1.0.0~alpha3))))
+  (dream (>= 1.0.0~alpha3))
+  (uri (>= 1.1))
+ )
+)
diff --git a/src/cli/config.ml b/src/cli/config.ml
index f1c60bee5..55278eec2 100644
--- a/src/cli/config.ml
+++ b/src/cli/config.ml
@@ -61,10 +61,10 @@ let init : config -> unit = fun cfg ->
   (* Log some configuration data. *)
   if Logger.log_enabled () then
     begin
-      Library.log_lib "running directory: %s" (Filename.current_dir ());
-      Library.log_lib "library root path: %s"
+      Library.log "running directory: %s" (Filename.current_dir ());
+      Library.log "library root path: %s"
         (match !lib_root with None -> assert false | Some(p) -> p);
-      let f = Library.log_lib "mapping: %a → %s" Path.pp in
+      let f = Library.log "mapping: %a → %s" Path.pp in
       Library.iter f
     end;
   (* Initialise the [Pure] interface (this must come last). *)
diff --git a/src/common/library.ml b/src/common/library.ml
index cbc7182af..b879070bb 100644
--- a/src/common/library.ml
+++ b/src/common/library.ml
@@ -4,8 +4,8 @@ open Lplib open Base open Extra
 open Timed
 open Error open Debug
 
-let log_lib = Logger.make 'l' "libr" "library files"
-let log_lib = log_lib.pp
+let log = Logger.make 'l' "libr" "library files"
+let log = log.pp
 
 (** Representation of the mapping from module paths to files. *)
 module LibMap :
@@ -81,7 +81,7 @@ module LibMap :
         List.fold_left Filename.concat root ks in
       let rec get (root, old_ks) ks map =
         if Logger.log_enabled () then
-          log_lib "get @[<hv>\"%s\"@ [%a]@ [%a]@ %a@]" root
+          log "get @[<hv>\"%s\"@ [%a]@ [%a]@ %a@]" root
             (D.list D.string) old_ks (D.list D.string) ks (D.strmap pp) map;
         match ks with
         | []      -> concat root old_ks
@@ -137,8 +137,7 @@ let set_lib_root : string option -> unit = fun dir ->
   match !lib_root with
   | None -> assert false (* pth is set above. *)
   | Some(pth) ->
-    (* Register the library root as part of the module mapping.
-         Required by [module_to_file]. *)
+    (* Register the library root as part of the module mapping. *)
     Timed.(lib_mappings := LibMap.set_root pth !lib_mappings)
 
 (** [add_mapping (mn, fn)] adds a new mapping from the module name [mn] to
@@ -165,7 +164,7 @@ let file_of_path : Path.t -> string = fun mp ->
   try
     let fp = LibMap.get mp !lib_mappings in
     if Logger.log_enabled () then
-      log_lib "file_of_path @[<hv>%a@ %a@ = \"%s\"@]"
+      log "file_of_path @[<hv>%a@ %a@ = \"%s\"@]"
         Path.pp mp LibMap.pp !lib_mappings fp;
     fp
   with LibMap.Root_not_set -> fatal_no_pos "Library root not set."
@@ -232,7 +231,7 @@ let path_of_file : (string -> string) -> string -> Path.t =
     String.sub base (len_fp + 1) (len_base - len_fp - 1)
   in
   let full_mp = mp @ List.map escape (String.split_on_char '/' rest) in
-  log_lib "path_of_file @[<hv>\"%s\"@ = %a@]" fname Path.pp full_mp;
+  log "path_of_file @[<hv>\"%s\"@ = %a@]" fname Path.pp full_mp;
   full_mp
 
 (** [install_path fname] prefixes the filename [fname] by the path to the
diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml
index df92ce330..2eecef981 100644
--- a/src/lsp/lp_doc.ml
+++ b/src/lsp/lp_doc.ml
@@ -126,6 +126,7 @@ let process_cmd _file (nodes,st,dg,logs) ast =
 let new_doc ~uri ~version ~text =
   let root, logs =
     try
+      let uri = Uri.pct_decode uri in
       (* We remove the ["file://"] prefix. *)
       assert(String.is_prefix "file://" uri);
       let path = String.sub uri 7 (String.length uri - 7) in

From 4c281ca6bb71a249a62aa4b69a64ad8d1021b292 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?=
 <fblanqui@users.noreply.github.com>
Date: Thu, 2 Jan 2025 15:51:24 +0100
Subject: [PATCH 5/5] ci: test ocaml 5.2.1 instead of ocaml 5.2.0 (#1173)

---
 .github/workflows/main.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index d5d2e1a01..7b7d3a929 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -8,7 +8,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        ocaml-version: [5.2.0, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1]
+        ocaml-version: [5.2.1, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1]
     runs-on: ubuntu-latest
     steps:
       - name: checking out lambdapi repo ...