Skip to content

hosting.md

Latest commit

 

History

History
126 lines (92 loc) · 4.26 KB

hosting.md

File metadata and controls

126 lines (92 loc) · 4.26 KB
Raw

Example for hosting Lean4Game yourself

These instructions aim to give you an exemplary manual on how to host your lean4game instance such that others can access it via the internet. This manual will assume that you already have a running Linux server that uses the apt package manager. (The steps are analogous for other Linux distributions and their package managers.)

Download Dependencies

We will use nginx for our server, but any other web server might be applied here. The same logic applies to pm2 as our choice for process management tool.

  1. Install a nginx web server as reverse proxy
   sudo apt update
   sudo apt install nginx
  1. install npm for building JavaScript projects
  curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
  source ~/.bashrc
  nvm install node npm
  1. install pm2 to manage processes on the server
   sudo npm install pm2 -g
  1. install tsc to compile TypeScript projects on the server
   sudo npm install typescript -g
  1. Install bubblewrap for secure execution of lean server
  sudo apt-get install bubblewrap
  1. install elan to manage versions of the Lean4 programming language and theorem prover
   curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

This will install the current version of elan with a default installation of lean and the lake package manager.

  1. Conclude elan installation by configuring your current shell to it
   source $HOME/.elan/env

Setup Reverse Proxy

The next step is to set up a reverse proxy with nginx and to add information concerning domain and SSL certification. As those considerations are quite individual, technical and safety critical, we refer to general instructions on how to set up a reverse proxy using nginx on Ubuntu.

Setting up Lean4Game

This section will be somewhat similar to what is written in the section about running Lean4Game locally. We diverge here in that we only describe the installation of Lean4Game itself. Before starting, you will need to generate a fine-grained GitHub access token with the following properties:

  • Expiration: choose "Custom" and select a day up to 365 days from today. (Note that you will need to update the token after a year)
  • Repository access: Public repositories (read-only)
  • No further permissions. It should say "0 permissions for none of your repositories" and "0 account permissions"

Save the access token after its generation as you can only see it once, and it is needed for step 3.

  1. Clone hosted projects via git onto server. Important: Please use the HTTPS URL from GitHub, not the SSH URL, to clone the project repositories.
   git clone https://github.com/leanprover-community/lean4game.git
  1. Install lean4game dependencies via npm
   cd lean4game
   npm install
  1. Set lean4game environment variables in ecosystem.config.cjs file. The github access token should have been generated and saved as described in the beginning of this section.
// This is a configuration file for pm2, a production process manager for nodejs
module.exports = {
  apps : [{
    name   : "lean4game",
    script : "relay/dist/src/index.js",
    env: {
      LEAN4GAME_GITHUB_USER: "<to-be-requested-from-admin>",
      LEAN4GAME_GITHUB_TOKEN: "<to-be-requested-from-admin>",
      RESERVED_DISC_SPACE_MB: <RESERVED_SPACE>,
      ISSUE_CONTACT: "<contact_link>",
      NODE_ENV: "production",
      PORT: <PORT>,
      API_PORT: <API_PORT>,
    },
  }]
}
  1. Build lean4game project via npm
   npm run build
  1. Start Lean4Game through PM2
   pm2 start ecosystem.config.cjs

Having done that you should now be able to access your hosted Lean4Game instance via the domain that has been specified during the setup of the nginx server. For more information on how to maintain your established server, please refer to the server maintenance documentation.