diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml deleted file mode 100644 index 2432704..0000000 --- a/.github/workflows/blueprint.yml +++ /dev/null @@ -1,90 +0,0 @@ -on: - push: - branches: - - main - -# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages -permissions: - contents: read - pages: write - id-token: write - -jobs: - build_project: - runs-on: ubuntu-latest - name: Build project - steps: - - name: Checkout project - uses: actions/checkout@v2 - 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 leanprover/lean4:4.5.0 - - - name: Get cache - run: ~/.elan/bin/lake exe cache get || true - - - name: Build project - run: ~/.elan/bin/lake build Polya - - - name: Cache mathlib docs - uses: actions/cache@v3 - with: - path: | - .lake/build/doc/Init - .lake/build/doc/Lake - .lake/build/doc/Lean - .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- - - - 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 - with: - docker_image: ghcr.io/xu-cheng/texlive-full:20231201 - run: | - apk update - 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: Move documentation to `docs/docs` - run: | - sudo chown -R runner docs - cp -r .lake/build/doc docs/docs - - - name: Upload docs & blueprint artifact - uses: actions/upload-pages-artifact@v1 - with: - path: docs/ - - - name: Deploy to GitHub Pages - id: deployment - uses: actions/deploy-pages@v1 - - - name: Make sure the cache works - run: | - mv docs/docs .lake/build/doc - diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 8ac0810..ea265c9 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -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 @@ -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: | @@ -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 @@ -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/ @@ -119,4 +111,5 @@ jobs: uses: actions/deploy-pages@v1 - name: Make sure the cache works - run: mv docs/docs .lake/build/doc \ No newline at end of file + run: | + mv docs/docs .lake/build/doc diff --git a/docs/.bundle/config b/docs/.bundle/config new file mode 100644 index 0000000..2369228 --- /dev/null +++ b/docs/.bundle/config @@ -0,0 +1,2 @@ +--- +BUNDLE_PATH: "vendor/bundle" diff --git a/docs/.gitignore b/docs/.gitignore new file mode 100644 index 0000000..e4b7ba1 --- /dev/null +++ b/docs/.gitignore @@ -0,0 +1,8 @@ +_site +.sass-cache +.jekyll-cache +.jekyll-metadata +vendor +blueprint/ +blueprint.pdf +docs/ diff --git a/docs/404.html b/docs/404.html new file mode 100644 index 0000000..086a5c9 --- /dev/null +++ b/docs/404.html @@ -0,0 +1,25 @@ +--- +permalink: /404.html +layout: default +--- + + + +
+

404

+ +

