Zulip Chat Archive

Stream: general

Topic: emacs lean-mode


Kevin Buzzard (Feb 27 2018 at 22:21):

I am going to switch to using emacs for writing lean files for a while; I am now competent with VS Code and sort of believe it to be a better end user experience than emacs. The reason I'm switching to emacs is because there is a risk that it will be the best option for some of my undergraduates in October. I think that I can offer them (via cocalc) blisteringly fast Lean plus group editing of files etc, except that they will have to use emacs.

Andrew Ashworth (Feb 27 2018 at 22:23):

emacs CUA mode isn't so bad, and I say this as a dirty windows user

Moses Schönfinkel (Feb 27 2018 at 22:24):

Windows hate is amusing in here considering a lot of Lean comes from MS Research :).

Kevin Buzzard (Feb 27 2018 at 22:24):

Here is something I find much easier to do in VS Code. I have completion running with company-lean, and I can get shift space to give me a big list of cool stuff (possible completions of what I've typed) plus types of the completions. I just want to cut and paste from one of these types

Kevin Buzzard (Feb 27 2018 at 22:25):

I select the correct completion and the type disappears. I then stop what I'm doing and type #check (the thing whose type I was interested in) and even then I can't access the output. So I then have to change buffers and cut and paste from there and then change back.

Kevin Buzzard (Feb 27 2018 at 22:25):

Am I missing a trick?

Andrew Ashworth (Feb 27 2018 at 22:25):

downside: you may be one of three people using company-lean

Simon Hudon (Feb 27 2018 at 22:27):

Windows hate is amusing in here considering a lot of Lean comes from MS Research :).

Windows is an interesting cute project but I'm not sure it will amount to much :stuck_out_tongue:

Moses Schönfinkel (Feb 27 2018 at 22:27):

I love windows.

Moses Schönfinkel (Feb 27 2018 at 22:28):

Honestly the amount of headaches I've had with various Linux distros. Ever since probably Win7 I've never really run into any sort of an issue with win.

Simon Hudon (Feb 27 2018 at 22:28):

But seriously, I love to hate windows but it got harder when they came up with the Slam checker. It kind of makes it look like they take software engineering and modularity more seriously than Apple

Simon Hudon (Feb 27 2018 at 22:29):

I love windows.

Have you had to turn on your computer since installing Windows 7?

Joey Dodds (Feb 27 2018 at 22:30):

Have you seen vscode live editing?

Moses Schönfinkel (Feb 27 2018 at 22:30):

Yes, my Win 7 8 and 10 have been running close to flawlessly.

Joey Dodds (Feb 27 2018 at 22:30):

live share I guess

Joey Dodds (Feb 27 2018 at 22:31):

(I'd be completely windows native is windows subsystem for Linux worked with Haskell)

Moses Schönfinkel (Feb 27 2018 at 22:31):

Que?

Andrew Ashworth (Feb 27 2018 at 22:33):

why does haskell need wsfl?
even before windows subsystem | docker for windows there was mingw, cygwin, virtual box, i've been happy developing on a windows host for decades now
despite this, i know way more about pthreads than about CreateProcess...

Moses Schönfinkel (Feb 27 2018 at 22:34):

You mean you don't know by heart what all those 49 parameters do?

Andrew Ashworth (Feb 27 2018 at 22:35):

maybe std::threads and modules will arrive before i'm an old man

Andrew Ashworth (Feb 27 2018 at 22:36):

and then i'll never need to know

Moses Schönfinkel (Feb 27 2018 at 22:37):

Nope, we need new fancy ways to initialize stuff. Call it uniform so at least something gives you the right to call it so.

Moses Schönfinkel (Feb 27 2018 at 22:38):

And then mix the syntax up with initializer lists. Then give up on the language.

Joey Dodds (Feb 27 2018 at 22:42):

I use virtualbox, but that's probably heavyweight to consider it developing on windows

Joey Dodds (Feb 27 2018 at 22:43):

I'm using Haskell tools that depend on C code that is challenging to build on windows

Sebastian Ullrich (Feb 27 2018 at 23:21):

@Kevin Buzzard I'm not sure if you can copy company candidates, but for those in the decl search window (C-c C-d) you can use C-c C-y.

Kevin Buzzard (Feb 28 2018 at 00:14):

I shall star that reply and consider it later when I have an emacs open. Yay for non-gitter things.


Last updated: Dec 20 2023 at 11:08 UTC