[ fix ] Address some proofs of void via impossible from issues #2250 … #994
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Idris2 and External Libs | |
| on: | |
| push: | |
| branches: | |
| - '*' | |
| tags: | |
| - '*' | |
| paths-ignore: | |
| - 'docs/**' | |
| - 'icons/**' | |
| - 'Release/**' | |
| - '**.md' | |
| - 'CONTRIBUTORS' | |
| - 'LICENSE' | |
| - 'CHANGELOG.md' | |
| - '.github/workflows/ci-bootstrap.yml' | |
| - '.github/workflows/ci-lint.yml' | |
| - '.github/workflows/ci-sphinx.yml' | |
| - '.github/workflows/ci-super-linter.yml' | |
| pull_request: | |
| branches: | |
| - main | |
| paths-ignore: | |
| - 'docs/**' | |
| - 'icons/**' | |
| - 'Release/**' | |
| - '**.md' | |
| - 'CONTRIBUTORS' | |
| - 'LICENSE' | |
| - '.github/workflows/ci-bootstrap.yml' | |
| - '.github/workflows/ci-lint.yml' | |
| - '.github/workflows/ci-sphinx.yml' | |
| - '.github/workflows/ci-super-linter.yml' | |
| concurrency: | |
| group: ${{ github.ref }} | |
| cancel-in-progress: true | |
| env: | |
| # We aim to keep newest Idris commits buildable by as early of a | |
| # previous version as possible. In reality, we bump this regularly | |
| # to allow us to use new compiler/library features in the compiler | |
| # codebase, but an admirable longterm goal is to support building the | |
| # current version of the compiler with a previous version that is older | |
| # than its immediate predecessor. | |
| IDRIS2_MINIMUM_COMPAT_VERSION: 0.7.0 | |
| jobs: | |
| initialise: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout Project | |
| uses: actions/checkout@v4 | |
| with: | |
| # for pull_request so we can do HEAD^2 | |
| fetch-depth: 2 | |
| - name: Get commit message | |
| id: get_commit_message | |
| run: | | |
| if [[ '${{ github.event_name }}' == 'push' ]]; then | |
| echo "commit_message=$(git log --format=%B -n 1 HEAD | tr '\n' ' ')" >> "$GITHUB_OUTPUT" | |
| elif [[ '${{ github.event_name }}' == 'pull_request' ]]; then | |
| echo "commit_message=$(git log --format=%B -n 1 HEAD^2 | tr '\n' ' ')" >> "$GITHUB_OUTPUT" | |
| fi | |
| outputs: | |
| commit_message: | |
| echo "${{ steps.get_commit_message.outputs.commit_message }}" | |
| ###################################################################### | |
| # Build from the previous version | |
| # We perform this check before all the other ones because: | |
| # 1. It is fast | |
| # 2. If it fails then there is no point in trying the rest | |
| ###################################################################### | |
| quick-check: | |
| needs: initialise | |
| runs-on: ubuntu-latest | |
| if: | | |
| !contains(needs.initialise.outputs.commit_message, '[ci: skip]') | |
| env: | |
| IDRIS2_CG: chez | |
| SCHEME: scheme | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Install build dependencies | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y chezscheme | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| # Get our hands on the released version either by using the cache | |
| # or by rebuilding it if necessary. | |
| - name: Cache Chez Previous Version | |
| id: previous-version-cache | |
| uses: actions/cache@v4 | |
| with: | |
| path: Idris2-${{ env.IDRIS2_MINIMUM_COMPAT_VERSION }} | |
| key: ${{ runner.os }}-idris2-bootstrapped-chez-${{ env.IDRIS2_MINIMUM_COMPAT_VERSION }} | |
| - name : Build previous version | |
| if: steps.previous-version-cache.outputs.cache-hit != 'true' | |
| run: | | |
| wget "https://github.com/idris-lang/Idris2/archive/refs/tags/v$IDRIS2_MINIMUM_COMPAT_VERSION.tar.gz" -O "idris2-$IDRIS2_MINIMUM_COMPAT_VERSION.tgz" | |
| tar zxvf "idris2-$IDRIS2_MINIMUM_COMPAT_VERSION.tgz" | |
| cd "Idris2-$IDRIS2_MINIMUM_COMPAT_VERSION" | |
| make bootstrap | |
| cd .. | |
| - name: Install previous version | |
| run: | | |
| cd "Idris2-$IDRIS2_MINIMUM_COMPAT_VERSION" | |
| make install | |
| cd .. | |
| # Build the current version and save the installation. | |
| - name: Build current version | |
| run: | | |
| make && make install | |
| - name: Artifact Idris2 from previous version | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| include-hidden-files: true | |
| name: ubuntu-installed-idris2-${{ env.IDRIS2_MINIMUM_COMPAT_VERSION }}-chez | |
| path: ~/.idris2/ | |
| ###################################################################### | |
| # Bootstrapping builds | |
| ###################################################################### | |
| # CHEZ | |
| ubuntu-bootstrap-chez: | |
| needs: [initialise, quick-check] | |
| runs-on: ubuntu-latest | |
| if: | | |
| !contains(needs.initialise.outputs.commit_message, '[ci:') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: ubuntu]') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: chez]') | |
| env: | |
| IDRIS2_CG: chez | |
| SCHEME: scheme | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Install build dependencies | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y chezscheme | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| - name: Make bootstrap folder readonly | |
| run: chmod -R a-w bootstrap | |
| - name: Build from bootstrap | |
| run: make bootstrap && make install | |
| - name: Artifact Bootstrapped Idris2 | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| include-hidden-files: true | |
| name: ubuntu-installed-bootstrapped-idris2-chez | |
| path: ~/.idris2/ | |
| macos-bootstrap-chez: | |
| needs: [initialise, quick-check] | |
| runs-on: macos-latest | |
| if: | | |
| !contains(needs.initialise.outputs.commit_message, '[ci:') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: macos]') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: chez]') | |
| env: | |
| SCHEME: chez | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Install build dependencies | |
| run: | | |
| brew update | |
| brew install --overwrite [email protected] | |
| brew install node | |
| brew install chezscheme | |
| brew install coreutils | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| - name: Make bootstrap folder readonly | |
| run: chmod -R a-w bootstrap | |
| - name: Build Idris 2 from bootstrap | |
| run: make bootstrap && make install | |
| shell: bash | |
| - name: Artifact Bootstrapped Idris2 | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| include-hidden-files: true | |
| name: macos-installed-bootstrapped-idris2-chez | |
| path: ~/.idris2/ | |
| windows-bootstrap-chez: | |
| needs: [initialise, quick-check] | |
| runs-on: windows-latest | |
| if: | | |
| !contains(needs.initialise.outputs.commit_message, '[ci:') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: windows]') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: chez]') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: racket]') | |
| env: | |
| MSYSTEM: MINGW64 | |
| MSYS2_PATH_TYPE: inherit | |
| SCHEME: scheme | |
| CC: gcc | |
| steps: | |
| - name: Init | |
| run: | | |
| git config --global core.autocrlf false | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Get Chez Scheme | |
| run: | | |
| git clone --depth 1 --branch v9.5.8a https://github.com/cisco/ChezScheme | |
| c:\msys64\usr\bin\bash -l -c "pacman -S --noconfirm tar make mingw-w64-x86_64-gcc" | |
| echo "PWD=$(c:\msys64\usr\bin\cygpath -u $(pwd))" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append | |
| - name: Configure and Build Chez Scheme | |
| run: | | |
| c:\msys64\usr\bin\bash -l -c "cd $env:PWD && cd ChezScheme && ./configure --threads && make" | |
| - name: Set Path | |
| run: | | |
| $chez="$(pwd)\ChezScheme\ta6nt\bin\ta6nt" | |
| $idris="$(pwd)\.idris2" | |
| echo "$chez" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append | |
| echo "$idris\bin" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append | |
| echo "IDRIS_PREFIX=$idris" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append | |
| echo "PREFIX=$(c:\msys64\usr\bin\cygpath -u $idris)" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append | |
| - name: Test Scheme | |
| run: | | |
| scheme --version | |
| - name: Bootstrap | |
| run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make bootstrap" | |
| - name: Bootstrap test | |
| run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make ci-windows-bootstrap-test" | |
| - name: Install | |
| run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make install" | |
| - name: Artifact Idris2 from chez | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| include-hidden-files: true | |
| name: windows-installed-bootstrapped-idris2-chez | |
| path: ${{ env.IDRIS_PREFIX }} | |
| nix-bootstrap-chez: | |
| needs: [initialise, quick-check] | |
| runs-on: ubuntu-latest | |
| if: | | |
| (!contains(needs.initialise.outputs.commit_message, '[ci:') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: nix]') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: chez]')) | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - uses: cachix/install-nix-action@v18 | |
| - name: Test with nix | |
| env: | |
| NIX_CONFIG: "experimental-features = nix-command flakes" | |
| run: nix build .#checks.x86_64-linux.idris2Tests -L | |
| # RACKET | |
| ubuntu-bootstrap-racket: | |
| needs: [initialise, quick-check] | |
| runs-on: ubuntu-latest | |
| if: | | |
| !contains(needs.initialise.outputs.commit_message, '[ci:') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: ubuntu]') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: racket]') | |
| env: | |
| IDRIS2_CG: racket | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Install build dependencies | |
| run: | | |
| sudo apt-get install -y racket | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| - name: Make bootstrap folder readonly | |
| run: chmod -R a-w bootstrap | |
| - name: Build from bootstrap | |
| run: make bootstrap-racket && make install | |
| - name: Artifact Bootstrapped Idris2 | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| include-hidden-files: true | |
| name: ubuntu-installed-bootstrapped-idris2-racket | |
| path: ~/.idris2/ | |
| ###################################################################### | |
| # Self-hosting builds and testing | |
| ###################################################################### | |
| # CHEZ | |
| ubuntu-self-host-chez: | |
| needs: ubuntu-bootstrap-chez | |
| runs-on: ubuntu-latest | |
| env: | |
| IDRIS2_CG: chez | |
| SCHEME: scheme | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Download Idris2 Artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ubuntu-installed-bootstrapped-idris2-chez | |
| path: ~/.idris2/ | |
| - name: Install build dependencies | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y chezscheme | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"* | |
| - name: Build self-hosted | |
| run: make all IDRIS2_BOOT="idris2 -Werror" && make install | |
| - name: Test self-hosted | |
| run: make ci-ubuntu-test INTERACTIVE='' | |
| macos-self-host-chez: | |
| needs: macos-bootstrap-chez | |
| runs-on: macos-latest | |
| env: | |
| SCHEME: chez | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Download Idris2 Artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: macos-installed-bootstrapped-idris2-chez | |
| path: ~/.idris2/ | |
| - name: Install build dependencies | |
| run: | | |
| brew update | |
| brew install --overwrite [email protected] | |
| brew install chezscheme | |
| brew install node | |
| brew install coreutils | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"* | |
| - name: Build self-hosted | |
| run: make all IDRIS2_BOOT="idris2 -Werror" && make install | |
| shell: bash | |
| - name: Test self-hosted | |
| run: make ci-macos-test INTERACTIVE='' | |
| shell: bash | |
| # RACKET | |
| ubuntu-self-host-racket: | |
| needs: ubuntu-bootstrap-racket | |
| runs-on: ubuntu-latest | |
| if: false | |
| env: | |
| IDRIS2_CG: racket | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Download Idris2 Artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ubuntu-installed-bootstrapped-idris2-racket | |
| path: ~/.idris2/ | |
| - name: Install build dependencies | |
| run: | | |
| sudo apt-get install -y racket | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"* | |
| - name: Build self-hosted | |
| run: make all IDRIS2_BOOT="idris2 -Werror" && make install | |
| - name: Test self-hosted | |
| run: make ci-ubuntu-test INTERACTIVE='' | |
| ubuntu-self-host-previous-version: | |
| needs: [initialise, quick-check] | |
| runs-on: ubuntu-latest | |
| if: | | |
| !contains(needs.initialise.outputs.commit_message, '[ci:') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: ubuntu]') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: libs]') | |
| env: | |
| IDRIS2_CG: chez | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Download Idris2 Artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ubuntu-installed-idris2-${{ env.IDRIS2_MINIMUM_COMPAT_VERSION }}-chez | |
| path: ~/.idris2/ | |
| - name: Install build dependencies | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y chezscheme | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"* | |
| - name: Build self-hosted from previous version | |
| run: make all IDRIS2_BOOT="idris2 -Werror" && make install | |
| - name: Test self-hosted from previous version | |
| run: make ci-ubuntu-test INTERACTIVE='' | |
| - name: Artifact Idris2 | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| include-hidden-files: true | |
| name: idris2-nightly-chez | |
| path: ~/.idris2/ | |
| windows-self-host-racket: | |
| needs: [initialise, windows-bootstrap-chez] | |
| runs-on: windows-latest | |
| if: | | |
| !contains(needs.initialise.outputs.commit_message, '[ci:') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: windows]') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: racket]') | |
| env: | |
| IDRIS2_CG: racket | |
| MSYSTEM: MINGW64 | |
| MSYS2_PATH_TYPE: inherit | |
| CC: gcc | |
| RACKET_RACO: raco | |
| steps: | |
| - name: Init | |
| run: | | |
| git config --global core.autocrlf false | |
| echo "PWD=$(c:\msys64\usr\bin\cygpath -u $(pwd))" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Get Chez Scheme | |
| run: | | |
| git clone --depth 1 --branch v9.5.8a https://github.com/cisco/ChezScheme | |
| c:\msys64\usr\bin\bash -l -c "pacman -S --noconfirm tar make mingw-w64-x86_64-gcc" | |
| echo "PWD=$(c:\msys64\usr\bin\cygpath -u $(pwd))" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append | |
| - name: Configure and Build Chez Scheme | |
| run: | | |
| c:\msys64\usr\bin\bash -l -c "cd $env:PWD && cd ChezScheme && ./configure --threads && make" | |
| - name: Set Path | |
| run: | | |
| $chez="$(pwd)\ChezScheme\ta6nt\bin\ta6nt" | |
| $idris="$(pwd)\.idris2" | |
| echo "$chez" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append | |
| echo "$idris\bin" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append | |
| echo "IDRIS_PREFIX=$idris" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append | |
| echo "PREFIX=$(c:\msys64\usr\bin\cygpath -u $idris)" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append | |
| - name: Download Idris2 Artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: windows-installed-bootstrapped-idris2-chez | |
| path: ${{ env.IDRIS_PREFIX }} | |
| - name: Install build dependencies | |
| uses: Bogdanp/[email protected] | |
| with: | |
| variant: 'CS' | |
| version: 'stable' | |
| distribution: 'full' | |
| - name: Self host | |
| run: | | |
| c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make" | |
| # TODO: fix the broken tests! | |
| # - name: Test | |
| # run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make ci-windows-test" | |
| - name: Install | |
| run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make install" | |
| ###################################################################### | |
| # Ubuntu API | |
| ###################################################################### | |
| ubuntu-build-api: | |
| needs: ubuntu-bootstrap-chez | |
| runs-on: ubuntu-latest | |
| env: | |
| IDRIS2_CG: chez | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Download Idris2 Artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ubuntu-installed-bootstrapped-idris2-chez | |
| path: ~/.idris2/ | |
| - name: Install build dependencies | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y chezscheme | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"* | |
| - name: Build API | |
| run: make install-api | |
| shell: bash | |
| - name: Test API | |
| run: cd tests/idris2/api/api001 && ./run "$HOME/.idris2/bin/idris2" | |
| shell: bash | |
| ###################################################################### | |
| # Testing some libraries on Ubuntu and pack. | |
| # | |
| # We are particularly interested in libraries that are heavily using | |
| # dependent types, that are prone to find bugs and regressions in the | |
| # compiler. | |
| ###################################################################### | |
| ###################################################################### | |
| # Test that we can build Collie | |
| ###################################################################### | |
| ub-test-collie: | |
| needs: [initialise, ubuntu-self-host-previous-version] | |
| runs-on: ubuntu-latest | |
| if: | | |
| !contains(needs.initialise.outputs.commit_message, '[ci:') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: libs]') | |
| env: | |
| IDRIS2_CG: chez | |
| steps: | |
| - name: Download Idris2 Artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: idris2-nightly-chez | |
| path: ~/.idris2/ | |
| - name: Install build dependencies | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y chezscheme | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"* | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: 'ohad/collie' | |
| - name: Build Collie | |
| run: | | |
| make | |
| ######################################################################## | |
| # Test that we can build Frex | |
| ######################################################################## | |
| ub-test-frex: | |
| needs: [initialise, ubuntu-self-host-previous-version] | |
| runs-on: ubuntu-latest | |
| if: | | |
| !contains(needs.initialise.outputs.commit_message, '[ci:') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: libs]') | |
| env: | |
| IDRIS2_CG: chez | |
| steps: | |
| - name: Download Idris2 Artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: idris2-nightly-chez | |
| path: ~/.idris2/ | |
| - name: Install build dependencies | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y chezscheme | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"* | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: 'frex-project/idris-frex' | |
| - name: Build Frex | |
| run: | | |
| make | |
| make test | |
| ###################################################################### | |
| # Test that we can build Stefan Höck's elab-util and pack | |
| ###################################################################### | |
| # ELAB-UTIL | |
| ub-test-elab-util: | |
| needs: [initialise, ubuntu-self-host-previous-version] | |
| runs-on: ubuntu-latest | |
| if: | | |
| !contains(needs.initialise.outputs.commit_message, '[ci:') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: libs]') | |
| env: | |
| IDRIS2_CG: chez | |
| steps: | |
| - name: Download Idris2 Artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: idris2-nightly-chez | |
| path: ~/.idris2/ | |
| - name: Install build dependencies | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y chezscheme | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"* | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: 'stefan-hoeck/idris2-elab-util' | |
| - name: Build idris2-elab-util | |
| run: | | |
| make all | |
| # PACK | |
| # | |
| # N.B. instead of bootstrapping pack, we use the dockerimage where it is | |
| # already, and then use pack to rebuild pack with this job's idris2 sources | |
| ub-pack-test-pack: | |
| needs: [initialise, ubuntu-self-host-previous-version] | |
| runs-on: ubuntu-latest | |
| if: | | |
| !contains(needs.initialise.outputs.commit_message, '[ci:') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: libs]') | |
| env: | |
| IDRIS2_CG: chez | |
| PACK_DIR: /root/.pack | |
| strategy: | |
| fail-fast: false | |
| # N.B.: | |
| container: ghcr.io/stefan-hoeck/idris2-pack:latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: 'stefan-hoeck/idris2-pack' | |
| # by default, pack uses the main idris2 head, not the current job's one | |
| - name: Toml setup | |
| run: | | |
| { echo "[idris2]" | |
| echo "url = \"https://github.com/${GITHUB_REPOSITORY}\"" | |
| echo "commit = \"latest:${GITHUB_REF_NAME}\"" | |
| echo "bootstrap = true" | |
| } > pack.toml | |
| - name: Build idris2-pack | |
| run: | | |
| git config --global --add safe.directory "${PWD}" | |
| # only fetch to a new branch if we're not on main (otherwise, git complains) | |
| if [[ $(git branch --show-current) != 'main' ]] | |
| then git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}" | |
| else git pull origin main | |
| fi | |
| # rebuild pack with the fetched Idris2 | |
| pack install pack | |
| ###################################################################### | |
| # Test that we can build the LSP | |
| ###################################################################### | |
| ub-pack-test-lsp: | |
| needs: [initialise, ubuntu-self-host-previous-version] | |
| runs-on: ubuntu-latest | |
| if: | | |
| !contains(needs.initialise.outputs.commit_message, '[ci:') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: libs]') | |
| env: | |
| IDRIS2_CG: chez | |
| PACK_DIR: /root/.pack | |
| # LSP is vastly easier to build using pack, so do that | |
| container: ghcr.io/stefan-hoeck/idris2-pack:latest | |
| strategy: | |
| fail-fast: false | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: 'idris-community/idris2-lsp' | |
| - name: Toml setup | |
| run: | | |
| { echo "[idris2]" | |
| echo "url = \"https://github.com/${GITHUB_REPOSITORY}\"" | |
| echo "commit = \"latest:${GITHUB_REF_NAME}\"" | |
| echo "bootstrap = true" | |
| } > pack.toml | |
| # make sure pack is running the PR's Idris2 before building LSP | |
| - name: Build pack with PR-Idris | |
| run: | | |
| git config --global --add safe.directory "${PWD}" | |
| # only fetch to a new branch if we're not on main (otherwise, git complains) | |
| if [[ $(git branch --show-current) != 'main' ]] | |
| then git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}" | |
| else git pull origin main | |
| fi | |
| pack install pack | |
| - name: Build+install idris2-lsp | |
| run: | | |
| pack --no-prompt install-app idris2-lsp | |
| ###################################################################### | |
| # Test that we can use Katla to build html doc of the libs | |
| ###################################################################### | |
| ub-test-katla-and-html: | |
| needs: [initialise, ubuntu-self-host-previous-version] | |
| runs-on: ubuntu-latest | |
| if: | | |
| !contains(needs.initialise.outputs.commit_message, '[ci:') | |
| || contains(needs.initialise.outputs.commit_message, '[ci: html]') | |
| env: | |
| IDRIS2_CG: chez | |
| steps: | |
| - name: Initialise DEPLOY variable | |
| run: | | |
| if [[ '${{ github.ref }}' == 'refs/heads/main' ]]; then | |
| echo "IDRIS2_DEPLOY=true" >> "$GITHUB_ENV" | |
| fi | |
| - name: Download Idris2 Artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: idris2-nightly-chez | |
| path: ~/.idris2/ | |
| - name: Install build dependencies | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y chezscheme markdown | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"* | |
| - name: Checkout idris2 | |
| uses: actions/checkout@v4 | |
| - name: Build API | |
| run: make install-api | |
| shell: bash | |
| - name: Checkout collie | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: 'ohad/collie' | |
| - name: Build and install Collie | |
| run: | | |
| make install | |
| - name: Checkout idrall | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: 'alexhumphreys/idrall' | |
| - name: Build and install idrall | |
| run: | | |
| make install | |
| - name: Checkout katla | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: 'idris-community/katla' | |
| - name: Build and install katla | |
| run: | | |
| make | |
| mkdir -p "${HOME}"/.local/bin/ | |
| cp -r build/exec/* "${HOME}"/.local/bin/ | |
| echo "${HOME}/.local/bin" >> "$GITHUB_PATH" | |
| - name: Checkout idris2 | |
| uses: actions/checkout@v4 | |
| - name: Build html doc & landing page | |
| run: | | |
| make -C libs/prelude/ install docs IDRIS2=idris2 | |
| make -C libs/base/ install docs IDRIS2=idris2 | |
| make -C libs/contrib/ install docs IDRIS2=idris2 | |
| make -C libs/network/ install docs IDRIS2=idris2 | |
| make -C libs/linear/ install docs IDRIS2=idris2 | |
| make -C libs/test/ install docs IDRIS2=idris2 | |
| make -C libs/papers/ install docs IDRIS2=idris2 | |
| cd .github/scripts | |
| ./katla.sh | |
| cd - | |
| cd www/ | |
| ./katla.sh | |
| cd - | |
| cp -r www/html/* .github/scripts/html/ | |
| cp www/source/idris-logo-base.png .github/scripts/html/ | |
| - name: Deploy HTML | |
| uses: JamesIves/[email protected] | |
| if: ${{ success() && env.IDRIS2_DEPLOY }} | |
| with: | |
| branch: gh-pages | |
| folder: .github/scripts/html/ | |
| git-config-name: Github Actions |