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

.github/workflows/main.yml

@@ -8,7 +8,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        ocaml-version: [5.1.1, 5.0.0, 4.14.1, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1]
+        ocaml-version: [5.2.0, 5.1.1, 5.0.0, 4.14.1, 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 ...
@@ -48,12 +48,12 @@ jobs:
       - name: generate-vscode-extension
         run: |
           npm install -g @types/vscode
-          npm install -g vsce 
+          npm install -g @vscode/vsce 
           make build-vscode-extension
           make publish-vscode-extension
         env:
-          PAT: ${{secrets.VSCODE_PAT}}
-      - name: publish vscode extension
+          PAT: ${{ secrets.VSCODE_PAT }}
+      - name: upload vscode extension
         uses: actions/upload-artifact@v4
         with: 
           name: assets-for-download

CHANGES.md

@@ -7,18 +7,18 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ### Added
 
-- Add tactic `set`
-- Add export format `raw_dk`
-
-### Changed
-
-- Several bug fixes
+- Add tactic `set`.
+- Add export format `raw_dk`.
+- Fix of the color of the text in command line when console.out is used.
+- Use black text instead of red when diplaying query answers.
+- Allow negative numbers in notation priorities.
+- New release 0.2.2 of the VSCode plugin.
 
 ## 2.5.0 (2024-02-25)
 
 ### Added
 
-- Add the `opaque` command to turn a defined symbol into a constant
+- Add the `opaque` command to turn a defined symbol into a constant.
 - Add the tactic `try` that tries to apply a tactic to the focused goal.
   If the application of the tactic fails, it catches the error and leaves the goal unchanged.
 

Makefile

@@ -22,6 +22,11 @@ doc: bnf
 bnf:
 	$(MAKE) -C doc -f Makefile.bnf
 
+.PHONY: test_libs
+test_libs: lambdapi
+	@dune exec --only-packages lambdapi -- tests/test_lib.sh https://github.com/Deducteam/lambdapi-logics.git
+	@dune exec --only-packages lambdapi -- tests/test_lib.sh https://github.com/Deducteam/lambdapi-stdlib.git
+
 #### Unit tests and sanity check #############################################
 
 .PHONY: tests
@@ -32,6 +37,7 @@ tests: lambdapi
 	@dune exec --only-packages lambdapi -- tests/export_dk.sh
 	@dune exec --only-packages lambdapi -- tests/export_lp.sh
 	@dune exec --only-packages lambdapi -- tests/export_raw_dk.sh
+	$(MAKE) test_libs
 
 .PHONY: tests_alt_ergo
 tests_alt_ergo: lambdapi
@@ -176,12 +182,27 @@ JQ = $(shell which jq)
 ifneq ($(VSCE),)
 ifneq ($(JQ),)
 EXT = $(shell vsce show --json deducteam.lambdapi 2>/dev/null | jq '.versions[0]' | jq '.version')
+
 .PHONY: publish-vscode-extension
 publish-vscode-extension:
 ifeq ($(EXT), $(shell cat editors/vscode/package.json | jq '.version'))
 	echo "extension already exists. Skip"
 else
+ifeq ($(PAT),)
+	# Note, when pushing code from a fork of the Lambdapi repository, PAT secret is not "reachable". 
+	# The extension is only published when merge occurs.
+	echo "The \"PAT\" secret is not set. Please check a PAT exists with permissions to publish to Vscode market"
+else
+ifeq ("$(GITHUB_REF_NAME)", "master")
+	# The extension is only published when code is pushed to master to avoid publishing from feature branches
 	cd editors/vscode && vsce publish -p ${PAT}
+else
+	echo "Env Variable \"GITHUB_REF_NAME\" is set to \"$(GITHUB_REF_NAME)\"."
+	echo "Extension will only be published when pushing to master."
+	echo "If used manualy, please set Variable \"GITHUB_REF_NAME\" to \"master\" to force publishing the extension"
+endif
 endif
 endif
+
 endif
+endif

editors/vscode/CHANGES.md

@@ -3,9 +3,12 @@ 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]
+## [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.
+- 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.
+- fix bug related to navigating sub-goals : navigating next subgoal stops before `{` instead of after it so that next subgoal is correctly shown in the `Goals` panel.
+- change navigation with ``navigate until cursor`` : Navigation includes the command if the cursor is whithin its range instead of the line above. 
+- first command is no more systematically navigated. If the current command is the first one, navigating the previous command results in no command being navigated.
 
 ## [0.1.2] - 2020-12-10
 - use vscode configuration for lambdapi.path to call the lambdapi LSP server

