emacs lean-mode

Stream: general

[Kevin Buzzard]

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]

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

[Moses Schönfinkel]

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

[Kevin Buzzard]

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]

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]

Am I missing a trick?

[Andrew Ashworth]

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

[Simon Hudon]

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]

I love windows.

[Moses Schönfinkel]

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]

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]

I love windows.

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

[Joey Dodds]

Have you seen vscode live editing?

[Moses Schönfinkel]

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

[Joey Dodds]

live share I guess

[Joey Dodds]

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

[Moses Schönfinkel]

Que?

[Andrew Ashworth]

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]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

and then i'll never need to know

[Moses Schönfinkel]

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]

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

[Joey Dodds]

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

[Joey Dodds]

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

[Sebastian Ullrich]

@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]

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