mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-24 15:07:37 +03:00
[ ci ] use katla to build html doc of the libs (#2422)
This commit is contained in:
G. Allais
GitHub
parent
98b1062772
commit
2287fd9edb
30
.github/scripts/katla.sh
vendored
Executable file
30
.github/scripts/katla.sh
vendored
Executable file
@ -0,0 +1,30 @@
|
||||
#!/bin/sh
|
||||
|
||||
prefix="../../libs"
|
||||
|
||||
find "$prefix" -name "*.idr" >tmp
|
||||
while IFS= read -r rawfile; do
|
||||
file=$(echo "$rawfile" | sed "s|\.\./\.\./libs/\(.*\)|\1|")
|
||||
libname=$(echo "$file" | sed "s|\([^/]*\)/.*|\1|")
|
||||
filename=$(echo "$file" | sed "s|[^/]*/\(.*\)\.idr|\1|")
|
||||
modulename=$(echo "$filename" | sed "s|/|.|g")
|
||||
htmldir="html/${libname}/source/"
|
||||
htmlfile="${htmldir}/${modulename}.html"
|
||||
mkdir -p "$htmldir"
|
||||
katla html "$rawfile" "${prefix}/${libname}/build/ttc/${filename}.ttm" >"$htmlfile"
|
||||
sed -i "s|<head>|<head><title>${modulename}</title>|" "$htmlfile"
|
||||
done <tmp
|
||||
rm tmp
|
||||
|
||||
find "$prefix"/* -maxdepth 0 -type d >tmp
|
||||
while IFS= read -r libdirectory; do
|
||||
libname=$(echo "$libdirectory" | sed "s|$prefix/||")
|
||||
cp -r "$prefix"/"$libname"/build/docs/* html/"$libname"
|
||||
find html/"$libname"/docs/ -name "*.html" >tmp2
|
||||
while IFS= read -r file; do
|
||||
filename=$(basename "$file" ".html")
|
||||
sed -i "s|<h1>${filename}</h1>|<h1>${filename}<span style=\"float:right\">(<a href=\"../source/${filename}.html\">source</a>)</span></h1>|" "$file"
|
||||
done <tmp2
|
||||
rm tmp2
|
||||
done <tmp
|
||||
rm tmp
|
||||
89
.github/workflows/ci-idris2.yml
vendored
89
.github/workflows/ci-idris2.yml
vendored
@ -251,10 +251,9 @@ jobs:
|
||||
needs: quick-check
|
||||
runs-on: ubuntu-latest
|
||||
if: |
|
||||
false
|
||||
&& (!contains(needs.initialise.outputs.commit_message, '[ci:')
|
||||
!contains(needs.initialise.outputs.commit_message, '[ci:')
|
||||
|| contains(needs.initialise.outputs.commit_message, '[ci: ubuntu]')
|
||||
|| contains(needs.initialise.outputs.commit_message, '[ci: racket]'))
|
||||
|| contains(needs.initialise.outputs.commit_message, '[ci: racket]')
|
||||
|
||||
env:
|
||||
IDRIS2_CG: racket
|
||||
@ -574,3 +573,87 @@ jobs:
|
||||
- name: Build idris2-elab-util
|
||||
run: |
|
||||
make all
|
||||
|
||||
######################################################################
|
||||
# Ubuntu using katla to build html doc of the libs
|
||||
######################################################################
|
||||
|
||||
ubuntu-katla:
|
||||
needs: ubuntu-test-collie
|
||||
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@v2
|
||||
with:
|
||||
name: idris2-nightly-chez
|
||||
path: ~/.idris2/
|
||||
- name: Install build dependencies
|
||||
run: |
|
||||
echo "deb http://security.ubuntu.com/ubuntu hirsute universe" | sudo tee -a /etc/apt/sources.list
|
||||
sudo apt-get update
|
||||
sudo apt-get install -y -t hirsute chezscheme
|
||||
echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
|
||||
chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
|
||||
- name: Checkout idris2
|
||||
uses: actions/checkout@v2
|
||||
- name: Build API
|
||||
run: make install-api
|
||||
shell: bash
|
||||
- name: Checkout collie
|
||||
uses: actions/checkout@v2
|
||||
with:
|
||||
repository: 'ohad/collie'
|
||||
- name: Build and install Collie
|
||||
run: |
|
||||
make install
|
||||
- name: Checkout idrall
|
||||
uses: actions/checkout@v2
|
||||
with:
|
||||
repository: 'alexhumphreys/idrall'
|
||||
- name: Build and install idrall
|
||||
run: |
|
||||
make install
|
||||
- name: Checkout katla
|
||||
uses: actions/checkout@v2
|
||||
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@v2
|
||||
- name: Build html doc
|
||||
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
|
||||
- name: Deploy HTML
|
||||
uses: JamesIves/github-pages-deploy-action@4.1.3
|
||||
if: ${{ success() && env.IDRIS2_DEPLOY }}
|
||||
|
||||
with:
|
||||
branch: gh-pages
|
||||
folder: .github/scripts/html/
|
||||
git-config-name: Github Actions
|
||||
|
||||
@ -3,4 +3,6 @@ version = 0.5.1
|
||||
|
||||
opts = "--ignore-missing-ipkg"
|
||||
|
||||
depends = contrib
|
||||
|
||||
modules = Test.Golden
|
||||
|
||||
Loading…
Reference in New Issue
Block a user