Page not found :(

+

The requested page could not be found.

+
diff --git a/docs/Gemfile b/docs/Gemfile new file mode 100644 index 0000000..a6a5bb0 --- /dev/null +++ b/docs/Gemfile @@ -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" diff --git a/docs/Gemfile.lock b/docs/Gemfile.lock new file mode 100644 index 0000000..0239bd6 --- /dev/null +++ b/docs/Gemfile.lock @@ -0,0 +1,287 @@ +GEM + remote: https://rubygems.org/ + specs: + activesupport (6.0.5) + concurrent-ruby (~> 1.0, >= 1.0.2) + i18n (>= 0.7, < 2) + minitest (~> 5.1) + tzinfo (~> 1.1) + zeitwerk (~> 2.2, >= 2.2.2) + addressable (2.8.0) + public_suffix (>= 2.0.2, < 5.0) + coffee-script (2.4.1) + coffee-script-source + execjs + coffee-script-source (1.11.1) + colorator (1.1.0) + commonmarker (0.23.4) + concurrent-ruby (1.1.10) + dnsruby (1.61.9) + simpleidn (~> 0.1) + em-websocket (0.5.3) + eventmachine (>= 0.12.9) + http_parser.rb (~> 0) + ethon (0.15.0) + ffi (>= 1.15.0) + eventmachine (1.2.7) + execjs (2.8.1) + faraday (1.10.0) + faraday-em_http (~> 1.0) + faraday-em_synchrony (~> 1.0) + faraday-excon (~> 1.1) + faraday-httpclient (~> 1.0) + faraday-multipart (~> 1.0) + faraday-net_http (~> 1.0) + faraday-net_http_persistent (~> 1.0) + faraday-patron (~> 1.0) + faraday-rack (~> 1.0) + faraday-retry (~> 1.0) + ruby2_keywords (>= 0.0.4) + faraday-em_http (1.0.0) + faraday-em_synchrony (1.0.0) + faraday-excon (1.1.0) + faraday-httpclient (1.0.1) + faraday-multipart (1.0.3) + multipart-post (>= 1.2, < 3) + faraday-net_http (1.0.1) + faraday-net_http_persistent (1.2.0) + faraday-patron (1.0.0) + faraday-rack (1.0.0) + faraday-retry (1.0.3) + ffi (1.15.5) + forwardable-extended (2.6.0) + gemoji (3.0.1) + github-pages (226) + github-pages-health-check (= 1.17.9) + jekyll (= 3.9.2) + jekyll-avatar (= 0.7.0) + jekyll-coffeescript (= 1.1.1) + jekyll-commonmark-ghpages (= 0.2.0) + jekyll-default-layout (= 0.1.4) + jekyll-feed (= 0.15.1) + jekyll-gist (= 1.5.0) + jekyll-github-metadata (= 2.13.0) + jekyll-include-cache (= 0.2.1) + jekyll-mentions (= 1.6.0) + jekyll-optional-front-matter (= 0.3.2) + jekyll-paginate (= 1.1.0) + jekyll-readme-index (= 0.3.0) + jekyll-redirect-from (= 0.16.0) + jekyll-relative-links (= 0.6.1) + jekyll-remote-theme (= 0.4.3) + jekyll-sass-converter (= 1.5.2) + jekyll-seo-tag (= 2.8.0) + jekyll-sitemap (= 1.4.0) + jekyll-swiss (= 1.0.0) + jekyll-theme-architect (= 0.2.0) + jekyll-theme-cayman (= 0.2.0) + jekyll-theme-dinky (= 0.2.0) + jekyll-theme-hacker (= 0.2.0) + jekyll-theme-leap-day (= 0.2.0) + jekyll-theme-merlot (= 0.2.0) + jekyll-theme-midnight (= 0.2.0) + jekyll-theme-minimal (= 0.2.0) + jekyll-theme-modernist (= 0.2.0) + jekyll-theme-primer (= 0.6.0) + jekyll-theme-slate (= 0.2.0) + jekyll-theme-tactile (= 0.2.0) + jekyll-theme-time-machine (= 0.2.0) + jekyll-titles-from-headings (= 0.5.3) + jemoji (= 0.12.0) + kramdown (= 2.3.2) + kramdown-parser-gfm (= 1.1.0) + liquid (= 4.0.3) + mercenary (~> 0.3) + minima (= 2.5.1) + nokogiri (>= 1.13.4, < 2.0) + rouge (= 3.26.0) + terminal-table (~> 1.4) + github-pages-health-check (1.17.9) + addressable (~> 2.3) + dnsruby (~> 1.60) + octokit (~> 4.0) + public_suffix (>= 3.0, < 5.0) + typhoeus (~> 1.3) + html-pipeline (2.14.1) + activesupport (>= 2) + nokogiri (>= 1.4) + http_parser.rb (0.8.0) + i18n (0.9.5) + concurrent-ruby (~> 1.0) + jekyll (3.9.2) + addressable (~> 2.4) + colorator (~> 1.0) + em-websocket (~> 0.5) + i18n (~> 0.7) + jekyll-sass-converter (~> 1.0) + jekyll-watch (~> 2.0) + kramdown (>= 1.17, < 3) + liquid (~> 4.0) + mercenary (~> 0.3.3) + pathutil (~> 0.9) + rouge (>= 1.7, < 4) + safe_yaml (~> 1.0) + jekyll-avatar (0.7.0) + jekyll (>= 3.0, < 5.0) + jekyll-coffeescript (1.1.1) + coffee-script (~> 2.2) + coffee-script-source (~> 1.11.1) + jekyll-commonmark (1.4.0) + commonmarker (~> 0.22) + jekyll-commonmark-ghpages (0.2.0) + commonmarker (~> 0.23.4) + jekyll (~> 3.9.0) + jekyll-commonmark (~> 1.4.0) + rouge (>= 2.0, < 4.0) + jekyll-default-layout (0.1.4) + jekyll (~> 3.0) + jekyll-feed (0.15.1) + jekyll (>= 3.7, < 5.0) + jekyll-gist (1.5.0) + octokit (~> 4.2) + jekyll-github-metadata (2.13.0) + jekyll (>= 3.4, < 5.0) + octokit (~> 4.0, != 4.4.0) + jekyll-include-cache (0.2.1) + jekyll (>= 3.7, < 5.0) + jekyll-mentions (1.6.0) + html-pipeline (~> 2.3) + jekyll (>= 3.7, < 5.0) + jekyll-optional-front-matter (0.3.2) + jekyll (>= 3.0, < 5.0) + jekyll-paginate (1.1.0) + jekyll-readme-index (0.3.0) + jekyll (>= 3.0, < 5.0) + jekyll-redirect-from (0.16.0) + jekyll (>= 3.3, < 5.0) + jekyll-relative-links (0.6.1) + jekyll (>= 3.3, < 5.0) + jekyll-remote-theme (0.4.3) + addressable (~> 2.0) + jekyll (>= 3.5, < 5.0) + jekyll-sass-converter (>= 1.0, <= 3.0.0, != 2.0.0) + rubyzip (>= 1.3.0, < 3.0) + jekyll-sass-converter (1.5.2) + sass (~> 3.4) + jekyll-seo-tag (2.8.0) + jekyll (>= 3.8, < 5.0) + jekyll-sitemap (1.4.0) + jekyll (>= 3.7, < 5.0) + jekyll-swiss (1.0.0) + jekyll-theme-architect (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-cayman (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-dinky (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-hacker (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-leap-day (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-merlot (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-midnight (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-minimal (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-modernist (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-primer (0.6.0) + jekyll (> 3.5, < 5.0) + jekyll-github-metadata (~> 2.9) + jekyll-seo-tag (~> 2.0) + jekyll-theme-slate (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-tactile (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-time-machine (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-titles-from-headings (0.5.3) + jekyll (>= 3.3, < 5.0) + jekyll-watch (2.2.1) + listen (~> 3.0) + jemoji (0.12.0) + gemoji (~> 3.0) + html-pipeline (~> 2.2) + jekyll (>= 3.0, < 5.0) + kramdown (2.3.2) + rexml + kramdown-parser-gfm (1.1.0) + kramdown (~> 2.0) + liquid (4.0.3) + listen (3.7.1) + rb-fsevent (~> 0.10, >= 0.10.3) + rb-inotify (~> 0.9, >= 0.9.10) + mercenary (0.3.6) + minima (2.5.1) + jekyll (>= 3.5, < 5.0) + jekyll-feed (~> 0.9) + jekyll-seo-tag (~> 2.1) + minitest (5.15.0) + multipart-post (2.1.1) + nokogiri (1.13.6-x86_64-linux) + racc (~> 1.4) + octokit (4.22.0) + faraday (>= 0.9) + sawyer (~> 0.8.0, >= 0.5.3) + pathutil (0.16.2) + forwardable-extended (~> 2.6) + public_suffix (4.0.7) + racc (1.6.0) + rb-fsevent (0.11.1) + rb-inotify (0.10.1) + ffi (~> 1.0) + rexml (3.2.5) + rouge (3.26.0) + ruby2_keywords (0.0.5) + rubyzip (2.3.2) + safe_yaml (1.0.5) + sass (3.7.4) + sass-listen (~> 4.0.0) + sass-listen (4.0.0) + rb-fsevent (~> 0.9, >= 0.9.4) + rb-inotify (~> 0.9, >= 0.9.7) + sawyer (0.8.2) + addressable (>= 2.3.5) + faraday (> 0.8, < 2.0) + simpleidn (0.2.1) + unf (~> 0.1.4) + terminal-table (1.8.0) + unicode-display_width (~> 1.1, >= 1.1.1) + thread_safe (0.3.6) + typhoeus (1.4.0) + ethon (>= 0.9.0) + tzinfo (1.2.9) + thread_safe (~> 0.1) + unf (0.1.4) + unf_ext + unf_ext (0.0.8.1) + unicode-display_width (1.8.0) + webrick (1.7.0) + zeitwerk (2.5.4) + +PLATFORMS + x86_64-linux + +DEPENDENCIES + github-pages + http_parser.rb (~> 0.6.0) + tzinfo (~> 1.2) + tzinfo-data + wdm (~> 0.1.1) + webrick (~> 1.7) + +BUNDLED WITH + 2.3.14 diff --git a/docs/_config.yml b/docs/_config.yml new file mode 100644 index 0000000..00a02b0 --- /dev/null +++ b/docs/_config.yml @@ -0,0 +1,52 @@ +# Welcome to Jekyll! +# +# This config file is meant for settings that affect your whole blog, values +# which you are expected to set up once and rarely edit after that. If you find +# yourself editing this file very often, consider using Jekyll's data files +# feature for the data you need to update frequently. +# +# For technical reasons, this file is *NOT* reloaded automatically when you use +# 'bundle exec jekyll serve'. If you change this file, please restart the server process. +# +# If you need help with YAML syntax, here are some quick references for you: +# https://learn-the-web.algonquindesign.ca/topics/markdown-yaml-cheat-sheet/#yaml +# https://learnxinyminutes.com/docs/yaml/ +# +# Site settings +# These are used to personalize your new site. If you look in the HTML files, +# you will see them accessed via {{ site.title }}, {{ site.email }}, and so on. +# You can create any custom variable you would like, and they will be accessible +# in the templates via {{ site.myvariable }}. + +title: Arithmetic Progressions - Almost Periodicity +#email: your-email@example.com +description: A digitisation of the Kelley-Meka bound on Roth numbers +baseurl: "" # the subpath of your site, e.g. /blog +url: "https://YaelDillies.github.io/LeanAPAP/" # the base hostname & protocol for your site, e.g. http://example.com +#twitter_username: jekyllrb +github_username: YaelDillies +repository: YaelDillies/LeanAPAP + +# Build settings +remote_theme: pages-themes/cayman@v0.2.0 +plugins: + - jekyll-remote-theme +# Exclude from processing. +# The following items will not be processed, by default. +# Any item listed under the `exclude:` key here will be automatically added to +# the internal "default list". +# +# Excluded items can be processed by explicitly listing the directories or +# their entries' file path in the `include:` list. +# +# exclude: +# - .sass-cache/ +# - .jekyll-cache/ +# - gemfiles/ +# - Gemfile +# - Gemfile.lock +# - node_modules/ +# - vendor/bundle/ +# - vendor/cache/ +# - vendor/gems/ +# - vendor/ruby/ diff --git a/docs/_include/mathjax.html b/docs/_include/mathjax.html new file mode 100644 index 0000000..136e1d9 --- /dev/null +++ b/docs/_include/mathjax.html @@ -0,0 +1,10 @@ + +{% if page.usemathjax %} + + +{% endif %} diff --git a/docs/_layouts/default.html b/docs/_layouts/default.html new file mode 100644 index 0000000..777faeb --- /dev/null +++ b/docs/_layouts/default.html @@ -0,0 +1,55 @@ + + + + + + + {% seo %} + + + + + + {% if jekyll.environment == "production" %} + + {% else %} + + {% endif %} + {% include head-custom.html %} + + + + + + + +
+ {{ content }} + + +
+ + + diff --git a/docs/about.md b/docs/about.md new file mode 100644 index 0000000..2aa6e31 --- /dev/null +++ b/docs/about.md @@ -0,0 +1,17 @@ +--- +title: About +permalink: /about/ +--- + +This is the base Jekyll theme. You can find out more info about customizing your Jekyll theme, as well as basic Jekyll usage documentation at [jekyllrb.com](https://jekyllrb.com/) + +You can find the source code for Minima at GitHub: +[jekyll][jekyll-organization] / +[minima](https://github.com/jekyll/minima) + +You can find the source code for Jekyll at GitHub: +[jekyll][jekyll-organization] / +[jekyll](https://github.com/jekyll/jekyll) + + +[jekyll-organization]: https://github.com/jekyll diff --git a/docs/assets/css/style.scss b/docs/assets/css/style.scss new file mode 100644 index 0000000..efd5216 --- /dev/null +++ b/docs/assets/css/style.scss @@ -0,0 +1,17 @@ +--- +--- + +@import "{{ site.theme }}"; + +.page-header { + background-image: linear-gradient(120deg, #2d4fdc, #dc2ddc); +} + +.main-content h1, +.main-content h2, +.main-content h3, +.main-content h4, +.main-content h5, +.main-content h6 { + color: #6f1599; +} diff --git a/docs/index.md b/docs/index.md new file mode 100644 index 0000000..9e025e8 --- /dev/null +++ b/docs/index.md @@ -0,0 +1,125 @@ +--- +# Feel free to add content and custom Front Matter to this file. +# To modify the layout, see https://jekyllrb.com/docs/themes/#overriding-theme-defaults + +# layout: home +--- + +# Arithmetic Progressions - Almost Periodicity + +The purpose of this repository is to *digitise* some mathematical definitions, theorem statements +and theorem proofs. Digitisation, or formalisation, is a process where the source material, +typically a mathematical textbook or a pdf file or website or video, is transformed into definitions +in a target system consisting of a computer implementation of a logical theory (such as set theory +or type theory). + +## The source + +The definitions, theorems and proofs in this repository are taken from the exposition of Bloom and +Sisask on the Kelley-Meka bound on Roth numbers [2302.07211](https://arxiv.org/abs/2302.07211). + +The main result is that there is some constant `c > 0` such that, if `A ⊆ {1, ..., N}` contains no +non-trivial arithmetic progression of length 3, then `|A| ≤ N/exp(c * (log n)^(1/12)))` for some +constant `c > 0`. This is an amazing improvement over previous bounds, which were all of the form +`N/(log n)^c` for some constant `c`. + +## The target + +The formal system which we are using as a target system is Lean's dependent type theory. Lean is a +project being developed at AWS and Microsoft Research by Leonardo de Moura and his team. + +At this stage, mathlib4 contains all the background material that we need. However, not all +quality-of-life improvements that we know from Lean 3 have made it to Lean 4 (yet) and Lean 4 +suffers from its own problems that currently make it unsuitable for new formalisation of +research-level mathematics. As a consequence, we are sticking to Lean 3 until the project is +complete. Then we will port it to Lean 4 in order to upstream our basic results. + +## Content of this project + +This project currently contains about 3k lines of Lean code about the discrete (difference) +convolution, discrete Lp norms, discrete Fourier transform. It also contains proofs of a version of +almost periodicity and of a quantitative version of the Marcinkiewicz-Zygmund inequality. + +Once finished, this project will contain two main results (here `R` is the Roth number, the maximum +size of a set without three term arithmetic progressions): +* The **finite field case**: A proof that `R(F_q^n) ≤ q ^ (n - c * n ^ (1/9))` for some constant + `c`. This is worse than the Ellenberg-Gijswijt bound `R(F_q^n) ≤ q ^ (n - c * n)` which was + formalised in [Dahmen, Hölzl, Lewis](https://drops.dagstuhl.de/opus/volltexte/2019/11070/). The + goal here is therefore not to improve on the existing bound but instead demonstrate the + probability and Fourier analysis techniques, whereas Ellenberg-Gijswijt used the polynomial + method. +* The **integer case**: A proof that `R(n) ≤ N/exp(c * (log n)^(1/9)))`, using the same techniques + as in the finite field case, except for the fact that we now use Bohr sets instead of subspaces. + This bound is a slight improvement over the Kelley-Meka bound (with `1/12` as the exponent instead + of `1/9`). It is due to Bloom and Sisask. + +### Code organisation + +The Lean code is contained in the directory `src/`. The subdirectories are: +* `Mathlib`: Material missing from existing mathlib developments +* `Prereqs`: New developments to be integrated to mathlib +* `Physics`: The physical (as opposed to Fourier space) proof steps that are shared + between the finite field cases and integer case +* `FiniteField`: The proof steps specific to the finite field case +* `Integer`: The proof steps specific to the integer case + +### Current progress + +The project is not yet finished. The following table details live which files are unfinished, and +how many 'sorries' (unproven statements) remain in each file. + +{% include sorries.md %} + +## What next? + +Almost periodicity is nowadays a standard tool in additive combinatorics. The version we formalised is sufficient for many applications. In particular, it gives one of the best known bounds on Freiman's theorem. As a side goal, we might tackle Freiman's theorem. + +The discrete convolution/Lp norm/Fourier transform material belongs in mathlib and we hope to PR it there once the transition to Lean 4 has completed. Almost periodicity should similarly be upstreamed to mathlib given the numerous applications. The rest of the material might forever live in this repository. + +On top of the new developments, there are many basic lemmas needed for this project that are currently missing from mathlib. + +Here is the list of files that do not depend on any other LeanAPAP file, indicating they are good candidates for upstreaming to mathlib: + +{% include files_to_upstream.md %} + +## Build the Lean files + +To build the Lean files of this project, you need to have a working version of Lean. +See [the installation instructions](https://leanprover-community.github.io/get_started.html) (under Regular install). +Alternatively, click on the button below to open a Gitpod workspace containing the project. + +[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/#https://github.com/YaelDillies/LeanAPAP) + +In either case, run `lake exe cache get` and then `lake build` to build the project. + +## Build the blueprint + +To build the web version of the blueprint, you need a working LaTeX installation. +Furthermore, you need some packages: +``` +sudo apt install graphviz libgraphviz-dev +pip install -r blueprint/requirements.txt +``` + +To actually build the blueprint, run +``` +lake exe cache get +lake build +inv all +``` + +## Acknowledgements + +Our project builds on mathlib. We must therefore thank its numerous contributors without whom this +project couldn't even have started. + +Much of the project infrastructure has been adapted from +* [sphere eversion](https://leanprover-community.github.io/sphere-eversion/) +* [liquid tensor experiment](https://github.com/leanprover-community/liquid/) +* [unit fractions](https://github.com/b-mehta/unit-fractions/) + +## Source reference + +`[BS]` : https://arxiv.org/abs/2302.07211 + +[BS]: https://arxiv.org/abs/2302.07211 diff --git a/scripts/count_sorries.py b/scripts/count_sorries.py new file mode 100644 index 0000000..a609930 --- /dev/null +++ b/scripts/count_sorries.py @@ -0,0 +1,36 @@ +from glob import glob +import os +import re + +def ident_to_word(ident: str): + ident = ident.replace("_", " ") + return ident[0].upper() + ident[1:] + +def pretty_file(file: str): + segments = file[4:].replace(".lean", "").split("/") + name = ": ".join(ident_to_word(s) for s in segments) + url = f"https://github.com/alma-n/Polya-lean/blob/main/{file}" + return f"[{name}]({url})" + +files = [file for tree in os.walk("Polya") for file in glob(os.path.join(tree[0], '*.lean'))] +sorries = {} + +for file in files: + with open(file, "r") as f: + contents = f.read() + matches = [m.start() for m in re.finditer("sorry", contents)] + if len(matches) != 0: + sorries[pretty_file(file)] = len(matches) + +result = """ +| File | Sorries | +| ---- | ------- | +""" +for file in sorted(sorries.keys()): + result += f"| {file} | {sorries[file]} |\n" + +print(result) +if not os.path.exists("docs/_includes"): + os.makedirs("docs/_includes") +with open("docs/_includes/sorries.md", "w") as f: + f.write(result)