Fix instance resolution of _≤ᵉ_, and left-over renamings from #900a1 #766
Workflow file for this run
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: Formal Ledger Specs | |
| on: [push] | |
| permissions: | |
| contents: write | |
| jobs: | |
| build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - run: | | |
| sudo apt-get update | |
| - name: Free disk space | |
| uses: jlumbroso/free-disk-space@main | |
| with: | |
| android: true | |
| dotnet: true | |
| haskell: false | |
| large-packages: false | |
| docker-images: true | |
| swap-storage: true | |
| - uses: actions/checkout@v3 | |
| - uses: cachix/install-nix-action@v20 | |
| with: | |
| nix_path: nixpkgs=channel:nixos-unstable | |
| extra_nix_config: | | |
| trusted-public-keys = hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= | |
| substituters = https://cache.nixos.org/ | |
| - name: Restore store | |
| id: cache-store-restore | |
| uses: actions/cache/restore@v3 | |
| with: | |
| path: | | |
| store | |
| derivations | |
| key: cache-store-${{ runner.os }}-${{github.run_id}} | |
| restore-keys: | | |
| cache-store-${{ runner.os }} | |
| - name: Import cached nix store | |
| continue-on-error: true | |
| run: | | |
| if [[ -f store ]]; then | |
| du -sh store || true | |
| nix-store --import < store | |
| else | |
| echo "No cached store found" | |
| fi | |
| # We have to build this explicitly, in order to cache it, | |
| # since it's not part of the static binary formalLedger closure | |
| - name: Build agda | |
| id: agda | |
| run: | | |
| v=$(nix-build -A agdaWithStdLibMeta) | |
| closure=$(nix-store --query --requisites --include-outputs $v | tr '\n' ' ') | |
| echo "derivation=$v" >> $GITHUB_OUTPUT | |
| echo "closure=$closure" >> $GITHUB_OUTPUT | |
| - name: Build formalLedger | |
| id: formalLedger | |
| run: | | |
| v=$(nix-build -A formalLedger) | |
| closure=$(nix-store --query --requisites --include-outputs $v | tr '\n' ' ') | |
| echo "derivation=$v" >> $GITHUB_OUTPUT | |
| echo "closure=$closure" >> $GITHUB_OUTPUT | |
| - name: Build ledger | |
| id: ledger | |
| run: | | |
| mkdir -p outputs | |
| v=$(nix-build -A ledger -j1 -o outputs/ledger| tr '\n' ' ') | |
| closure=$(nix-store --query --requisites --include-outputs $v | tr '\n' ' ') | |
| echo "derivation=$v" >> $GITHUB_OUTPUT | |
| echo "closure=$closure" >> $GITHUB_OUTPUT | |
| - name: Build midnight | |
| id: midnight | |
| run: | | |
| v=$(nix-build -A midnight -j1 -o outputs/midnight | tr '\n' ' ') | |
| closure=$(nix-store --query --requisites --include-outputs $v | tr '\n' ' ') | |
| echo "derivation=$v" >> $GITHUB_OUTPUT | |
| echo "closure=$closure" >> $GITHUB_OUTPUT | |
| - name: Export all derivations | |
| id: export-derivations | |
| run: | | |
| hashes="${{steps.agda.outputs.derivation}}-${{steps.formalLedger.outputs.derivation}}-${{steps.ledger.outputs.derivation}}-${{steps.midnight.outputs.derivation}}" | |
| closures="${{steps.agda.outputs.closure}} ${{steps.formalLedger.outputs.closure}} ${{ steps.ledger.outputs.closure}} ${{steps.midnight.outputs.closure}}" | |
| touch derivations | |
| updated=false | |
| # export only if the hashes changed or the store does not exist for some reason | |
| if grep -qe "^$hashes" derivations && [[ -f store ]] | |
| then | |
| echo "No need to re-export the store" | |
| else | |
| nix-store --export $closures > store | |
| echo "Exported store of size: $(du -sh store)" | |
| echo "$hashes" > derivations | |
| echo "Wrote new derivations hashes: $(cat derivations)" | |
| updated=true | |
| fi | |
| echo "updated=$updated" >> $GITHUB_OUTPUT | |
| - name: Upload nix store | |
| id: cache-derivations-save | |
| uses: actions/cache/save@v3 | |
| if: steps.export-derivations.outputs.updated == 'true' | |
| with: | |
| path: | | |
| store | |
| derivations | |
| key: cache-store-${{ runner.os }}-${{github.run_id}} | |
| - name: Prepare pdf files to be deployed to site | |
| if: github.ref == 'refs/heads/master' | |
| run: | | |
| mkdir -p pdfs | |
| for f in $(find -L outputs -name '*.pdf'); do | |
| cp -L --force $f pdfs | |
| done | |
| - name: Prepare html docs to be deployed to site | |
| if: github.ref =='refs/heads/master' | |
| id: html | |
| run: | | |
| mkdir -p html | |
| cp -L -r outputs/ledger/html html/ledger | |
| cp -L -r outputs/midnight/html html/midnight | |
| ledger=$(nix eval -f default.nix "ledger.name") | |
| midnight=$(nix eval -f default.nix "midnight.name") | |
| echo "ledger=$ledger" >> $GITHUB_OUTPUT | |
| echo "midnight=$midnight" >> $GITHUB_OUTPUT | |
| - name: Build static file | |
| if: github.ref == 'refs/heads/master' | |
| run: | | |
| ledger="${{steps.html.outputs.ledger}}.PDF.html" | |
| midnight="${{steps.html.outputs.midnight}}.PDF.html" | |
| touch index.html | |
| cat > index.html << EOF | |
| <!DOCTYPE html> | |
| <html> | |
| <body> | |
| <h3>Formal ledger specs</h3> | |
| <ul> | |
| EOF | |
| for f in pdfs/*.pdf; do | |
| echo "<li><a href="$f">$(basename $f)</a></li>" >> index.html | |
| done | |
| echo "<li><a href="html/ledger/${ledger}">${ledger}</a></li>" >> index.html | |
| echo "<li><a href="html/midnight/${midnight}">${midnight}</a></li>" >> index.html | |
| cat >> index.html << EOF | |
| </ul> | |
| </body> | |
| </html> | |
| EOF | |
| - name: Add files | |
| if: github.ref == 'refs/heads/master' | |
| run: | | |
| git config user.name 'github-actions[bot]' | |
| git config user.email 'github-actions[bot]@users.noreply.github.com' | |
| git add index.html | |
| git add pdfs | |
| git add html | |
| git commit -m "Updated for ${{ github.sha }}" | |
| - name: Push to gh-pages | |
| if: github.ref == 'refs/heads/master' | |
| uses: ad-m/[email protected] | |
| with: | |
| github_token: ${{ secrets.GITHUB_TOKEN }} | |
| branch: gh-pages | |
| force: true | |
| directory: . |