Frédéric Blanqui
Frédéric Blanqui
``` Warning (smie): token simplify is both opener and neither Warning (smie): token [ is both opener and neither ```
Emacs interface very slow because of timeouts. `*EGLO events*` buffer: `jsonrpc-request: jsonrpc-error: "request id=17 failed:", (jsonrpc-error-message . "Timed out")`. Using lambdapi-mode 20240130.1533, jsonrpc 1.0.24, eglot 1.17.
When we insert some text in the green zone, the green zone is not reduced. The behavior is perhaps the same in VSCode (not checked).
VSCode doesn't work properly with the attached file. [cupicef.lp.txt](https://github.com/Deducteam/lambdapi/files/10522857/cupicef.lp.txt)
after dune clean, dune build fails: ``` File "editors/emacs/dune", line 5, characters 7-19: 5 | (run %{bin:emacs} --batch --quick --funcall batch-byte-compile ^^^^^^^^^^^^ Error: Program emacs not found in the tree...
when a search command produces several items, the first one is in red but the others are in black both in emacs and vscode
When requiring a module A which itself requires another module B, then B itself is loaded: https://github.com/Deducteam/lambdapi/blob/557de40f483080df08e6e3f2e1e44ffe3feb5a8b/src/handle/compile.ml#L75 even if what is exported from A may not actually depend on B....
Printing unification rules by using `print unif_rule` or `verbose` fails. The problem is in Term.term_of_rhs: r.arities.(i) is invalid if i corresponds to a RHS extra variable. Contrary to what is...
Example: tests/OK/ac.lp ``` lambdapi check --verbose 4 tests/OK/ac.lp Checking "/home/blanqui/src/lambdapi/tests/OK/ac.lp" ... /home/blanqui/src/lambdapi/tests/OK/ac.lp:3:0-25 constant symbol A : TYPE; symbol A : TYPE /home/blanqui/src/lambdapi/tests/OK/ac.lp:5:0-33 commutative symbol + : A → A →...