idle software developer to help make lean more easily usable

Stream: general

[Adam Kurkiewicz]

Hey guys, one of my student software developers (bright and hard-working, the type I like!) is going idle from today (we've just finished a project). He doesn't do any lean, but he's very good with windows installers, linux packaging, iOS apps, android apps and all sorts of boring software engineering fluff (actually he doesn't think it's boring, which is why I like him even more!). I think lean could use some help in that regard. Happy to chat more if anybody's interested. I vaguely remember @Kevin Buzzard in particular raising some issues with windows installers for lean or something along the lines.

[Patrick Massot]

The challenge is extremely easy to state: say you have a colleague who wants to try maths in Lean, either on Linux, MacOS or Windows. We want him to download one file, execute it, wait at most 3 minutes, and be ready to fire either emacs or VScode and play.

[Patrick Massot]

That would be a hugely useful achievement

[Johan Commelin]

Make that VScode please...

[Johan Commelin]

If they know emacs, they know how to do the rest themselves as well...

[Patrick Massot]

I meant the colleague should be able to choose between emacs and VScode.

[Patrick Massot]

I guess it's fair to assume emacs is already installed if the colleague want to use emacs, but the default stuff should be to install VScode along the way, unless the user explicitly refuses to get it.

[Adam Kurkiewicz]

I realise that this is something, which is badly needed, and happy to put some work to make it happen (especially working with Marcell, he's a really a brilliant software dev), but I'm afraid there would have to be a stream of funding for this. Marcell uses these kinds of jobs to pay for his rent, etc. and I don't think we could have him volunteer to do this.

[Patrick Massot]

Oh, I didn't get that from your first message.

[Adam Kurkiewicz]

Sorry, should have been more clear.

[Patrick Massot]

No idea who could have money for that, except MS of course

[Patrick Massot]

But I'm pretty sure Leo won't be interested right now

[Adam Kurkiewicz]

I could maybe ask for some money from SICSA, but it's a bit hard given that this isn't, strictly speaking, research: http://www.sicsa.ac.uk/funding/

[Adam Kurkiewicz]

I don't think any of the clients we normally work with would care enough to fund this type of work either.

[Adam Kurkiewicz]

I realise that Leo has very different priorities, and I actually think this is entirely justifiable.

[Adam Kurkiewicz]

Another idea, which comes to mind is Google Summer of Code, but this is a lot of work, lean would have to become an affiliated partner, etc.

[Adam Kurkiewicz]

I don't think I'd be able to commit to such a big task as coordinating GSoC.

[Patrick Massot]

I don't think GSoC would be interested in helping packaging, and actual contributions to Lean are far beyond the scope of GSoC

[Adam Kurkiewicz]

The thing is, I'm pretty sure, if we get all the pipelines with all the installers nicely polished, swapping the binary from Lean 3 to Lean 4 would be no problem at all.

[Adam Kurkiewicz]

True.

[Adam Kurkiewicz]

Well, anyway, let's keep thinking about these options, maybe somebody will get a good idea for a funding stream.

[Patrick Massot]

There are also intermediate goals that should be reachable, like having Travis building mathlib nightly olean, copying what works for lean nightlies

[Adam Kurkiewicz]

Marcell's done plenty of travis builds, both before and after we've started working together.

[Adam Kurkiewicz]

There's this website, which lists some possibilities: https://www.software.ac.uk/how-fund-research-software-development

[Adam Kurkiewicz]

I'll investigate and let you guys know what I've found