[Draft] Deeper integration with Agda: foundational work #109
This file contains hidden or 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
| # modified from https://github.com/simonmichael/hledger/blob/master/.github/workflows/linux.yml | |
| name: CI | |
| defaults: | |
| run: | |
| shell: bash | |
| on: | |
| push: | |
| branches: [master, ci-*, ci, dev] | |
| tags: | |
| - 'v*' # Push events to matching v*, i.e. v1.0, v20.15.10 | |
| pull_request: | |
| branches: [master] | |
| jobs: | |
| build-and-test: | |
| name: Build and Test | |
| runs-on: ${{ matrix.os }} | |
| strategy: | |
| matrix: | |
| os: [windows-latest, ubuntu-latest, macos-latest, macos-13] | |
| agda: ['Agda-2.8.0', 'Agda-2.7.0.1', 'Agda-2.6.4.3'] | |
| fail-fast: false | |
| steps: | |
| - name: 📥 Checkout repository | |
| uses: actions/checkout@v4 | |
| - name: 📤 Install yq (Windows) | |
| if: runner.os == 'Windows' | |
| uses: frenck/action-setup-yq@v1 | |
| - name: 🎛️ Determine which version of Agda to target | |
| run: | | |
| STACK_YAML=$(echo stack-9.10.2-${{ matrix.agda }}.yaml) | |
| STACK_YAML_ARG="--stack-yaml $(echo stack-9.10.2-${{ matrix.agda }}.yaml)" | |
| # Determine artifact naming based on branch/tag | |
| if [[ "${{ github.ref }}" == "refs/heads/dev" ]]; then | |
| PREFIX="als-dev" | |
| else | |
| PREFIX="als" | |
| fi | |
| if [[ ${{ matrix.os }} == "ubuntu-latest" ]]; then | |
| ARTEFACT="$PREFIX-${{ matrix.agda }}-ubuntu" | |
| fi | |
| if [[ ${{ matrix.os }} == "macos-latest" ]]; then | |
| ARTEFACT="$PREFIX-${{ matrix.agda }}-macos-arm64" | |
| fi | |
| if [[ ${{ matrix.os }} == "macos-13" ]]; then | |
| ARTEFACT="$PREFIX-${{ matrix.agda }}-macos-x64" | |
| fi | |
| if [[ ${{ matrix.os }} == "windows-latest" ]]; then | |
| ARTEFACT="$PREFIX-${{ matrix.agda }}-windows" | |
| fi | |
| echo STACK_YAML_ARG="${STACK_YAML_ARG}" >> "${GITHUB_ENV}" | |
| echo STACK_YAML="${STACK_YAML}" >> "${GITHUB_ENV}" | |
| echo ARTEFACT="${ARTEFACT}" >> "${GITHUB_ENV}" | |
| - name: 🎛️ Determine Stack resolver & GHC version | |
| run: | | |
| STACK_RESOLVER=$(yq .resolver $STACK_YAML) | |
| GHC_VERSION=$(echo $(yq .compiler $STACK_YAML) | cut -c 5-) | |
| echo STACK_RESOLVER="${STACK_RESOLVER}" >> "${GITHUB_ENV}" | |
| echo GHC_VERSION="${GHC_VERSION}" >> "${GITHUB_ENV}" | |
| - name: 💾 Cache Haskell toolchain | |
| if: runner.os == 'macOS' | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ~/.ghcup | |
| ~/.stack/programs | |
| ~/.stack/pantry | |
| key: ${{ runner.os }}-${{ runner.arch }}-haskell-${{ env.GHC_VERSION }}-stack-latest | |
| restore-keys: | | |
| ${{ runner.os }}-${{ runner.arch }}-haskell-${{ env.GHC_VERSION }}- | |
| ${{ runner.os }}-${{ runner.arch }}-haskell- | |
| - name: 🏗 Setup Haskell | |
| if : runner.os == 'macOS' | |
| uses: haskell-actions/setup@v2 | |
| id: setup-haskell | |
| with: | |
| ghc-version: ${{ env.GHC_VERSION }} | |
| enable-stack: true | |
| stack-version: 'latest' | |
| - name: 🎛️ Determine Stack root | |
| run: | | |
| STACK_ROOT="$(stack path $STACK_YAML_ARG --stack-root)" | |
| echo STACK_ROOT="${STACK_ROOT}" >> "${GITHUB_ENV}" | |
| - name: 🔍 Review all variables | |
| run: | | |
| echo "STACK_YAML = ${STACK_YAML}" | |
| echo "STACK_YAML_ARG = ${STACK_YAML_ARG}" | |
| echo "STACK_RESOLVER = ${STACK_RESOLVER}" | |
| echo "ARTEFACT = ${ARTEFACT}" | |
| echo "GHC_VERSION = ${GHC_VERSION}" | |
| echo "STACK_ROOT = ${STACK_ROOT}" | |
| # things to be restored: | |
| # Include STACK_RESOLVER in cache key, otherwise caches accumulate build products for different resolvers. | |
| - name: 💾 Restore cached stack global package db | |
| id: stack-global | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: ${{ env.STACK_ROOT }} | |
| key: ${{ matrix.os }}-stack-resolver-${{ env.STACK_RESOLVER }}-global-${{ hashFiles('**.yaml') }}-${{ matrix.agda }} | |
| restore-keys: | | |
| ${{ matrix.os }}-stack-resolver-${{ env.STACK_RESOLVER }}-global | |
| - name: 💾 Restore cached .stack-work | |
| id: stack-work | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: .stack-work | |
| key: ${{ matrix.os }}-stack-resolver-${{ env.STACK_RESOLVER }}-work-${{ hashFiles('**.yaml') }}-${{ matrix.agda }} | |
| restore-keys: | | |
| ${{ matrix.os }}-stack-resolver-${{ env.STACK_RESOLVER }}-work | |
| # actions: | |
| - name: ⚙️ Set PKG_CONFIG_PATH for the ICU library (on macOS) | |
| if: runner.os == 'macOS' | |
| run: | | |
| echo PKG_CONFIG_PATH="$(brew --prefix)/opt/icu4c/lib/pkgconfig" >> "${GITHUB_ENV}" | |
| - name: 📥 Install the icu library (on Windows) | |
| if: runner.os == 'Windows' | |
| run: | | |
| stack exec $STACK_YAML_ARG -- pacman -S --noconfirm mingw-w64-x86_64-icu mingw-w64-x86_64-pkgconf | |
| - name: 📸 Build Snapshot | |
| run: stack build $STACK_YAML_ARG --no-terminal --only-snapshot -j1 | |
| - name: 🏗️ Build Dependencies | |
| run: stack build $STACK_YAML_ARG --no-terminal --only-dependencies | |
| - name: 🏗️ Build ALS | |
| run: stack build $STACK_YAML_ARG | |
| - name: 🏗️ Build Testings | |
| run: stack build $STACK_YAML_ARG --test --no-terminal --only-dependencies | |
| # things to be cached | |
| - name: 💾 Cache stack global package db | |
| if: always() && steps.stack-global.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@v4 | |
| with: | |
| path: ${{ env.STACK_ROOT }} | |
| key: ${{ steps.stack-global.outputs.cache-primary-key }} | |
| - name: 💾 Cache .stack-work | |
| if: always() && steps.stack-work.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@v4 | |
| with: | |
| path: .stack-work | |
| key: ${{ steps.stack-work.outputs.cache-primary-key }} | |
| - name: 📦 Bundle executable, DLLs and data files (on macOS) | |
| if: runner.os == 'macOS' | |
| run: | # Bundle icu4c DLLs | |
| # see if icu4c has been installed | |
| if [ "$(brew list | grep icu4c)" = "" ] | |
| then | |
| echo "installing icu4c" | |
| brew install icu4c | |
| fi | |
| # get the directory of the DDLs we want (icuuc, icui18n, icudata) | |
| dylib_dir=$(dirname "$(brew list icu4c | grep icuuc.dylib)") | |
| echo "dylib_dir: $dylib_dir" | |
| # find the path of "als" | |
| executable=$(find "$(stack path $STACK_YAML_ARG --local-install-root)"/bin -name "als") | |
| echo "executable: $executable" | |
| # remove the old dylib, and make a new one | |
| rm -rf dylib | |
| mkdir dylib | |
| ################################################################################ | |
| # icuuc | |
| ################################################################################ | |
| icuuc_id=$(otool -L "$executable" | grep icuuc | awk '{print $1}') | |
| icuuc_id_basename=$(basename "$icuuc_id") | |
| icuuc_path=$dylib_dir/$icuuc_id_basename | |
| icuuc_path_new=dylib/$icuuc_id_basename | |
| icuuc_id_new=@loader_path/dylib/$icuuc_id_basename | |
| # copy icuuc to the new directory | |
| cp "$icuuc_path" "$icuuc_path_new" | |
| # change icuuc's ID referenced by ALS | |
| install_name_tool -change "$icuuc_id" "$icuuc_id_new" "$executable" | |
| echo "icuuc referenced by ALS" | |
| echo " old ID : $icuuc_id" | |
| echo " new ID : $icuuc_id_new" | |
| echo " old path: $icuuc_path" | |
| echo " new path: $icuuc_path_new" | |
| ################################################################################ | |
| # icui18n | |
| ################################################################################ | |
| icui18n_id=$(otool -L "$executable" | grep icui18n | awk '{print $1}') | |
| icui18n_id_basename=$(basename "$icui18n_id") | |
| icui18n_path=$dylib_dir/$icui18n_id_basename | |
| icui18n_path_new=dylib/$icui18n_id_basename | |
| icui18n_id_new=@loader_path/dylib/$icui18n_id_basename | |
| # copy icui18n to the new directory | |
| cp "$icui18n_path" "$icui18n_path_new" | |
| # change icui18n's ID referenced by ALS | |
| install_name_tool -change "$icui18n_id" "$icui18n_id_new" "$executable" | |
| echo "icui18n referenced by ALS" | |
| echo " old ID : $icui18n_id" | |
| echo " new ID : $icui18n_id_new" | |
| echo " old path: $icui18n_path" | |
| echo " new path: $icui18n_path_new" | |
| ################################################################################ | |
| # icudata | |
| ################################################################################ | |
| # otool -L "$icui18n_id" | grep icudata | awk '{print $1}' | |
| icudata_id=$(otool -L "$icuuc_path" | grep icudata | awk '{print $1}') | |
| icudata_id_basename=$(basename "$icudata_id") | |
| icudata_path=$dylib_dir/$icudata_id_basename | |
| icudata_path_new=dylib/$icudata_id_basename | |
| # copy icudata to the new directory | |
| cp "$icudata_path" "$icudata_path_new" | |
| # no need of changing the ID because supposely it's already of "@loader_path" | |
| echo "icudata referenced by icuuc" | |
| echo " old ID : $icudata_id" | |
| echo " old path : $icudata_path" | |
| echo " new path : $icudata_path_new" | |
| - name: 📦 Bundle executable, DLLs and data files (on Linux and macOS) | |
| if: runner.os != 'Windows' | |
| id: zip | |
| run: | | |
| # locate the data-dir | |
| datadir=$(find "$(stack path $STACK_YAML_ARG --snapshot-install-root)/share" -type d -name "Agda-*") | |
| echo "datadir: $datadir" | |
| # locate the executable | |
| executable=$(find "$(stack path $STACK_YAML_ARG --local-install-root)/bin" -name "als") | |
| echo "executable: $executable" | |
| # make a temporary directory for compresssing | |
| mkdir zip | |
| cp -r "$datadir" zip/data | |
| if [[ ${{ runner.os }} == "macOS" ]]; then | |
| cp -r dylib zip/dylib | |
| fi | |
| cp "$executable" zip/ | |
| # compress | |
| cd zip | |
| zip -r $ARTEFACT.zip ./* | |
| cd .. | |
| mv zip/$ARTEFACT.zip . | |
| - name: 📦 Bundle executable, DLLs and data files (on Windows) | |
| if: runner.os == 'Windows' | |
| shell: pwsh | |
| run: | | |
| # locate the data-dir | |
| $snapshot = (stack path $STACK_YAML_ARG --snapshot-install-root) | |
| $datadir = (ls $snapshot\share *Agda-* -Recurse -Directory).FullName | |
| # locate the executable | |
| $local = (stack path $STACK_YAML_ARG --local-install-root) | |
| $executable = (ls $local\bin *als.exe* -Recurse -File).FullName | |
| # make a temporary directory for compresssing | |
| mkdir zip | |
| cp -r $datadir zip/data | |
| cp $executable zip/ | |
| # include text-icu DLLs | |
| $mingw64bin = (stack path $STACK_YAML_ARG --extra-library-dirs).split(", ") -match "\\bin" | |
| cp (ls $mingw64bin *libicudt*) zip/ | |
| cp (ls $mingw64bin *libicuin*) zip/ | |
| cp (ls $mingw64bin *libicuuc*) zip/ | |
| ls zip | |
| # compress | |
| cd zip | |
| Compress-Archive * "$($env:ARTEFACT).zip" | |
| cd .. | |
| mv zip/"$($env:ARTEFACT).zip" . | |
| - name: 🧪 Run tests | |
| run: stack test $STACK_YAML_ARG | |
| - name: 📤 Upload build artifact | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: ${{ env.ARTEFACT }} | |
| path: ${{ env.ARTEFACT }}.zip | |
| retention-days: 1 | |
| build-wasm: | |
| name: Build WASM | |
| if: github.ref == 'refs/heads/dev' || github.ref == 'refs/heads/ci' | |
| runs-on: ubuntu-22.04 | |
| env: | |
| GHC_WASM_META_FLAVOUR: '9.10' | |
| GHC_WASM_META_COMMIT_HASH: 'c3f44696d29aaeadd755d69c51735954bfcd59db' | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| path: als | |
| submodules: true | |
| - name: Compute cache key | |
| run: echo "CI_CACHE_KEY=${{ runner.os }}-${{ runner.arch }}-${{ env.GHC_WASM_META_COMMIT_HASH }}-flavor-${{ env.GHC_WASM_META_FLAVOUR }}" >> "$GITHUB_ENV" | |
| - name: Try to restore cached .ghc-wasm | |
| id: ghc-wasm-cache-restore | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: ~/.ghc-wasm | |
| key: ghc-wasm-${{ env.CI_CACHE_KEY }} | |
| restore-keys: | | |
| ghc-wasm-${{ runner.os }}-${{ runner.arch }}- | |
| - name: Try to restore cached native cabal | |
| id: native-cabal-cache-restore | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: | | |
| ~/.config/cabal | |
| ~/.cache/cabal | |
| key: native-cabal-${{ env.CI_CACHE_KEY }} | |
| restore-keys: | | |
| native-cabal-${{ runner.os }}-${{ runner.arch }}- | |
| - name: Try to restore cached dist-newstyle | |
| id: dist-newstyle-cache-restore | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: als/dist-newstyle | |
| key: dist-newstyle-${{ env.CI_CACHE_KEY }} | |
| restore-keys: | | |
| dist-newstyle-${{ runner.os }}-${{ runner.arch }}- | |
| - name: Clone and setup ghc-wasm-meta | |
| id: ghc-wasm-setup | |
| if: steps.ghc-wasm-cache-restore.outputs.cache-matched-key == '' | |
| run: | | |
| mkdir ghc-wasm-meta | |
| cd ghc-wasm-meta | |
| git config --global init.defaultBranch dontcare | |
| git config --global advice.detachedHead false | |
| git init | |
| git remote add origin https://gitlab.haskell.org/haskell-wasm/ghc-wasm-meta.git | |
| git fetch origin ${{ env.GHC_WASM_META_COMMIT_HASH }} --depth=1 | |
| git checkout FETCH_HEAD | |
| FLAVOUR=${{ env.GHC_WASM_META_FLAVOUR }} ./setup.sh | |
| - name: Add ghc-wasm-meta to PATH | |
| run: ~/.ghc-wasm/add_to_github_path.sh | |
| - name: Update wasm32 cabal | |
| if: steps.ghc-wasm-setup.outcome == 'success' || steps.ghc-wasm-setup.outcome == 'skipped' | |
| run: wasm32-wasi-cabal update | |
| - name: Install native utilities | |
| run: | | |
| echo ">>> Update cabal" | |
| ~/.ghc-wasm/cabal/bin/cabal update | |
| echo ">>> Install alex and happy" | |
| ~/.ghc-wasm/cabal/bin/cabal install alex-3.5.0.0 happy-1.20.1.1 | |
| - name: Cabal configure | |
| working-directory: './als' | |
| run: | | |
| mv cabal.project.wasm32 cabal.project | |
| wasm32-wasi-cabal configure --flag=Agda-2-8-0 | |
| - name: Build Agda as dependency | |
| id: build-dep-agda | |
| working-directory: './als' | |
| run: wasm32-wasi-cabal build lib:agda | |
| - name: Cache dist-newstyle | |
| uses: actions/cache/save@v4 | |
| if: steps.build-dep-agda.outcome == 'success' | |
| with: | |
| path: als/dist-newstyle | |
| key: dist-newstyle-${{ env.CI_CACHE_KEY }} | |
| - name: Build dependencies other than Agda | |
| working-directory: './als' | |
| run: | | |
| # Setup network submodule autotools | |
| cd wasm-submodules/network | |
| autoreconf -i | |
| cd ../.. | |
| # Build all dependencies (cabal git deps + network submodule) | |
| wasm32-wasi-cabal build --dependencies-only | |
| - name: Build als | |
| working-directory: './als' | |
| run: | | |
| mkdir ~/out | |
| wasm32-wasi-cabal build | |
| WASM_BINARY_PATH=$(wasm32-wasi-cabal list-bin als) | |
| WASM_BINARY_NAME=$(basename "$WASM_BINARY_PATH") | |
| cp "$WASM_BINARY_PATH" ~/out | |
| echo "WASM_BINARY_NAME=$WASM_BINARY_NAME" >> $GITHUB_ENV | |
| - name: Clean up native/wasm cabal logs | |
| run: rm -rf ~/.cache/cabal/logs ~/.ghc-wasm/.cabal/logs | |
| - name: Cache native cabal | |
| uses: actions/cache/save@v4 | |
| if: steps.ghc-wasm-setup.outcome == 'success' | |
| with: | |
| path: | | |
| ~/.config/cabal | |
| ~/.cache/cabal | |
| key: ${{ steps.native-cabal-cache-restore.outputs.cache-primary-key }} | |
| - name: Cache ghc-wasm-meta | |
| uses: actions/cache/save@v4 | |
| if: steps.ghc-wasm-setup.outcome == 'success' | |
| with: | |
| path: ~/.ghc-wasm | |
| key: ${{ steps.ghc-wasm-cache-restore.outputs.cache-primary-key }} | |
| - name: 📤 Upload WASM artifact | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: als-dev-wasm | |
| path: ~/out/${{ env.WASM_BINARY_NAME }} | |
| retention-days: 1 | |
| create-release: | |
| name: Create Release | |
| needs: [build-and-test, build-wasm] | |
| if: always() && !cancelled() && !contains(needs.*.result, 'failure') && (startsWith(github.ref, 'refs/tags/v') || github.ref == 'refs/heads/dev' || github.ref == 'refs/heads/ci') | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: 📥 Checkout repository | |
| uses: actions/checkout@v4 | |
| - name: 🏭 Create Stable Release | |
| if: startsWith(github.ref, 'refs/tags/v') | |
| run: | | |
| gh release create ${{ github.ref_name }} --generate-notes | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - name: 🚢 Create/Update Dev Release | |
| if: github.ref == 'refs/heads/dev' || github.ref == 'refs/heads/ci' | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| # Delete existing dev release if it exists | |
| gh release delete dev --cleanup-tag -y || true | |
| # Wait for GitHub to process the deletion to avoid race condition | |
| # that causes releases to be created as drafts | |
| # See: https://github.com/cli/cli/issues/8458 | |
| sleep 5 | |
| # Create new dev pre-release | |
| gh release create dev \ | |
| --title "Development Release (dev)" \ | |
| --notes "Development pre-release build from latest changes. This is a pre-release for testing purposes." \ | |
| --prerelease | |
| upload-stable-release: | |
| name: Upload to Stable Release | |
| needs: create-release | |
| if: startsWith(github.ref, 'refs/tags/v') | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: 📥 Download all artifacts | |
| uses: actions/download-artifact@v4 | |
| with: | |
| path: artifacts | |
| - name: 🚢 Upload artifacts to release | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| cd artifacts | |
| for dir in */; do | |
| artifact_name="${dir%/}" | |
| echo "Uploading ${artifact_name}..." | |
| if [ -f "${artifact_name}/${artifact_name}.zip" ]; then | |
| gh release upload ${{ github.ref_name }} "${artifact_name}/${artifact_name}.zip" --clobber --repo ${{ github.repository }} | |
| else | |
| echo "Warning: No .zip file found in ${artifact_name}" | |
| fi | |
| done | |
| upload-dev-release: | |
| name: Upload to Dev Release | |
| needs: create-release | |
| if: github.ref == 'refs/heads/dev' || github.ref == 'refs/heads/ci' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: 📥 Download all artifacts | |
| uses: actions/download-artifact@v4 | |
| with: | |
| path: artifacts | |
| - name: 🚢 Upload artifacts to dev release | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| cd artifacts | |
| # Upload only Agda-2.8.0 artifacts and WASM | |
| for dir in *Agda-2.8.0* als-dev-wasm; do | |
| if [ -d "$dir" ]; then | |
| artifact_name="$dir" | |
| echo "Uploading ${artifact_name}..." | |
| if [ -f "${artifact_name}/${artifact_name}.zip" ]; then | |
| gh release upload dev "${artifact_name}/${artifact_name}.zip" --clobber --repo ${{ github.repository }} | |
| elif [ "$artifact_name" = "als-dev-wasm" ]; then | |
| # Find the WASM binary (filename may vary) | |
| wasm_file=$(find "${artifact_name}" -type f -name "als*" | head -1) | |
| if [ -n "$wasm_file" ]; then | |
| gh release upload dev "$wasm_file" --clobber --repo ${{ github.repository }} | |
| else | |
| echo "Warning: WASM binary not found in ${artifact_name}" | |
| fi | |
| fi | |
| fi | |
| done |