Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[ fix #2086 ] new www deploy strategy #2147

Merged
merged 18 commits into from
Oct 14, 2023
Merged

[ fix #2086 ] new www deploy strategy #2147

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
3849ef3
[ ci ] new www deploy strategy
gallais Oct 12, 2023
13999a7
[ fix ] index.html page
gallais Oct 12, 2023
c2b75b1
[ fix ] reinstate index.agda generation
gallais Oct 12, 2023
9bc74fa
[ fix ] more silly mistakes
gallais Oct 12, 2023
475739f
[ html ] more structure
gallais Oct 12, 2023
a534f6a
[ refactor ] use template file + .sh script
gallais Oct 12, 2023
e11ab71
[ fix ] no need to escape quotes in .html file
gallais Oct 12, 2023
00e877f
[ fix ] missing newline
gallais Oct 12, 2023
e67bb8a
[ fix ] make landing.sh executable
gallais Oct 12, 2023
393ede7
[ fix ] should be ready
gallais Oct 12, 2023
2d0afd7
[ fix ] reverse order sort
gallais Oct 13, 2023
1a942bf
[ cleanup ] More html structure
gallais Oct 13, 2023
dcc5bb3
[ revert ] go back to building everything
gallais Oct 13, 2023
a084ff6
[ cosmetic ] whitespace
gallais Oct 13, 2023
e04f06b
Revert "[ revert ] go back to building everything"
gallais Oct 13, 2023
a09366e
Revert "Revert "[ revert ] go back to building everything""
gallais Oct 13, 2023
f24daec
[ cosmetic ] a bit of CSS & logo
gallais Oct 13, 2023
223c83c
[ fix ] missing agda logo
gallais Oct 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion .github/workflows/ci-ubuntu.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ jobs:
|| '${{ github.base_ref }}' == 'master' ]]; then
# Pick Agda version for master
echo "AGDA_COMMIT=tags/v2.6.4" >> $GITHUB_ENV;
echo "AGDA_HTML_DIR=html" >> $GITHUB_ENV
echo "AGDA_HTML_DIR=html/master" >> $GITHUB_ENV
elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \
|| '${{ github.base_ref }}' == 'experimental' ]]; then
# Pick Agda version for experimental
Expand Down Expand Up @@ -125,6 +125,7 @@ jobs:
run: cabal update

- name: Install alex & happy
if: steps.cache-cabal.outputs.cache-hit != 'true'
run: |
${{ env.CABAL_INSTALL }} alex
${{ env.CABAL_INSTALL }} happy
Expand Down Expand Up @@ -177,6 +178,9 @@ jobs:
rm -f '${{ env.AGDA_HTML_DIR }}'/*.css
${{ env.AGDA }} --html --html-dir ${{ env.AGDA_HTML_DIR }} index.agda

cp travis/* .
./landing.sh

- name: Deploy HTML
uses: JamesIves/[email protected]
if: ${{ success() && env.AGDA_DEPLOY }}
Expand Down
16 changes: 16 additions & 0 deletions travis/agda-logo.svg
View file
Open in desktop
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
4 changes: 4 additions & 0 deletions travis/landing-bottom.html
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
</ul>
</div>
</body>
</html>
24 changes: 24 additions & 0 deletions travis/landing-top.html
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
<html>

<head>
<title>Documention for the Agda standard library</title>
</head>

<body>

<div id="container" style="width:50%;min-width:500px;margin:auto">
<img src="agda-logo.svg" style="width:80px;float:right" />
<h1>Documention for the Agda standard library</h1>

<hr />

<h2>Development versions</h2>

<ul>
<li><a href="master">master</a></li>
<li><a href="experimental">experimental</a></li>
</ul>

<h2>Released versions</h2>

<ul>
17 changes: 17 additions & 0 deletions travis/landing.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
set -eu
set -o pipefail

rm html/index.html

cat landing-top.html >> landing.html

find html/ -name "index.html" \
| grep -v "master\|experimental" \
| sort -r \
| sed 's|html/\([^\/]*\)/index.html| <li><a href="\1">\1</a></li>|g' \
>> landing.html

cat landing-bottom.html >> landing.html

mv landing.html html/index.html
mv agda-logo.svg html/