Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-05-16

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
01:48 ilbot3 joined #isabelle
01:48 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
04:15 keep_learning joined #isabelle
05:30 keep_learning Hi Everyone
05:31 keep_learning I have downloaded the latest version http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html
05:32 keep_learning and going through https://proofgeneral.github.io/doc/userman/ProofGeneral_3/#Walkthrough-example-in-Isabelle
05:33 keep_learning When I type C-c C-n it says Searching for program: no such file or directory, isabelle-process
05:33 keep_learning While in bin directory
05:34 keep_learning u5935541@newport:~/Mukesh/Isabelle2016-1/bin$ ls
05:34 keep_learning isabelle  isabelle_java  isabelle_scala_script
05:34 keep_learning There is no isabelle-process file
05:34 keep_learning Any idea how to resolve this
05:35 larsrh keep_learning: ProofGeneral doesn't work for recent Isabelle
05:38 keep_learning larsrh: It means I need to use editor given with distribution ?
05:38 larsrh yes
05:38 keep_learning larsrh: Thank you
05:39 keep_learning larsrh: I am wondering why they took away the emacs support. Just curious.
05:43 larsrh keep_learning: because the way jEdit interaction works and Emacs interaction works have been diverging since at least 2011
05:43 larsrh and it became too hard to maintain both
05:56 pruvisto Makarius is working on Visual Studio Code support though
05:57 pruvisto I'm somewhat wary of that Electron-powered Lovecraftian monster, but we'll see.
06:15 fowlslegs joined #isabelle
06:22 larsrh pruvisto: those use mostly similar technology though
06:29 pruvisto "those"?
06:30 pruvisto You mean jEdit and VSC?
06:30 pruvisto Yes, it was more in the vein of "if you don't like jEdit, support for another editor may be coming soon-ish"
06:32 int-e I was blissfully unaware of Electron before https://blog.fefe.de/?ts=a7eb7243 ... now I'm scared :P
06:35 pruvisto Electron itself doesn't really surprise me
06:35 pruvisto People have been writing performance- and safety-critical web stuff in PHP for ages
06:36 pruvisto So why not write desktop applications in Node.js with an entire bloaty web browser as an interpreter
06:36 pruvisto But I am a bit surprised that Microsoft uses it
06:36 pruvisto I would have expected them to just use .NET
06:39 pruvisto I mean, you can even run that on Mac OS X and Linux if you really want to
06:40 larsrh int-e: uuuuh, fefe
08:30 ammbauer but we also get the language server protocol (http://sketis.net/2017/visual-studio-code-as-prover-ide-for-isabelle). then we can go back to emacs :D
08:55 pruvisto ammbauer: if you volunteer to implement it in Emacs. :P
09:09 JCaesar I'd really like to implement some standalone ncurses client that doesn't take any keyboard input and just displays the status window for the last line that has changed in the last file that was written, or so…
09:09 JCaesar As small and dumb as possible, anyway.
09:14 JCaesar Mh. I guess it does need a side channel to receive the current cursor position from the editor. But I've always hated that…
09:29 ammbauer pruvisto: https://github.com/emacs-lsp/lsp-mode/
10:03 pruvisto Hm. Not sure if that'll be enough to fully support Isabelle though.
10:03 pruvisto I very much doubt it.
10:03 pruvisto (I will never stop reading "lsp" as "lumpy space princess")
10:08 ammbauer does anyone know where I can find the release dates of all the isabelle version?
10:10 ammbauer okay, 'grep "New in Isabelle" NEWS' works :D
10:22 larsrh ammbauer: .hgtags
13:12 ammbauer joined #isabelle
13:30 ammbauer larsrh: ah, thanks
15:59 fowlslegs joined #isabelle
17:58 fowlslegs joined #isabelle
21:58 ertes joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary