** [[https://coq.inria.fr][Coq]] (with [[https://github.com/ProofGeneral/PG][Proof General]])
#+begin_src emacs-lisp
-(use-package proof-general)
+(use-package proof-site
+ :straight proof-general)
#+end_src
** [[https://leanprover.github.io][Lean]] (with [[https://github.com/leanprover/lean-mode][lean-mode]])
#+begin_src emacs-lisp
(use-package shrink-path
- :after eshell
+ :defer 2
:config
(setq eshell-prompt-regexp "\\(.*\n\\)*λ "
eshell-prompt-function #'+eshell/prompt)
#+begin_src emacs-lisp
(use-package eshell-up
+ :commands eshell-up
:after eshell)
#+end_src