Re: [isabelle] Another newbie proofs

Just as historic fun fact: in 2007 I supervised a bachelor project that
developed a vim plugin ("Plugvim") for interacting with "Isabelle". It
kind of worked at that time (when Isabelle itself was in the end just a
REPL), but never for serious work. Anyway, it is long forgotten (or
rather never took of in the first place) and even though I am using vim
for most everything except when working with Isabelle, I am not looking
back: The continuous and parallel proof checking and semantic
information that comes with the Prover IDE is just too valuable.



On 4/5/19 1:39 PM, Makarius wrote:
> On 05/04/2019 13:31, Mathias Fleury wrote:
>> As long as Isabelle supports the language server protocol, it is possible to make vim interact with Isabelle (with some limitations; e.g., there are no colours in the equivalent of the 'buffer+output buffer'). However, the integration requires some work. I don't know anything about the internals of vim, but, at least in emacs, the lack of multithreading is an issue.
> I would say that is rather theoretical. A really working Prover IDE
> requires a lot of polishing and finishing beyond such standardized (and
> limited) protocols.
>> Otherwise, VSCode probably has a mode with vim keybindings.
> It has one, but vim users have told me that it is not very serious. I
> also see a vi mode in IntelliJ IDEA, but cannot say anything about its
> quality.
> Generally, one needs to understand that Isabelle came out of an Emacs
> environment, but in the past 7 years that has been lost its relevance.
> Since 4.5 years there is no way to get back to it.
> Vi never had a role in the Isabelle community. It is a plain text
> editor, not the basis of a multithreaded IDE.
> 	Makarius

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.