Server host for lean4web and loogle?

Stream: general

[Joseph Tooby-Smith]

I'm looking to set up lean4web and loogle for physlean.

Does anyone have any recommendations of what hosting services to use and what sort of configurations I would need? I've experimented a bit with DigitalOcean, and tried to follow the instructions here for lean4web, but ran into memory problems on the npm run build step.

If anyone knows of any detailed steps for setting up these online with a project downstream of mathlib that would also be very helpful!

[Shreyas Srinivas]

Hetzner is good https://www.hetzner.com/

[Shreyas Srinivas]

In general you can find a lot of good options here

https://european-alternatives.eu/product/hetzner

[Joachim Breitner]

Have you used nix/nixos or have someone to help you that does? The live instance is described by a nix flake, and I could put the interesting bits into a public nix module for easy reuse (but was hoping to not have to give generic nixos training and support)

[Joachim Breitner]

Started dumping the setup we use (stripped of parts not related to lean4web) here:
https://github.com/nomeata/lean-live-nix
Ah, you also want loogle. Shouldn’t have deleted that then :-)

[Joachim Breitner]

Ok, if you sign up for https://garnix.io/ and clone this repository, then you should get a running instance on
https://live-garnix.master.lean-live-nix.<your-github-username>.garnix.me/ without further steps. It will take 40mins or so to download the mathlib caches.
If you want a different hostname you can use CNAMES to point to that.
Not sure how to adjust the size of these garnix machines. But of course the nixos setup works elsewhere as well, the garnix is just a (maybe too) convenient way of deploying and hosting this stuff.

If you can it's maybe easier to use a more conventional way of hosting to get started (i.e. get a hetzner machine, install nixos, run .deploy .#live)

To adjust which repos are hosted you’d have to fork https://github.com/kha/lean4web, but in principle the relevant information could be in this repository as well.

For those willing to try out garnix to host something like this, maybe join the discussion at https://discord.com/channels/960235377506025542/960235378030301216/1346929006007554079

[Joseph Tooby-Smith]

Thank you so much for taking the time to write this out and do this @Joachim Breitner ! I'm going to go through it all properly later this week, and have a go at seeing if I can get it to work.

[Joseph Tooby-Smith]

Ok, I managed to get a version of lean4web up and running for physlean :):
live.physlean.com

I ended up following the steps I've outlined here.
This is likely to be a first pass at this, but it's something I could get working.

Thanks for your help @Joachim Breitner !

[Jon Eugster]

If you wanted to PR any instructions to the doc at lean4web - formal or informal - to help others in the future, that would be be very much appreciated :)

[Joseph Tooby-Smith]

@Jon Eugster I will try and write something up next week for this :smile: .

[Joseph Tooby-Smith]

I have also managed to get loogle working, so you can search Physlean for physics related terms e.g. Higgs.

I modified the home page loogle.physlean.com, to make it clear that this is not the mathlib version of it etc. I am happy to change any messaging there to what every people feel is appropriate