Frédéric Blanqui

Improve handling of bad credentials erros by suggesting to generate a new token.

5

Hello. I get the following error: ``` 14:40 ~/trash/lambdapi (release) dune-release publish distrib [-] Publishing distribution [-] Publishing to github [-] The tag 2.1.0 is present and uptodate on the...

Question about #REQUIRE

3

#REQUIRE does not seem necessary and can be ignored. What is it for?

``` Prop:Type. def Prf:Prop -> Type. N:Type. eq:N -> N -> Prop. def add:N -> N -> N. add_com1 (x:N) (y:N) : Prf(eq (add x y) (add y x)). def...

Why Reduction.are_convertible_lst calls term_eq ?

5

This has been pointed to me by @01mf02. It looks useless and inefficient. The code of conversion_step looks strange too (calls to snf).

``` 09:09 /tmp l tests_OK_why3_quantifiers.dk def o : tests_OK_logic.U. 09:10 /tmp l tests_OK_logic.dk U : Type. 09:10 /tmp dkdep.native -q -s tests_OK_why3_quantifiers.dk dkdep: internal error, uncaught exception: Api.Files.Files_error(_) ```

https://raw.githubusercontent.com/Deducteam/Dedukti/master/syntax.bnf is not up to date

With ``` Set : Type. Prop : Type. def El : ({|_|} : Set -> Type). def Prf : ({|_|} : Prop -> Type). o : Set. [] El o...

new_line counting different with from_string and from_channel

1

We currently get some trouble with new_line counting (see https://github.com/Deducteam/lambdapi/issues/549). When reading from a file, the line position is correctly incremented but not when reading from a string. The code...

Alt-ergo incompatible with menhir.20211125 when using ocaml 4.08, 4.09 or 4.10 ?

5

Hi. I have a strange error this morning. See https://github.com/Deducteam/lambdapi/runs/4332121191?check_suite_focus=true. Alt-ergo fails when menhir is upgraded from 20211012 to 20211125 but opam info menhir mentions no 20211125 version for menhir...

This is not a bug report, just to tell you thank you for the improvement on the efficiency (-14%)! Results with Coq 8.15: ``` 18:51 ~/src/color (master) l log-8.15.0 generate...