davidnet/prove2me-mixin:0.1.0

schemaVersion: "3"
displayName: Prove2Me Lean toolchain
description: Lean 4 and cached Mathlib setup for Prove2Me missions
version: 0.1.0
kind: mixin
provides:
    - [email protected]
capabilities:
    - type: com.docker.sandbox/network-policy@1
      config:
        install:
            allow:
                - elan.lean-lang.org:443
                - release.lean-lang.org:443
                - releases.lean-lang.org:443
                - github.com:443
                - raw.githubusercontent.com:443
                - objects.githubusercontent.com:443
                - release-assets.githubusercontent.com:443
                - lakecache.blob.core.windows.net:443
        runtime:
            allow:
                - prove2.me:443
                - github.com:443
                - raw.githubusercontent.com:443
                - objects.githubusercontent.com:443
                - releases.lean-lang.org:443
                - release.lean-lang.org:443
                - release-assets.githubusercontent.com:443
                - lakecache.blob.core.windows.net:443
    - type: com.docker.sandbox/lifecycle@1
      config:
        install:
            - command: bash /usr/local/share/prove2me/bootstrap.sh
              user: "1000"
            - command: |
                for tool in elan lean lake; do
                  if [ ! -e "/usr/local/bin/$tool" ]; then
                    ln -s "/home/agent/.elan/bin/$tool" "/usr/local/bin/$tool"
                  fi
                done
              user: "0"
    - type: com.docker.sandbox/agent-context@1
      config:
        contentFile: /usr/share/sandbox/kit/prove2me-mixin/context.md