Merge remote-tracking branch 'dk/master' into why3

.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 ...

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**
 

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))
+ )
+)

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

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

editors/vscode/CHANGES.md

@@ -3,6 +3,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
+
+### 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]
 - 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.

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.

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"
         }
       }
     },
@@ -138,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": [
@@ -170,4 +187,4 @@
     "fs-extra": "^9.0.1",
     "vscode-languageclient": "^9.0.1"
   }
-}
+}

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",

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);
         });
 

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). *)

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

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