editors/vscode/RELEASE.md

@@ -4,10 +4,10 @@ TODO list for a new release on the VSCode Marketplace
 
 The github DICD pipeline detects the existance of a new version of the Lambdapi extension for Vscode based on the `version` field in the `editors/vscode/package.json` file and publishes it on the Marketplace.
 
-Please note that a valid Azure Personal Access Token (PAT) is required for this operation. This PAT must be saved in the `PAT` environment variable as described [here](https://docs.github.com/en/actions/security-guides/using-secrets-in-github-actions).
+Please note that a valid Azure Personal Access Token (PAT) is required for this operation. This PAT must be saved in the `VSCODE_PAT` environment variable as described [here](https://docs.github.com/en/actions/security-guides/using-secrets-in-github-actions).
 
 If the pipeline fails at publishing the extension, it may be due to the PAT being expired.
-Please generate a new one on [Azure](https://dev.azure.com/lambdapi/) and update the `PAT` env variable value as described in the link above.
+Please generate a new one on [Azure](https://dev.azure.com/lambdapi/) and update the `VSCODE_PAT` env variable value as described in the link above.
 
 **manual release**
 

editors/vscode/package.json

@@ -8,7 +8,7 @@
     "François Lefoulon <[email protected]>",
     "Ashish Barnawal <[email protected]>"
   ],
-  "version": "0.2.1",
+  "version": "0.2.2",
   "publisher": "Deducteam",
   "engines": {
     "vscode": "^1.82.0"

editors/vscode/src/client.ts

@@ -163,6 +163,34 @@ function checkProofBackward(context: ExtensionContext) {
 
 function checkProofUntilCursor(context: ExtensionContext) {
 
+    function previousCaracterSkippingSpaces(document: TextDocument, currentPos: Position) {
+        const index = document.offsetAt(currentPos)
+        const slicedText = document.getText().slice(0, index);
+
+    // Match the last letter before a series of spaces and tabulations
+        const regex =/(\S)(?=[ \t]*$)/;
+
+    // Find the last letter before spaces
+        let myMatch = slicedText.match(regex);
+
+    // return the last letter if found
+        return myMatch ? myMatch[1] : null;
+    }
+
+    function nextCaracterSkippingSpaces(document: TextDocument, currentPos: Position) {
+        const index = document.offsetAt(currentPos)
+        const slicedText = document.getText().slice(index);
+
+    // Match the last letter after spaces and tabulations
+        const regex = /(\S)(?=[ \t]*$)/;
+
+    // Find the last letter after spaces
+        let myMatch = slicedText.split(/\r?\n/)[0].match(regex);
+
+    // return the last letter if found
+        return myMatch ? myMatch[0] : null;
+    }
+
     //Checking workspace
     const openEditor: TextEditor | undefined = window.activeTextEditor;
     if (!openEditor)
@@ -178,13 +206,16 @@ function checkProofUntilCursor(context: ExtensionContext) {
 
     //The current position of the cursor
     let cursorPosition: Position = openEditor.selection.active;
-    if (proofState.line == cursorPosition.line)
-        return;
 
-    //To simplify the code, proof states are always at the beggining of the highlighted line
-    //So must be the cursor position since it is the new proof state
-    if (cursorPosition.character != 0)
-        cursorPosition = new Position(cursorPosition.line, 0);
+    const cursorIsAtEndOfCommand = previousCaracterSkippingSpaces(openEditor.document, cursorPosition) === ";";
+    const commandExistsAfterCursorinSameLine = nextCaracterSkippingSpaces(openEditor.document, cursorPosition) != null;
+
+    // If the cursor is at the begining or in the middle of a command or there are more commands in the same line,
+    // then do not move the green zone further.
+    // Else, stop at the current position
+    if(!cursorIsAtEndOfCommand || commandExistsAfterCursorinSameLine) {
+        cursorPosition = stepCommand(openEditor.document, cursorPosition, true);
+    }
 
     context.workspaceState.update('proofState', cursorPosition); //proof state is set to the cursor position
 
@@ -509,7 +540,11 @@ function stepCommand(document: TextDocument, currentPos: Position, forward: bool
     const termRegex = new RegExp(terminators.join("|"), 'gi');
 
     let termPositions = [...document.getText().matchAll(termRegex)]
-        .map(rm => rm.index ? rm.index + rm[0].length : undefined)
+        .map(rm => { 
+            if (rm[0] === ";") {
+                return rm.index ? rm.index + rm[0].length : undefined
+            }
+            else return rm.index ? rm.index : undefined })
         .filter((x): x is number => x !== undefined) // remove undefined
         .map(x => document.positionAt(x));
 
@@ -664,6 +699,15 @@ function sendGoalsRequest(position: Position, panel: WebviewPanel, docUri: Uri,
     let cursor = { textDocument: doc, position: position };
     const req = new RequestType<ParamsGoals, GoalResp, void>("proof/goals");
     client.sendRequest(req, cursor).then((goals) => {
+        // If uri is not a lambdapi/dedukti file, do nothing
+        if(goals.goals == null){
+            return;
+        }
+        // Take focus back if the goal panel lost it.
+        window.showErrorMessage("Going through Goals");
+        if(!panel.active) {
+            panel.reveal(2, false);
+        }
 
         updateTerminalText(goals.logs);
 

src/lsp/lp_doc.ml

@@ -164,35 +164,29 @@ let dummy_loc =
 
 let check_text ~doc =
   let uri, version = doc.uri, doc.version in
+  let cmds, error = Pure.parse_text ~fname:uri doc.text in
   let root =
     match doc.root with
-    | Some(ss) -> ss
+    | Some ss -> ss
     | None ->
-      raise(Error.fatal_no_pos "Root state is missing
-      probably because new_doc has raised exception")
+        raise(Error.fatal_no_pos "Root state is missing probably because \
+                                  new_doc raised an exception")
   in
-  try
-    let cmds =
-      let (cmds, root) = Pure.parse_text root ~fname:uri doc.text in
-      (* One shot state update after parsing. *)
-      doc.root <- Some(root); doc.final <- Some(root); cmds
-    in
-
-    (* compute rangemap *)
-    let map = Pure.rangemap cmds in
-
-    let nodes, final, diag, logs =
-      List.fold_left (process_cmd uri) ([],root,[],[]) cmds in
-    let logs = List.rev logs in
-    let doc = { doc with nodes; final=Some(final); map; logs } in
-    doc,
-    LSP.mk_diagnostics ~uri ~version @@
+  let nodes, final, diags, logs =
+    List.fold_left (process_cmd uri) ([],root,[],[]) cmds in
+  let logs = List.rev logs
+  and diags = (* filter out diagnostics with no position *)
     List.fold_left (fun acc (pos,lvl,msg,goal) ->
         match pos with
         | None     -> acc
         | Some pos -> (pos,lvl,msg,goal) :: acc
-      ) [] diag
-  with
-  | Pure.Parse_error(loc, msg) ->
-    let logs = [((1, msg), Some loc)] in
-    {doc with logs}, mk_error ~doc loc msg
+      ) [] diags
+  in
+  let logs, diags =
+    match error with
+    | None -> logs, diags
+    | Some(pos,msg) -> logs @ [((1, msg), Some pos)], diags @ [pos,1,msg,None]
+  in
+  let map = Pure.rangemap cmds in
+  let doc = { doc with nodes; final=Some(final); map; logs } in
+  doc, LSP.mk_diagnostics ~uri ~version diags

src/lsp/lp_lsp.ml

@@ -238,7 +238,7 @@ let get_node_at_pos doc line pos =
 let rec get_goals ~doc ~line ~pos =
   let node = get_node_at_pos doc line pos in
   let goals = match node with
-    | None -> None
+    | None -> Some([], None)
     | Some n ->
         closest_before (line+1, pos) n.goals in
   match goals with
@@ -294,7 +294,7 @@ let get_logs ~doc ~line ~pos : string =
       (fun ((_,msg),loc) ->
          match loc with
          | Some Pos.{start_line; start_col; _}
-           when compare (start_line,start_col) end_limit <= 0 -> Some msg
+           when compare (start_line,start_col) end_limit < 0 -> Some msg
          | _ -> None)
       doc.Lp_doc.logs
   in
@@ -526,7 +526,14 @@ let process_input ofmt (com : J.t) =
   | exn ->
     let bt = Printexc.get_backtrace () in
     LIO.log_error "[BT]" bt;
-    LIO.log_error "process_input" (Printexc.to_string exn)
+    LIO.log_error "process_input" (Printexc.to_string exn);
+    (*Send an "empty" answer with Null goals when exception occurs*)
+    let id     = oint_field "id" (U.to_assoc com) in
+    let goals = None in
+    let logs = "" in
+    let result = LSP.json_of_goals goals ~logs in
+    let msg = LSP.mk_reply ~id ~result in
+    LIO.send_json ofmt msg
 
 let main std log_file =
 

src/parsing/lpLexer.ml

@@ -338,7 +338,10 @@ and comment next i lb =
 (** [token buf] is a lexing function on buffer [buf] that can be passed to
     a parser. *)
 let token : lexbuf -> unit -> token * Lexing.position * Lexing.position =
-  with_tokenizer token
+  fun lb () -> try with_tokenizer token lb () with
+  | Sedlexing.MalFormed -> fail lb "Not Utf8 encoded file"
+  | Sedlexing.InvalidCodepoint k ->
+      fail lb ("Invalid Utf8 code point " ^ string_of_int k)
 
 let token =
   let r = ref (EOF, Lexing.dummy_pos, Lexing.dummy_pos) in fun lb () ->

src/pure/pure.ml

@@ -58,30 +58,23 @@ end
 type state = Time.t * Sig_state.t
 
 (** Exception raised by [parse_text] on error. *)
-exception Parse_error of Pos.pos * string
 
-let parse_text : state -> fname:string -> string -> Command.t list * state =
-    fun (t,st) ~fname s ->
-  let dk_syntax = Filename.check_suffix fname dk_src_extension in
+let parse_text :
+      fname:string -> string -> Command.t list * (Pos.pos * string) option =
+  fun ~fname s ->
+  let parse_string =
+    if Filename.check_suffix fname dk_src_extension then
+      Parser.Dk.parse_string
+    else Parser.parse_string
+  in
+  let cmds = Stdlib.ref [] in
   try
-    LibMeta.reset_meta_counter();
-    Time.restore t;
-    let ast =
-      let strm =
-        if dk_syntax then Parser.Dk.parse_string fname s
-        else Parser.parse_string fname s
-      in
-      (* NOTE this processing could be avoided with a parser for a list of
-         commands. Such a parser is not trivially done. *)
-      let cmds = Stdlib.ref [] in
-      Stream.iter (fun c -> Stdlib.(cmds := c :: !cmds)) strm;
-      List.rev Stdlib.(!cmds)
-    in
-    (ast, (Time.save (), st))
+    Stream.iter (fun c -> Stdlib.(cmds := c :: !cmds)) (parse_string fname s);
+    List.rev Stdlib.(!cmds), None
   with
-  | Fatal(Some(Some(pos)), msg) -> raise (Parse_error(pos, msg))
-  | Fatal(Some(None)     , _  ) -> assert false (* Should not produce. *)
-  | Fatal(None           , _  ) -> assert false (* Should not produce. *)
+  | Fatal(Some(Some(pos)), msg) -> List.rev Stdlib.(!cmds), Some(pos, msg)
+  | Fatal(Some(None)     , _  ) -> assert false
+  | Fatal(None           , _  ) -> assert false
 
 type proof_finalizer = Sig_state.t -> Proof.proof_state -> Sig_state.t