CODEWITHSUNDEEP
emacsisabelle
danielspaniol
danielspaniol

Reputation: 2338

How can I use Isabelle in Emacs

Most of the Isabelle documentation I see says that Proof-General supports Isabelle, but as far as I know PG dropped support about 5 years ago.

Is there another possibility to use (current) Isabelle with Emacs? Neither JEdit, nor VSCode really work for me.

Upvotes: 2

Views: 542

Answers (2)

gavenkoa
gavenkoa

Reputation: 48903

Proof General removed Isabelle support:

https://github.com/ProofGeneral/PG/blob/master/README.md

Removed instances: Twelf, CCC, Hol-Light, ACL2, Plastic, Lambda-Clam, HOL98, LEGO, Isabelle

There is incomplete attempt of Isabelle's LSP server:

Upvotes: 0

Mathias Fleury
Mathias Fleury

Reputation: 2281

There is no official solution and no way to make Proof General work again.

However, there is an unofficial solution. You could try isabelle-emacs (Disclaimer: I develop it in my free time. The experience is a bit rough, but there are a few people using it). It uses the Isabelle's LSP server like VScode, but it uses Emacs based. The difference between isabelle-emacs and Isabelle is limited to a few line in the LSP server and the Emacs specific code. Neither kernel nor any other theory is changed.

Upvotes: 7

Related Questions