Frédéric Blanqui

Incorrect use of Unicode symbol in error message for Coq

1

See https://github.com/ProofGeneral/PG/issues/616.

Comparison on 22/02/24 of db branch 60945055 with master branch 9597727 on Intel(R) Core(TM) i7-8665U CPU @ 1.90GHz with 32Go RAM and ocaml 4.14.1: | library | master | db...

TODO - [ ] remove --confluence/--termination options ? - [ ] check XTC output - [ ] add tests for HRS and XTC outputs

Problem in the generation of fresh metavariables in unification rule applications

5

``` symbol A:TYPE; symbol B:TYPE; symbol C:TYPE; symbol a:A; unif_rule A ≡ B ↪ [ A ≡ Π x:C, $m[x] ]; symbol b : B ≔ begin print; refine a;...

``` 16:47 ~/src/lambdapi (db) lambdapi check --no-col 16:51 ~/src/lambdapi (db) lambdapi check --blabla lambdapi: unknown option `--blabla'. Usage: lambdapi check [OPTION]... [FILE]... Try `lambdapi check --help' or `lambdapi --help' for...

``` constant symbol A : TYPE; constant symbol a : A; symbol f : A → A; rule f $x ↪ $x; rule f _ ↪ a; [/home/blanqui/src/lambdapi/tmp/dup_cp.lp:6:0-13] Unjoinable critical...

``` symbol T:TYPE; constant symbol arrow : T → T → T; constant symbol L : T → TYPE; symbol app a b : L (arrow a b) → L...

Libraries to check: - make dklib focalide matita holide verine iprover zenon_modulo - https://github.com/Deducteam/dedukti_set_theory - https://github.com/Deducteam/ett-in-lambdapi - https://github.com/fblanqui/lib

Currently, normalization of defined variables is not shared: https://github.com/Deducteam/lambdapi/blob/326d987306c51f1092d5cef6c36fc28f26896aa4/src/core/eval.ml#L164-L168 In addition, would it be better to deal with let's by extending c.defmap instead? https://github.com/Deducteam/lambdapi/blob/326d987306c51f1092d5cef6c36fc28f26896aa4/src/core/eval.ml#L154-L155