diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index f9921083f..a3cee9e09 100644 --- a/.github/workflows/main.yml +++ b/.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 diff --git a/.ocamlformat b/.ocamlformat deleted file mode 100644 index ca44b5ae6..000000000 --- a/.ocamlformat +++ /dev/null @@ -1,19 +0,0 @@ -version=0.15.0 -profile=ocamlformat - -# to enable a whole directory, put "disable=false" in dir/.ocamlformat -# to enable specific files put them in .ocamlformat-enable -disable=true - -module-item-spacing=compact -sequence-style=terminator -cases-exp-indent=2 -field-space=loose -exp-grouping=preserve -break-cases=fit -doc-comments=before -space-around-records -space-around-lists -space-around-arrays -wrap-comments=true -parse-docstrings=true diff --git a/CHANGES.md b/CHANGES.md index f1cba03b4..935c360f2 100644 --- a/CHANGES.md +++ b/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. diff --git a/Makefile b/Makefile index 59dd48617..9673948f1 100644 --- a/Makefile +++ b/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 \ No newline at end of file diff --git a/editors/vscode/CHANGES.md b/editors/vscode/CHANGES.md index fdecc2e40..bb8d98305 100644 --- a/editors/vscode/CHANGES.md +++ b/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 diff --git a/editors/vscode/RELEASE.md b/editors/vscode/RELEASE.md index a2ea96bdd..9a611586c 100644 --- a/editors/vscode/RELEASE.md +++ b/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** diff --git a/editors/vscode/package.json b/editors/vscode/package.json index fc13a67c5..e173c9d3f 100644 --- a/editors/vscode/package.json +++ b/editors/vscode/package.json @@ -8,7 +8,7 @@ "François Lefoulon ", "Ashish Barnawal " ], - "version": "0.2.1", + "version": "0.2.2", "publisher": "Deducteam", "engines": { "vscode": "^1.82.0" diff --git a/editors/vscode/src/client.ts b/editors/vscode/src/client.ts index 7ee27277e..362ba7463 100644 --- a/editors/vscode/src/client.ts +++ b/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("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); diff --git a/src/lplib/.ocamlformat b/src/lplib/.ocamlformat deleted file mode 100644 index a22a2ff88..000000000 --- a/src/lplib/.ocamlformat +++ /dev/null @@ -1 +0,0 @@ -disable=false diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml index 48d437f6e..4bd40cce8 100644 --- a/src/lsp/lp_doc.ml +++ b/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 diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index 7023d40f2..ae3d6a5b1 100644 --- a/src/lsp/lp_lsp.ml +++ b/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 = diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml index 6511ba136..ef1e3432d 100644 --- a/src/parsing/lpLexer.ml +++ b/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 () -> diff --git a/src/pure/pure.ml b/src/pure/pure.ml index 1e4d78363..0ab9a9d16 100644 --- a/src/pure/pure.ml +++ b/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 diff --git a/src/pure/pure.mli b/src/pure/pure.mli index a9b532c8d..0ac8f2e08 100644 --- a/src/pure/pure.mli +++ b/src/pure/pure.mli @@ -35,14 +35,12 @@ type state (** Representation of the state when in a proof. *) type proof_state -(** Exception raised by [parse_text]. *) -exception Parse_error of Pos.pos * string - -(** [parse_text st ~fname contents] runs the parser on the string [contents] - as if it were a file named [fname]. The action takes place in the state - [st], and an updated state is returned. The function may raise - [Parse_error]. *) -val parse_text : state -> fname:string -> string -> Command.t list * state +(** [parse_text ~fname contents] runs the parser on the string [contents] as + if it were a file named [fname]. It returns the list of commands it could + parse and, either [None] if it could parse all commands, or some position + and error message otherwise. *) + val parse_text : + fname:string -> string -> Command.t list * (Pos.pos * string) option (** A goal is given by a list of assumptions and a conclusion. Each assumption has a name and a type. *) diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml index a555e1917..a21a507af 100644 --- a/src/tool/indexing.ml +++ b/src/tool/indexing.ml @@ -308,7 +308,7 @@ module DB = struct (* disk persistence *) - let dbpath = Sys.getenv "HOME" ^ "/.LPSearch.db" + let dbpath = "~/.LPSearch.db" let rwpaths = ref [] let restore_from_disk () = diff --git a/tests/regressions/.ocamlformat b/tests/regressions/.ocamlformat deleted file mode 100644 index a22a2ff88..000000000 --- a/tests/regressions/.ocamlformat +++ /dev/null @@ -1 +0,0 @@ -disable=false diff --git a/tests/runtests.sh b/tests/runtests.sh index 57b2a0569..3f4fbd564 100755 --- a/tests/runtests.sh +++ b/tests/runtests.sh @@ -14,22 +14,11 @@ ok_tests() { tests/OK/why3*.lp);; #FIXME *) echo lambdapi check $options $f ... - $lambdapi "$f" > $out 2>&1 - if test $? -ne 0; then cat $out; exit 1; fi;; + $lambdapi "$f" > $out 2>&1 || (cat $out; exit 1) esac done } -ko_tests() { - echo '############ KO tests ############' - for f in tests/KO/*.lp tests/KO/*.dk - do - echo lambdapi check $f ... - $lambdapi "$f" > $out 2>&1 - if test $? -eq 0; then cat $out; exit 1; fi - done -} - rm -f 'tests/OK/a b/escape file.lpo' tests/OK/*.lpo echo "############ compile tests/OK files ############" diff --git a/tests/test_lib.sh b/tests/test_lib.sh new file mode 100755 index 000000000..7f481546d --- /dev/null +++ b/tests/test_lib.sh @@ -0,0 +1,31 @@ +#!/bin/bash + +set -e + +lambdapi='dune exec -- lambdapi check' +options='-w' +TIMEFORMAT="%Es" + +out=/tmp/lambdapi.output + +checkout_lib() { + IFS='/' read -ra ADDR <<< "$1" + repo_path="${ADDR[-1]}" + IFS='.' read -ra ADDR <<< "$repo_path" + repo_path="/tmp/${ADDR[0]}" + if [ -d "$repo_path" ] ; then + rm -fr "$repo_path" + fi + git clone $1 $repo_path +} + +test_lib() { + for f in $(find $1 -name '*.lp' -o -name '*.dk') + do + echo lambdapi check $options $f ... + $lambdapi "$f" > $out 2>&1 || (cat $out; exit 1) + done +} + +checkout_lib $1 +time test_lib $repo_path