Skip to content

Commit

Permalink
Basic infrastructure for the website
Browse files Browse the repository at this point in the history
  • Loading branch information
YaelDillies committed Jul 18, 2024
1 parent 555f869 commit 6e5bf19
Show file tree
Hide file tree
Showing 14 changed files with 709 additions and 147 deletions.
90 changes: 0 additions & 90 deletions .github/workflows/blueprint.yml

This file was deleted.

107 changes: 50 additions & 57 deletions .github/workflows/push.yml
Original file line number Diff line number Diff line change
Expand Up @@ -10,20 +10,19 @@ permissions:
id-token: write

jobs:
# style_lint:
# name: Lint style
# runs-on: ubuntu-latest
# steps:
# # Check for long lines in .lean files and report if any lines exceed 100 characters
# - name: Check for long lines
# if: always()
# run: |
# ! (find Polya -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')

# - name: Don't 'import Mathlib', use precise imports
# if: always()
# run: |
# ! (find Polya -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
style_lint:
name: Lint style
runs-on: ubuntu-latest
steps:
- name: Check for long lines
if: always()
run: |
! (find Polya -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
- name: Don't 'import Mathlib', use precise imports
if: always()
run: |
! (find Polya -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
build_project:
runs-on: ubuntu-latest
Expand All @@ -34,19 +33,27 @@ jobs:
with:
fetch-depth: 0

- name: Install elan
run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
- name: Print files to upstream
run: |
grep -r --files-without-match 'import Polya' Polya | sort > 1.txt
grep -r --files-with-match 'sorry' Polya | sort > 2.txt
mkdir -p docs/_includes
comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/alma-n\/Polya-lean\/blob\/main\/\1)/' > docs/_includes/files_to_upstream.md
rm 1.txt 2.txt
- name: Count sorries
run: python scripts/count_sorry.py

# - name: Update doc-gen4
# run: ~/.elan/bin/lake -R -Kenv=dev update «doc-gen4»
- name: Install elan
run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0

- name: Get cache
run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
run: ~/.elan/bin/lake exe cache get || true

- name: Build project
run: ~/.elan/bin/lake -Kenv=dev build Polya
run: ~/.elan/bin/lake build Polya

- name: Cache mathlib documentation
- name: Cache mathlib docs
uses: actions/cache@v3
with:
path: |
Expand All @@ -56,12 +63,12 @@ jobs:
.lake/build/doc/Std
.lake/build/doc/Mathlib
.lake/build/doc/declarations
!.lake/build/doc/declarations/declaration-data-Polya*
key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
#restore-keys: MathlibDoc-
restore-keys: |
MathlibDoc-
- name: Build project documentation
run: ~/.elan/bin/lake -Kenv=dev build Polya:docs
- name: Build documentation
run: ~/.elan/bin/lake -R -Kenv=dev build Polya:docs

- name: Build blueprint and copy to `docs/blueprint`
uses: xu-cheng/texlive-action@v2
Expand All @@ -73,43 +80,28 @@ jobs:
apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
git config --global --add safe.directory $GITHUB_WORKSPACE
git config --global --add safe.directory `pwd`
python3 -m venv env
source env/bin/activate
pip install --upgrade pip requests wheel
pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
pip install leanblueprint
leanblueprint pdf
mkdir docs
cp blueprint/print/print.pdf docs/blueprint.pdf
leanblueprint web
cp -r blueprint/web docs/blueprint
- name: Check declarations
run: ~/.elan/bin/lake exe checkdecls blueprint/lean_decls

- name: Remove lake files from documentation
run: |
find .lake/build/doc -name "*.trace" -delete
find .lake/build/doc -name "*.hash" -delete
find .lake/build/doc -name "*/header-data.bmp" -delete
python3 -m pip install --upgrade pip requests wheel
python3 -m pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
pip install -r blueprint/requirements.txt
python3 -m pip install invoke
inv all
- name: Copy documentation to `docs/docs`
run: |
sudo chown -R runner docs
cp -r .lake/build/doc docs/docs
mv .lake/build/doc docs/docs
# - name: Bundle dependencies
# uses: ruby/setup-ruby@v1
# with:
# working-directory: docs
# ruby-version: "3.0"
# bundler-cache: true
- name: Bundle dependencies
uses: ruby/setup-ruby@v1
with:
working-directory: docs
ruby-version: "3.0" # Not needed with a .ruby-version file
bundler-cache: true # runs 'bundle install' and caches installed gems automatically

# - name: Bundle website
# working-directory: docs
# run: JEKYLL_ENV=production bundle exec jekyll build
- name: Bundle website
working-directory: docs
run: JEKYLL_ENV=production bundle exec jekyll build

- name: Upload docs & blueprint artifact to `docs`
- name: Upload docs & blueprint artifact
uses: actions/upload-pages-artifact@v1
with:
path: docs/
Expand All @@ -119,4 +111,5 @@ jobs:
uses: actions/deploy-pages@v1

- name: Make sure the cache works
run: mv docs/docs .lake/build/doc
run: |
mv docs/docs .lake/build/doc
2 changes: 2 additions & 0 deletions docs/.bundle/config
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
---
BUNDLE_PATH: "vendor/bundle"
8 changes: 8 additions & 0 deletions docs/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
_site
.sass-cache
.jekyll-cache
.jekyll-metadata
vendor
blueprint/
blueprint.pdf
docs/
25 changes: 25 additions & 0 deletions docs/404.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
---
permalink: /404.html
layout: default
---

<style type="text/css" media="screen">
.container {
margin: 10px auto;
max-width: 600px;
text-align: center;
}
h1 {
margin: 30px 0;
font-size: 4em;
line-height: 1;
letter-spacing: -1px;
}
</style>

<div class="container">
<h1>404</h1>

<p><strong>Page not found :(</strong></p>
<p>The requested page could not be found.</p>
</div>
25 changes: 25 additions & 0 deletions docs/Gemfile
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
source "https://rubygems.org"

# To upgrade, run `bundle update github-pages`.
gem "github-pages", group: :jekyll_plugins
# If you have any plugins, put them here!
group :jekyll_plugins do
#gem "jekyll-feed", "~> 0.12"
end

# Windows and JRuby does not include zoneinfo files, so bundle the tzinfo-data gem
# and associated library.
platforms :mingw, :x64_mingw, :mswin, :jruby do
gem "tzinfo", "~> 1.2"
gem "tzinfo-data"
end

# Performance-booster for watching directories on Windows.
gem "wdm", "~> 0.1.1", :platforms => [:mingw, :x64_mingw, :mswin]

# Lock `http_parser.rb` gem to `v0.6.x` on JRuby builds since newer versions of the gem
# do not have a Java counterpart.
gem "http_parser.rb", "~> 0.6.0", :platforms => [:jruby]

# Used for locally serving the website.
gem "webrick", "~> 1.7"
Loading

0 comments on commit 6e5bf19

Please sign in to comment.