Frédéric Blanqui

add tactic set

4

TODO: - [x] print definitions in lsp clients - [ ] replace t by x in the current goal when doing set x := t - [ ] extend tactic...

``` -------- Message transféré -------- Sujet : [Termtools] new ARI format at termCOMP '24 Date : Fri, 26 Apr 2024 12:10:26 +0200 De : Florian Frohn [](mailto:[email protected]) Pour : termtools...

Dune langage version and menhir version incompatible

2

``` 07:39 ~/src/dedukti ((HEAD détachée sur 5990bc6c)) make install File "dune-project", line 3, characters 14-17: 3 | (using menhir 2.0) ^^^ Warning: Version 2.0 of the menhir extension is not...

opam install ocamlfind.1.9.5 fails with ocaml 4.00.1

1

``` 15:58 ~/src/hol-light (master) ocamlc -v The OCaml compiler, version 4.00.1 Standard library directory: /home/blanqui/.opam/4.00.1/lib/ocaml 15:57 ~/src/hol-light (master) opam install ocamlfind The following actions will be performed: ∗ install ocamlfind...

Hi Michael. I tested kontroli on the translation of the HOL-Light base library to Dedukti (http://files.inria.fr/blanqui/hol-for-kocheck.dk.gz) and it seems slower than dkcheck. Using a computer with 32 processors Intel(R) Core(TM)...

Missing keywords

2

Hi Michael. Would it be possible to accept the keywords "#REQUIRE" and "injective", even if you do nothing with them? This would help using kocheck with currently produced dk files...

In Emacs, when the LSP server hasn't run yet and we do Ctrl-C Ctrl-K, Emacs loops and we need to kill it by hand.

``` 18:05 ~/src/opam-coq-repository/released/packages (master) l coq-lens/coq-lens.1.0.1+8.12/opam opam-version: "2.0" synopsis: "Generation of lenses for record datatypes" maintainer: "[email protected]" authors: [ "Gregory Malecha " ] homepage: "https://github.com/bedrocksystems/coq-lens" dev-repo: "git://github.com/bedrocksystems/coq-lens.git" bug-reports: "https://github.com/bedrocksystems/coq-lens/issues" license:...