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

.github/workflows/main.yml

@@ -50,6 +50,9 @@ jobs:
           npm install -g @types/vscode
           npm install -g vsce 
           make build-vscode-extension
+          make publish-vscode-extension
+        env:
+          PAT: ${{secrets.VSCODE_PAT}}
       - name: publish vscode extension
         uses: actions/upload-artifact@v4
         with: 

CHANGES.md

@@ -7,7 +7,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ### Added
 
-- add export format `raw_dk`
+- 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 queries answers.
 
 ## 2.5.0 (2024-02-25)
 

Makefile

@@ -170,3 +170,11 @@ uninstall_vim_mode:
 .PHONY: build-vscode-extension
 build-vscode-extension:
 	cd editors/vscode && make && mkdir extensionFolder && vsce package -o extensionFolder
+
+.PHONY: publish-vscode-extension
+publish-vscode-extension:
+ifeq ($(shell vsce show --json deducteam.lambdapi | jq '.versions[0]' | jq '.version'), $(shell cat editors/vscode/package.json | jq '.version'))
+	echo "extension already exists. Skip"
+else
+	cd editors/vscode && vsce publish -p ${PAT}
+endif

doc/options.rst

@@ -110,6 +110,8 @@ For the format ``stt_coq``, several other options are available:
 
 It tells Lambdapi which symbols of the input files are used for the encoding. Example: `encoding.lp <https://github.com/Deducteam/lambdapi/blob/master/libraries/encoding.lp>`__. The first argument ``a`` of the symbols corresponding to the builtins ``"eq"``, ``"all"`` and ``"ex"`` need not be declared as implicit.
 
+In symbol declarations or definitions, parameters with no type are assumed to be of type the term associated with the builtin ``"Set"``.
+
 * ``--no-implicits`` instructs Lambdapi that the symbols of the encoding have no implicit arguments.
 
 * ``--renaming <LP_FILE>`` where ``<LP_FILE>`` contains a sequence of builtin declarations of the form

editors/vscode/INSTALL.md

@@ -6,7 +6,7 @@ Installation from the sources
 - extract node:
 
 ```bash
-sudo apt-get install xz-utils # if you do not have xz already installed
+sudo apt-get install jq xz-utils
 tar xfa $node_file.tar.xz # creates $node_dir
 ```
 
@@ -35,7 +35,7 @@ If you intend to do this often, it is recomanded to add the two `export` command
 
 ```bash
 npm install -g @types/vscode
-npm install -g vsce # for creating VSCE packages only
+npm install -g @vscode/vsce # to create VSCE packages
 ```
 
 - compilation:

editors/vscode/RELEASE.md

@@ -1,7 +1,18 @@
 TODO list for a new release on the VSCode Marketplace
 -----------------------------------------------------
+**Release from pipeline**
 
-See the details [here](https://code.visualstudio.com/api/working-with-extensions/publishing-extension).
+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).
+
+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.
+
+**manual release**
+
+Though it is not recommanded, it is still possible to manually publish a new version on the marketplace as described bellow 
+(See the details [here](https://code.visualstudio.com/api/working-with-extensions/publishing-extension)).
 
 - Check the rendering of README.md in some [Markdown viewer](https://codebeautify.org/markdown-viewer). It will be displayed in VSCode by going to extensions
 (Ctrl+Shift+X) and by clicking on lambdapi.

src/common/console.ml

@@ -20,6 +20,7 @@ let set_default_verbose : int -> unit = fun i ->
     [lvl] is strictly greater than the current verbosity level.  Note that the
     output channel is automatically flushed if logging modes are enabled. *)
 let out : int -> 'a outfmt -> 'a = fun lvl fmt ->
+  Color.update_with_color Stdlib.(!out_fmt);
   let out = Format.(if lvl > !verbose then ifprintf else fprintf) in
   out Stdlib.(!out_fmt) (fmt ^^ "@.")
 

src/common/pos.ml

@@ -99,18 +99,20 @@ let to_string : ?print_fname:bool -> pos -> string =
   else
     Printf.sprintf "%s%d:%d-%d" fname start_line start_col end_col
 
+let popt_to_string : ?print_fname:bool -> popt -> string =
+  fun ?(print_fname=true) pop ->
+  match pop with
+    | None -> "Unknown location "
+    | Some (p) -> to_string ~print_fname p ^ " "
+
 (** [pp ppf pos] prints the optional position [pos] on [ppf]. *)
 let pp : popt Lplib.Base.pp = fun ppf p ->
-  match p with
-  | None    -> string ppf "unknown location"
-  | Some(p) -> string ppf (to_string p)
+  string ppf (popt_to_string p)
 
 (** [short ppf pos] prints the optional position [pos] on [ppf]. *)
 let short : popt Lplib.Base.pp = fun ppf p ->
-  match p with
-  | None    -> string ppf "unknown location"
-  | Some(p) -> let print_fname=false in
-               string ppf (to_string ~print_fname p)
+  let print_fname=false in
+  string ppf (popt_to_string ~print_fname p)
 
 (** [map f loc] applies function [f] on the value of [loc] and keeps the
     position unchanged. *)

src/core/dune

@@ -2,7 +2,7 @@
  (targets version.ml)
  (action
   (with-stdout-to version.ml
-    (run ocaml unix.cma %{dep:../../misc/gen_version.ml})))
+    (run ocaml -I +unix unix.cma %{dep:../../misc/gen_version.ml})))
  (mode fallback))
 
 (library