diff --git a/.gitea/workflows/deploy-lean.yml b/.gitea/workflows/deploy-lean.yml deleted file mode 100644 index 349d405..0000000 --- a/.gitea/workflows/deploy-lean.yml +++ /dev/null @@ -1,53 +0,0 @@ -name: Build and Deploy Lean - -on: - push: - branches: [master] - # This pipeline owns the lean editor image: heavy (it builds lean4web - # with Mathlib), so it runs only when lean/** actually changes - paths: - - "lean/**" - workflow_dispatch: - -jobs: - build: - runs-on: docker - - steps: - - name: Checkout - uses: actions/checkout@v4 - - - name: Install SSH client - run: | - apt-get update -y && apt-get install -y openssh-client - - - name: Setup SSH inside container - run: | - mkdir -p ~/.ssh - echo "${{ secrets.DEPLOY_KEY }}" > ~/.ssh/id_ed25519 - chmod 600 ~/.ssh/id_ed25519 - - # Add the container host to known_hosts - ssh-keyscan -H ${{ secrets.DEPLOY_HOST }} >> ~/.ssh/known_hosts - - - name: Log in to registry - run: | - echo "${{ secrets.REGISTRY_PASSWORD }}" | docker login git.aranroig.com -u "${{ secrets.REGISTRY_USER }}" --password-stdin - - # Multi-stage: compilers/dev deps stay in the builder, the pushed image - # is the slim runtime (toolchain + client + Mathlib cache). Still a - # heavy build and a multi-GB push — expect it to take a while. - # Pin upstream with: docker build --build-arg LEAN4WEB_REF=v0.2.2 ... - - name: Build lean editor server - run: | - docker build -t git.aranroig.com/${{ secrets.REGISTRY_USER }}/mathew-lean:latest ./lean - docker push git.aranroig.com/${{ secrets.REGISTRY_USER }}/mathew-lean:latest - - - name: Deploy - run: | - ssh deploy@${{ secrets.DEPLOY_HOST }} << 'EOF' - echo "${{ secrets.REGISTRY_PASSWORD }}" | docker login git.aranroig.com -u "${{ secrets.REGISTRY_USER }}" --password-stdin - cd /var/www/app/ - docker compose pull lean - docker compose up -d lean - EOF diff --git a/.gitea/workflows/deploy.yml b/.gitea/workflows/deploy.yml index 2d66e74..62c3577 100644 --- a/.gitea/workflows/deploy.yml +++ b/.gitea/workflows/deploy.yml @@ -1,21 +1,64 @@ -name: Build and Deploy Nuxt +name: Build and Deploy on: push: branches: [master] - # The Lean editor carries Mathlib and moves on its own schedule — its - # image is built and pushed by deploy-lean.yml, only when lean/** changes - paths-ignore: - - "lean/**" + workflow_dispatch: jobs: - build: + # One file, two lifecycles. The app pair (frontend + backend) moves with + # most commits; the lean image carries Mathlib and is heavy to build and + # push, so its job runs only when lean/** actually changed. This step reads + # the pushed diff and opens the gates for the jobs below. + changes: runs-on: docker - + + outputs: + app: ${{ steps.filter.outputs.app }} + lean: ${{ steps.filter.outputs.lean }} + steps: - name: Checkout uses: actions/checkout@v4 - + with: + fetch-depth: 0 + + - name: What changed? + id: filter + env: + BEFORE: ${{ github.event.before }} + AFTER: ${{ github.event.after }} + run: | + # Manual runs, first pushes or rewritten history carry no usable + # "before" commit — rebuild everything rather than guess. + if [ -z "${BEFORE}" ] || [ -z "${BEFORE//0/}" ] || ! git cat-file -e "${BEFORE}^{commit}" 2>/dev/null; then + echo "app=yes" >> "$GITHUB_OUTPUT" + echo "lean=yes" >> "$GITHUB_OUTPUT" + echo "app=yes lean=yes (no usable before-commit)" + exit 0 + fi + changed=$(git diff --name-only "$BEFORE" "$AFTER") + lean=no + app=no + if [ -n "$changed" ]; then + if echo "$changed" | grep -q '^lean/'; then lean=yes; fi + if echo "$changed" | grep -qvx 'lean/.*'; then app=yes; fi + fi + echo "app=$app" >> "$GITHUB_OUTPUT" + echo "lean=$lean" >> "$GITHUB_OUTPUT" + echo "app=$app lean=$lean" + + # The wiki app itself. Its deploy (`compose pull && up -d`) also pulls + # whatever mathew-lean:latest the registry holds — the lean job keeps it current. + deploy: + runs-on: docker + needs: changes + if: needs.changes.outputs.app == 'yes' + + steps: + - name: Checkout + uses: actions/checkout@v4 + - name: Install SSH client run: | apt-get update -y && apt-get install -y openssh-client @@ -48,8 +91,6 @@ jobs: scp docker-compose.yml deploy@${{ secrets.DEPLOY_HOST }}:/var/www/app/ scp nginx.conf deploy@${{ secrets.DEPLOY_HOST }}:/var/www/app/nginx.conf - # `compose pull` also pulls the lean image from the registry — - # deploy-lean.yml is what keeps that tag current - name: Deploy run: | ssh deploy@${{ secrets.DEPLOY_HOST }} << 'EOF' @@ -58,3 +99,46 @@ jobs: docker compose pull docker compose up -d --remove-orphans EOF + + # The Lean editor (lean4web): multi-stage, heavy by nature (it fetches + # Mathlib); expect a long build and a multi-GB push. Pin upstream with: + # docker build --build-arg LEAN4WEB_REF=v0.2.2 ... + deploy-lean: + runs-on: docker + needs: changes + if: needs.changes.outputs.lean == 'yes' + + steps: + - name: Checkout + uses: actions/checkout@v4 + + - name: Install SSH client + run: | + apt-get update -y && apt-get install -y openssh-client + + - name: Setup SSH inside container + run: | + mkdir -p ~/.ssh + echo "${{ secrets.DEPLOY_KEY }}" > ~/.ssh/id_ed25519 + chmod 600 ~/.ssh/id_ed25519 + + # Add the container host to known_hosts + ssh-keyscan -H ${{ secrets.DEPLOY_HOST }} >> ~/.ssh/known_hosts + + - name: Log in to registry + run: | + echo "${{ secrets.REGISTRY_PASSWORD }}" | docker login git.aranroig.com -u "${{ secrets.REGISTRY_USER }}" --password-stdin + + - name: Build lean editor server + run: | + docker build -t git.aranroig.com/${{ secrets.REGISTRY_USER }}/mathew-lean:latest ./lean + docker push git.aranroig.com/${{ secrets.REGISTRY_USER }}/mathew-lean:latest + + - name: Deploy + run: | + ssh deploy@${{ secrets.DEPLOY_HOST }} << 'EOF' + echo "${{ secrets.REGISTRY_PASSWORD }}" | docker login git.aranroig.com -u "${{ secrets.REGISTRY_USER }}" --password-stdin + cd /var/www/app/ + docker compose pull lean + docker compose up -d lean + EOF diff --git a/AGENTS.md b/AGENTS.md index bacab8e..f601196 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -64,13 +64,14 @@ its theme (live, same page), and the Goals/Messages pane. `lean/Dockerfile` still builds lean4web (upstream's real Lean + Mathlib per session; `--build-arg LEAN4WEB_REF=` pins it) and runs its websocket server on port 8080; the compose `lean` service runs it (image `git.aranroig.com/syndria98/mathew-lean:latest` — -CI builds and pushes it, and deploys lean, only when `lean/**` changes: `deploy-lean.yml`; -the regular deploy just pulls the tag). Upstream asks for a dedicated machine, so the build -is **multi-stage**: dev tooling stays in the builder, and the pushed image is a slim runtime -of node + elan toolchain + built client + Mathlib's compiled cache (~11GB — the cache is -the bulk; upstream's second demo project `Stable` is dropped, its extra ~3GB toolchain was -unused). `--build-arg BAKE_MATHLIB=false` ships Mathlib *out* of the image (~4GB) into a -`.lake` volume, filled once at first start by `lean/entrypoint.sh` — see lean/README.md. +CI pushes it, and deploys lean, only when `lean/**` changes: `.gitea/workflows/deploy.yml` +gates its `deploy-lean` job on the pushed diff; the app deploy just pulls the tag). Upstream +asks for a dedicated machine, so the build is **multi-stage**: dev tooling stays in the +builder, and the pushed image is a slim runtime of node + elan toolchain + built client + +Mathlib's compiled cache (~11GB — the cache is the bulk; upstream's second demo project +`Stable` is dropped, its extra ~3GB toolchain was unused). `--build-arg BAKE_MATHLIB=false` +ships Mathlib *out* of the image (~4GB) into a `.lake` volume, filled once at first start +by `lean/entrypoint.sh` — see lean/README.md. It runs `NO_BWRAP=true` — bubblewrap cannot nest in a container, so Docker itself is the sandbox; whoever reaches the port can run Lean. Build/run, TLS, security and projects: `lean/README.md`. diff --git a/lean/README.md b/lean/README.md index 89a0aa2..583eb1a 100644 --- a/lean/README.md +++ b/lean/README.md @@ -153,11 +153,11 @@ and its cache re-downloads, so treat this like the heavy build it is (run it on the machine that hosts the editor; pin `LEAN4WEB_REF` for a build that stands still). -CI follows the same split: `.gitea/workflows/deploy-lean.yml` rebuilds, pushes -and redeploys the lean image **only when `lean/**` changes**; the regular -deploy pipeline ignores `lean/**` entirely and just pulls whatever -`mathew-lean:latest` the registry holds. (In volume mode the pushed image is -~4GB and a lean rebuild doesn't fetch Mathlib at all.) +CI follows the same split inside one workflow: `.gitea/workflows/deploy.yml` gates a +`deploy-lean` job on the pushed diff — it rebuilds, pushes and redeploys the lean image +**only when `lean/**` changed** — while the app jobs run on every other change and just +pull whatever `mathew-lean:latest` the registry holds. (In volume mode the pushed image +is ~4GB and a lean rebuild doesn't fetch Mathlib at all.) ## Adding Lean projects