`npm run production` vs `npm start`

[lecopivo]

I'm trying out lean4web locally before setting up the server and I got struck on the PORT=8080 npm run production step, getting Waiting for Lean server to start.... The simple trick is to run npm start instead.

I do not understand any of the technology behind this so I'm just copy pasting commands. It might be worth updating the instructions for dummies like me.

[joneugster]

Indeed, seems like the instructions for setting up the server in production mode could need an update, they've never got really polished in any way!

npm start runs everything in development mode. Notably it does not use any bubblewrap container.

I'll try to update the instructions next time I'm setting up a setup somewhere, but if you have notes of your attempts, feel free to push them or add them here. Or ask for help directly :)

[nnarek]

I also have same issue
bug is inside lean4web/server/bubblewrap.sh
it says Lean Server: bwrap: Can't chdir to /tmp/lean4web/Projects/MathlibDemo/: No such file or directory while such directory exists

[abentkamp]

Could you try to put the lean4web repo somewhere other than /tmp? For example somewhere in /home?

[nnarek]

yes, it works when lean4web is inside other dir. but behavior is strange.
Thank you