Skip to content

Commit

Permalink
Merge branch 'release-v0.5.1'
Browse files Browse the repository at this point in the history
* release-v0.5.1:
  Bump version and update changelog
  Update documentation
  Use fetch-depth: 0
  Rebase but do not force push
  Do not rebase when deploying with mike
  Do not deploy docs for main, deploy tags as latest
  Use mike to deploy versioned docs
  Bring the diagram in front of the snippet in zoom
  Replace the custom svg hook with a plugin on PyPI
  Update appearance, fix versions in docs
  Drop Tiryoh/actions-mkdocs
  Fix logging in generate_svgs.py
  Fix mkdocs.yml
  Update mkdocs.yml workflow and dependencies
  Switch to Material theme for MkDocs
  Fix links to *.rzk.md in mkdocs.yml
  Fix generate_svgs.py to work on macOS
  Fix computation for Unit
  • Loading branch information
fizruk committed Jun 29, 2023
2 parents fb6eda1 + fee57f0 commit aede460
Show file tree
Hide file tree
Showing 44 changed files with 435 additions and 2,491 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/binaries.yml
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ jobs:
tar -cavf program.tar.gz *
shell: bash

- name: Upload assets
- name: 🚀 Upload assets
id: upload-release-asset
uses: actions/upload-release-asset@v1
env:
Expand Down
9 changes: 5 additions & 4 deletions .github/workflows/ghcjs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -63,23 +63,24 @@ jobs:
mkdir -p dist/result/bin
cp -r ${{ env.store }}$(realpath result)/bin/try-rzk.jsexe/ dist/result/bin/.
chmod -R +w dist/
cp try-rzk/playground.html dist/.
cp try-rzk/index.html dist/.
- name: "📘 Publish JS \"binaries\" (${{ github.ref_name }})"
- name: "🚀 Publish JS \"binaries\" (${{ github.ref_name }})"
if: ${{ github.ref_name != 'main' && github.event_name == 'push' }}
uses: JamesIves/github-pages-deploy-action@v4
with:
token: ${{ secrets.GITHUB_TOKEN }}
folder: dist
target-folder: ${{ github.ref_name }}
target-folder: ${{ github.ref_name }}/playground
clean: false
single-commit: true

- name: "📘 Publish JS \"binaries\""
- name: "🚀 Publish JS \"binaries\""
if: ${{ github.ref_name == 'main' && github.event_name == 'push' }}
uses: JamesIves/github-pages-deploy-action@v4
with:
token: ${{ secrets.GITHUB_TOKEN }}
folder: dist
target-folder: playground
clean: false
single-commit: true
2 changes: 1 addition & 1 deletion .github/workflows/haddock.yml
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ jobs:
mkdir -p dist/haddock
mv $(stack path --local-doc-root)/* dist/haddock
- name: 📘 Publish Haddock Documentation
- name: 🚀 Publish Haddock Documentation
uses: JamesIves/github-pages-deploy-action@v4
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
Expand Down
57 changes: 29 additions & 28 deletions .github/workflows/mkdocs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ name: Build and Deploy MkDocs to GitHub Pages

on:
push:
branches: [ main, develop ]
branches: [ develop ]
tags: [ v* ]
paths:
- .github/workflows/mkdocs.yml
Expand All @@ -16,40 +16,41 @@ jobs:
steps:
- name: 📥 Checkout repository
uses: actions/checkout@v3
with:
fetch-depth: 0

- name: 🧰 Set up Python
uses: actions/setup-python@v4
with:
python-version: '3.9'
cache: 'pip' # caching pip dependencies

- name: 🔨 Install rzk proof assistant
uses: jaxxstorm/[email protected]
with:
repo: fizruk/rzk
tag: latest # FIXME: should use the version from the same Git commit
rename-to: rzk
chmod: 0755

- name: 🔨 Build MkDocs
uses: Tiryoh/actions-mkdocs@v0
with:
mkdocs_version: 'latest' # option
#mkdocs_version: '1.1' # option
requirements: 'docs/requirements.txt' # option
configfile: 'docs/mkdocs.yml' # option
- name: 🔨 Install Pygments lexer for rzk
run: pip install rzk/RzkLexer

- name: 🔨 Install MkDocs Material and mike
run: pip install -r docs/requirements.txt

- name: 🔨 Copy MkDocs files
- name: ⚙️ Configure Git user
run: |
mkdir -p dist/ && cp -r docs/root/* docs/site dist/.
git config --local user.email "github-actions[bot]@users.noreply.github.com"
git config --local user.name "github-actions[bot]"
- name: 🚀 Deploy with mike (${{ github.ref_name }}, latest)
if: ${{ github.ref_name != 'develop' }}
run: |
mike deploy --rebase --push --config-file docs/mkdocs.yml ${{ github.ref_name }} latest
- name: 🚀 Deploy with mike (${{ github.ref_name }})
if: ${{ github.ref_name == 'develop' }}
run: |
mike deploy --rebase --push --config-file docs/mkdocs.yml ${{ github.ref_name }}
- name: 📘 Publish Generated MkDocs (${{ github.ref_name }})
if: ${{ github.ref_name != 'main' }}
uses: JamesIves/github-pages-deploy-action@v4
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
folder: dist
target-folder: ${{ github.ref_name }}
clean: false
single-commit: true

- name: 📘 Publish Generated MkDocs
if: ${{ github.ref_name == 'main' }}
uses: JamesIves/github-pages-deploy-action@v4
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
folder: dist
clean: false
single-commit: true
108 changes: 0 additions & 108 deletions docs/custom_theme/css/gruvbox-light.css

This file was deleted.

10 changes: 0 additions & 10 deletions docs/custom_theme/css/highlightjs-11.7.0.min.css

This file was deleted.

53 changes: 0 additions & 53 deletions docs/custom_theme/css/highlightjs-copy.css

This file was deleted.

Loading

0 comments on commit aede460

Please sign in to comment.