From a849c838924490beb94736be55b653e1c885d967 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 09:16:26 -0400 Subject: [PATCH 01/29] feat: update doc home page --- .github/workflows/docs.yml | 18 +++++- doc/.gitignore | 5 ++ doc/404.html | 25 ++++++++ doc/Gemfile | 36 +++++++++++ doc/Gemfile.lock | 120 +++++++++++++++++++++++++++++++++++++ doc/_config.yml | 53 ++++++++++++++++ doc/about.markdown | 6 ++ doc/index.markdown | 8 +++ 8 files changed, 270 insertions(+), 1 deletion(-) create mode 100644 doc/.gitignore create mode 100644 doc/404.html create mode 100644 doc/Gemfile create mode 100644 doc/Gemfile.lock create mode 100644 doc/_config.yml create mode 100644 doc/about.markdown create mode 100644 doc/index.markdown diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 4f95505..4475699 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -2,6 +2,7 @@ on: push: branches: - master + - Update-versions name: Build and deploy documentation @@ -56,11 +57,26 @@ jobs: - name: Build documentation run: ~/.elan/bin/lake -Kenv=dev build HepLean:docs + - name: Copy documentation to `docs/docs` + run: | + mv .lake/build/doc docs/docs + + - 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: Upload docs & blueprint artifact uses: actions/upload-pages-artifact@v1 with: - path: .lake/build/doc + path: docs/_site - name: Deploy to GitHub Pages id: deployment diff --git a/doc/.gitignore b/doc/.gitignore new file mode 100644 index 0000000..f40fbd8 --- /dev/null +++ b/doc/.gitignore @@ -0,0 +1,5 @@ +_site +.sass-cache +.jekyll-cache +.jekyll-metadata +vendor diff --git a/doc/404.html b/doc/404.html new file mode 100644 index 0000000..086a5c9 --- /dev/null +++ b/doc/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/doc/Gemfile b/doc/Gemfile new file mode 100644 index 0000000..1ea1366 --- /dev/null +++ b/doc/Gemfile @@ -0,0 +1,36 @@ +source "https://rubygems.org" +# Hello! This is where you manage which Jekyll version is used to run. +# When you want to use a different version, change it below, save the +# file and run `bundle install`. Run Jekyll with `bundle exec`, like so: +# +# bundle exec jekyll serve +# +# This will help ensure the proper Jekyll version is running. +# Happy Jekylling! +gem "jekyll", "~> 4.3.3" +# This is the default theme for new Jekyll sites. You may change this to anything you like. +gem "minima", "~> 2.5" +# If you want to use GitHub Pages, remove the "gem "jekyll"" above and +# uncomment the line below. 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", "< 3" + 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] + +# Theme +gem "jekyll-theme-simplex" \ No newline at end of file diff --git a/doc/Gemfile.lock b/doc/Gemfile.lock new file mode 100644 index 0000000..2add535 --- /dev/null +++ b/doc/Gemfile.lock @@ -0,0 +1,120 @@ +GEM + remote: https://rubygems.org/ + specs: + addressable (2.8.6) + public_suffix (>= 2.0.2, < 6.0) + bigdecimal (3.1.8) + colorator (1.1.0) + concurrent-ruby (1.3.3) + em-websocket (0.5.3) + eventmachine (>= 0.12.9) + http_parser.rb (~> 0) + eventmachine (1.2.7) + ffi (1.17.0) + ffi (1.17.0-arm64-darwin) + ffi (1.17.0-x86_64-darwin) + forwardable-extended (2.6.0) + google-protobuf (4.27.1) + bigdecimal + rake (>= 13) + google-protobuf (4.27.1-arm64-darwin) + bigdecimal + rake (>= 13) + google-protobuf (4.27.1-x86_64-darwin) + bigdecimal + rake (>= 13) + http_parser.rb (0.8.0) + i18n (1.14.5) + concurrent-ruby (~> 1.0) + jekyll (4.3.3) + addressable (~> 2.4) + colorator (~> 1.0) + em-websocket (~> 0.5) + i18n (~> 1.0) + jekyll-sass-converter (>= 2.0, < 4.0) + jekyll-watch (~> 2.0) + kramdown (~> 2.3, >= 2.3.1) + kramdown-parser-gfm (~> 1.0) + liquid (~> 4.0) + mercenary (>= 0.3.6, < 0.5) + pathutil (~> 0.9) + rouge (>= 3.0, < 5.0) + safe_yaml (~> 1.0) + terminal-table (>= 1.8, < 4.0) + webrick (~> 1.7) + jekyll-feed (0.17.0) + jekyll (>= 3.7, < 5.0) + jekyll-sass-converter (3.0.0) + sass-embedded (~> 1.54) + jekyll-seo-tag (2.8.0) + jekyll (>= 3.8, < 5.0) + jekyll-theme-simplex (0.9.8.15) + jekyll (~> 4.0) + jekyll-watch (2.2.1) + listen (~> 3.0) + kramdown (2.4.0) + rexml + kramdown-parser-gfm (1.1.0) + kramdown (~> 2.0) + liquid (4.0.4) + listen (3.9.0) + rb-fsevent (~> 0.10, >= 0.10.3) + rb-inotify (~> 0.9, >= 0.9.10) + mercenary (0.4.0) + minima (2.5.1) + jekyll (>= 3.5, < 5.0) + jekyll-feed (~> 0.9) + jekyll-seo-tag (~> 2.1) + pathutil (0.16.2) + forwardable-extended (~> 2.6) + public_suffix (5.0.5) + rake (13.2.1) + rb-fsevent (0.11.2) + rb-inotify (0.11.1) + ffi (~> 1.0) + rexml (3.3.0) + strscan + rouge (4.3.0) + safe_yaml (1.0.5) + sass-embedded (1.77.5) + google-protobuf (>= 3.25, < 5.0) + rake (>= 13) + sass-embedded (1.77.5-aarch64-mingw-ucrt) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-arm64-darwin) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-x86-cygwin) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-x86-mingw-ucrt) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-x86_64-cygwin) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-x86_64-darwin) + google-protobuf (>= 3.25, < 5.0) + strscan (3.1.0) + terminal-table (3.0.2) + unicode-display_width (>= 1.1.1, < 3) + unicode-display_width (2.5.0) + webrick (1.8.1) + +PLATFORMS + aarch64-mingw-ucrt + arm64-darwin-23 + ruby + x86-cygwin + x86-mingw-ucrt + x86_64-cygwin + x86_64-darwin + +DEPENDENCIES + http_parser.rb (~> 0.6.0) + jekyll (~> 4.3.3) + jekyll-feed (~> 0.12) + jekyll-theme-simplex + minima (~> 2.5) + tzinfo (>= 1, < 3) + tzinfo-data + wdm (~> 0.1.1) + +BUNDLED WITH + 2.5.13 diff --git a/doc/_config.yml b/doc/_config.yml new file mode 100644 index 0000000..1ab1755 --- /dev/null +++ b/doc/_config.yml @@ -0,0 +1,53 @@ +# 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: HepLean +#email: your-email@example.com +description: >- # this means to ignore newlines until "baseurl:" + A project to digitalize results from high-energy physics into Lean 4. +baseurl: "" # the subpath of your site, e.g. /blog +url: "" # the base hostname & protocol for your site, e.g. http://example.com +#twitter_username: jekyllrb +github_username: HEPLean + +# Build settings +theme: minima +plugins: + - jekyll-feed + +# 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/doc/about.markdown b/doc/about.markdown new file mode 100644 index 0000000..2e6534f --- /dev/null +++ b/doc/about.markdown @@ -0,0 +1,6 @@ +--- +layout: page +title: About +permalink: /about/ +--- + diff --git a/doc/index.markdown b/doc/index.markdown new file mode 100644 index 0000000..3a952fa --- /dev/null +++ b/doc/index.markdown @@ -0,0 +1,8 @@ +--- +# 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 +--- +## Documentation + From 1d06ef188e5a7dd1eb6d62782ac13ad04062a7b1 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 09:27:08 -0400 Subject: [PATCH 02/29] Update Gemfile --- doc/Gemfile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/Gemfile b/doc/Gemfile index 1ea1366..fe73ca0 100644 --- a/doc/Gemfile +++ b/doc/Gemfile @@ -7,12 +7,12 @@ source "https://rubygems.org" # # This will help ensure the proper Jekyll version is running. # Happy Jekylling! -gem "jekyll", "~> 4.3.3" +#gem "jekyll", "~> 4.3.3" # This is the default theme for new Jekyll sites. You may change this to anything you like. gem "minima", "~> 2.5" # If you want to use GitHub Pages, remove the "gem "jekyll"" above and # uncomment the line below. To upgrade, run `bundle update github-pages`. -# gem "github-pages", group: :jekyll_plugins +gem "github-pages", group: :jekyll_plugins # If you have any plugins, put them here! group :jekyll_plugins do gem "jekyll-feed", "~> 0.12" From bf578e435f339bad1eb0232e8e220a47b4db3526 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 09:28:19 -0400 Subject: [PATCH 03/29] Update workflow --- .github/workflows/docs.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 4475699..09f4809 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -59,18 +59,18 @@ jobs: - name: Copy documentation to `docs/docs` run: | - mv .lake/build/doc docs/docs + mv .lake/build/doc doc/docs - name: Bundle dependencies uses: ruby/setup-ruby@v1 with: - working-directory: docs + working-directory: doc 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 + working-directory: doc run: JEKYLL_ENV=production bundle exec jekyll build - name: Upload docs & blueprint artifact From 3fc21aaf20594d49142968ec359db204f0565280 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 09:48:40 -0400 Subject: [PATCH 04/29] Update Gemfile --- doc/Gemfile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/Gemfile b/doc/Gemfile index fe73ca0..1ea1366 100644 --- a/doc/Gemfile +++ b/doc/Gemfile @@ -7,12 +7,12 @@ source "https://rubygems.org" # # This will help ensure the proper Jekyll version is running. # Happy Jekylling! -#gem "jekyll", "~> 4.3.3" +gem "jekyll", "~> 4.3.3" # This is the default theme for new Jekyll sites. You may change this to anything you like. gem "minima", "~> 2.5" # If you want to use GitHub Pages, remove the "gem "jekyll"" above and # uncomment the line below. To upgrade, run `bundle update github-pages`. -gem "github-pages", group: :jekyll_plugins +# gem "github-pages", group: :jekyll_plugins # If you have any plugins, put them here! group :jekyll_plugins do gem "jekyll-feed", "~> 0.12" From cb45f5800ad1f3f12c64c65e44ef19fe6386c4ca Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 09:58:30 -0400 Subject: [PATCH 05/29] Update docs.yml --- .github/workflows/docs.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 09f4809..486e92c 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -65,7 +65,7 @@ jobs: uses: ruby/setup-ruby@v1 with: working-directory: doc - ruby-version: "3.0" # Not needed with a .ruby-version file + ruby-version: "3.1" # Not needed with a .ruby-version file bundler-cache: true # runs 'bundle install' and caches installed gems automatically From 009ff421082656d91ad127947abe300f20c57d1b Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 10:08:07 -0400 Subject: [PATCH 06/29] Update docs.yml --- .github/workflows/docs.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 486e92c..567b71b 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -76,7 +76,7 @@ jobs: - name: Upload docs & blueprint artifact uses: actions/upload-pages-artifact@v1 with: - path: docs/_site + path: doc/_site - name: Deploy to GitHub Pages id: deployment From 133ebce22ac195762a13614c17f2e55b805b7375 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 10:24:40 -0400 Subject: [PATCH 07/29] refactor: Try to get docs working --- doc/Gemfile | 6 +- doc/Gemfile.lock | 260 ++++++++++++++++++++++++++++++++++++++--------- 2 files changed, 216 insertions(+), 50 deletions(-) diff --git a/doc/Gemfile b/doc/Gemfile index 1ea1366..1aa9ada 100644 --- a/doc/Gemfile +++ b/doc/Gemfile @@ -7,12 +7,12 @@ source "https://rubygems.org" # # This will help ensure the proper Jekyll version is running. # Happy Jekylling! -gem "jekyll", "~> 4.3.3" +#gem "jekyll", "~> 4.3.3" # This is the default theme for new Jekyll sites. You may change this to anything you like. gem "minima", "~> 2.5" # If you want to use GitHub Pages, remove the "gem "jekyll"" above and # uncomment the line below. To upgrade, run `bundle update github-pages`. -# gem "github-pages", group: :jekyll_plugins +gem "github-pages", "~> 231", group: :jekyll_plugins # If you have any plugins, put them here! group :jekyll_plugins do gem "jekyll-feed", "~> 0.12" @@ -32,5 +32,3 @@ gem "wdm", "~> 0.1.1", :platforms => [:mingw, :x64_mingw, :mswin] # do not have a Java counterpart. gem "http_parser.rb", "~> 0.6.0", :platforms => [:jruby] -# Theme -gem "jekyll-theme-simplex" \ No newline at end of file diff --git a/doc/Gemfile.lock b/doc/Gemfile.lock index 2add535..45c3b15 100644 --- a/doc/Gemfile.lock +++ b/doc/Gemfile.lock @@ -1,57 +1,212 @@ GEM remote: https://rubygems.org/ specs: + activesupport (7.1.3.4) + base64 + bigdecimal + concurrent-ruby (~> 1.0, >= 1.0.2) + connection_pool (>= 2.2.5) + drb + i18n (>= 1.6, < 2) + minitest (>= 5.1) + mutex_m + tzinfo (~> 2.0) addressable (2.8.6) public_suffix (>= 2.0.2, < 6.0) + base64 (0.2.0) bigdecimal (3.1.8) + coffee-script (2.4.1) + coffee-script-source + execjs + coffee-script-source (1.12.2) colorator (1.1.0) + commonmarker (0.23.10) concurrent-ruby (1.3.3) + connection_pool (2.4.1) + dnsruby (1.72.1) + simpleidn (~> 0.2.1) + drb (2.2.1) em-websocket (0.5.3) eventmachine (>= 0.12.9) http_parser.rb (~> 0) + ethon (0.16.0) + ffi (>= 1.15.0) eventmachine (1.2.7) + execjs (2.9.1) + faraday (2.9.1) + faraday-net_http (>= 2.0, < 3.2) + faraday-net_http (3.1.0) + net-http ffi (1.17.0) ffi (1.17.0-arm64-darwin) ffi (1.17.0-x86_64-darwin) forwardable-extended (2.6.0) - google-protobuf (4.27.1) - bigdecimal - rake (>= 13) - google-protobuf (4.27.1-arm64-darwin) - bigdecimal - rake (>= 13) - google-protobuf (4.27.1-x86_64-darwin) - bigdecimal - rake (>= 13) + gemoji (4.1.0) + github-pages (231) + github-pages-health-check (= 1.18.2) + jekyll (= 3.9.5) + jekyll-avatar (= 0.8.0) + jekyll-coffeescript (= 1.2.2) + jekyll-commonmark-ghpages (= 0.4.0) + jekyll-default-layout (= 0.1.5) + jekyll-feed (= 0.17.0) + jekyll-gist (= 1.5.0) + jekyll-github-metadata (= 2.16.1) + 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.13.0) + kramdown (= 2.4.0) + kramdown-parser-gfm (= 1.1.0) + liquid (= 4.0.4) + mercenary (~> 0.3) + minima (= 2.5.1) + nokogiri (>= 1.13.6, < 2.0) + rouge (= 3.30.0) + terminal-table (~> 1.4) + github-pages-health-check (1.18.2) + addressable (~> 2.3) + dnsruby (~> 1.60) + octokit (>= 4, < 8) + public_suffix (>= 3.0, < 6.0) + typhoeus (~> 1.3) + html-pipeline (2.14.3) + activesupport (>= 2) + nokogiri (>= 1.4) http_parser.rb (0.8.0) i18n (1.14.5) concurrent-ruby (~> 1.0) - jekyll (4.3.3) + jekyll (3.9.5) addressable (~> 2.4) colorator (~> 1.0) em-websocket (~> 0.5) - i18n (~> 1.0) - jekyll-sass-converter (>= 2.0, < 4.0) + i18n (>= 0.7, < 2) + jekyll-sass-converter (~> 1.0) jekyll-watch (~> 2.0) - kramdown (~> 2.3, >= 2.3.1) - kramdown-parser-gfm (~> 1.0) + kramdown (>= 1.17, < 3) liquid (~> 4.0) - mercenary (>= 0.3.6, < 0.5) + mercenary (~> 0.3.3) pathutil (~> 0.9) - rouge (>= 3.0, < 5.0) + rouge (>= 1.7, < 4) safe_yaml (~> 1.0) - terminal-table (>= 1.8, < 4.0) - webrick (~> 1.7) + jekyll-avatar (0.8.0) + jekyll (>= 3.0, < 5.0) + jekyll-coffeescript (1.2.2) + coffee-script (~> 2.2) + coffee-script-source (~> 1.12) + jekyll-commonmark (1.4.0) + commonmarker (~> 0.22) + jekyll-commonmark-ghpages (0.4.0) + commonmarker (~> 0.23.7) + jekyll (~> 3.9.0) + jekyll-commonmark (~> 1.4.0) + rouge (>= 2.0, < 5.0) + jekyll-default-layout (0.1.5) + jekyll (>= 3.0, < 5.0) jekyll-feed (0.17.0) jekyll (>= 3.7, < 5.0) - jekyll-sass-converter (3.0.0) - sass-embedded (~> 1.54) + jekyll-gist (1.5.0) + octokit (~> 4.2) + jekyll-github-metadata (2.16.1) + jekyll (>= 3.4, < 5.0) + octokit (>= 4, < 7, != 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-theme-simplex (0.9.8.15) - jekyll (~> 4.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.13.0) + gemoji (>= 3, < 5) + html-pipeline (~> 2.2) + jekyll (>= 3.0, < 5.0) kramdown (2.4.0) rexml kramdown-parser-gfm (1.1.0) @@ -60,42 +215,56 @@ GEM listen (3.9.0) rb-fsevent (~> 0.10, >= 0.10.3) rb-inotify (~> 0.9, >= 0.9.10) - mercenary (0.4.0) + mercenary (0.3.6) + mini_portile2 (2.8.7) minima (2.5.1) jekyll (>= 3.5, < 5.0) jekyll-feed (~> 0.9) jekyll-seo-tag (~> 2.1) + minitest (5.23.1) + mutex_m (0.2.0) + net-http (0.4.1) + uri + nokogiri (1.16.6) + mini_portile2 (~> 2.8.2) + racc (~> 1.4) + nokogiri (1.16.6-arm64-darwin) + racc (~> 1.4) + nokogiri (1.16.6-x86_64-darwin) + racc (~> 1.4) + octokit (4.25.1) + faraday (>= 1, < 3) + sawyer (~> 0.9) pathutil (0.16.2) forwardable-extended (~> 2.6) public_suffix (5.0.5) - rake (13.2.1) + racc (1.8.0) rb-fsevent (0.11.2) rb-inotify (0.11.1) ffi (~> 1.0) rexml (3.3.0) strscan - rouge (4.3.0) + rouge (3.30.0) + rubyzip (2.3.2) safe_yaml (1.0.5) - sass-embedded (1.77.5) - google-protobuf (>= 3.25, < 5.0) - rake (>= 13) - sass-embedded (1.77.5-aarch64-mingw-ucrt) - google-protobuf (>= 3.25, < 5.0) - sass-embedded (1.77.5-arm64-darwin) - google-protobuf (>= 3.25, < 5.0) - sass-embedded (1.77.5-x86-cygwin) - google-protobuf (>= 3.25, < 5.0) - sass-embedded (1.77.5-x86-mingw-ucrt) - google-protobuf (>= 3.25, < 5.0) - sass-embedded (1.77.5-x86_64-cygwin) - google-protobuf (>= 3.25, < 5.0) - sass-embedded (1.77.5-x86_64-darwin) - google-protobuf (>= 3.25, < 5.0) + 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.9.2) + addressable (>= 2.3.5) + faraday (>= 0.17.3, < 3) + simpleidn (0.2.3) strscan (3.1.0) - terminal-table (3.0.2) - unicode-display_width (>= 1.1.1, < 3) - unicode-display_width (2.5.0) - webrick (1.8.1) + terminal-table (1.8.0) + unicode-display_width (~> 1.1, >= 1.1.1) + typhoeus (1.4.1) + ethon (>= 0.9.0) + tzinfo (2.0.6) + concurrent-ruby (~> 1.0) + unicode-display_width (1.8.0) + uri (0.13.0) PLATFORMS aarch64-mingw-ucrt @@ -107,10 +276,9 @@ PLATFORMS x86_64-darwin DEPENDENCIES + github-pages (~> 231) http_parser.rb (~> 0.6.0) - jekyll (~> 4.3.3) jekyll-feed (~> 0.12) - jekyll-theme-simplex minima (~> 2.5) tzinfo (>= 1, < 3) tzinfo-data From b5f1b3db6d3633508584bfeeeefd30cdfbbcf93b Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 10:31:29 -0400 Subject: [PATCH 08/29] Update docs.yml --- .github/workflows/docs.yml | 50 +++++++++++++++++++------------------- 1 file changed, 25 insertions(+), 25 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 567b71b..a1234ab 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -30,36 +30,36 @@ jobs: comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/teorth\/HepLean\/blob\/master\/\1)/' > docs/_includes/files_to_upstream.md rm 1.txt 2.txt - - 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: 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 + # - name: Get cache + # run: ~/.elan/bin/lake -Kenv=dev exe cache get || true - - name: Build project - run: ~/.elan/bin/lake -Kenv=dev build HepLean + # - name: Build project + # run: ~/.elan/bin/lake -Kenv=dev build HepLean - - 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-HepLean* - key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} - restore-keys: | - MathlibDoc- + # - 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-HepLean* + # key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} + # restore-keys: | + # MathlibDoc- - - name: Build documentation - run: ~/.elan/bin/lake -Kenv=dev build HepLean:docs + # - name: Build documentation + # run: ~/.elan/bin/lake -Kenv=dev build HepLean:docs - - name: Copy documentation to `docs/docs` - run: | - mv .lake/build/doc doc/docs + #- name: Copy documentation to `docs/docs` + # run: | + # mv .lake/build/doc doc/docs - name: Bundle dependencies uses: ruby/setup-ruby@v1 From a1601c02ccc23c5c4d3380e7aa370a89a512065a Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 10:43:37 -0400 Subject: [PATCH 09/29] update Gemfiles --- doc/Gemfile | 5 +- doc/Gemfile.lock | 257 ++++++++--------------------------------------- 2 files changed, 45 insertions(+), 217 deletions(-) diff --git a/doc/Gemfile b/doc/Gemfile index 1aa9ada..f01211b 100644 --- a/doc/Gemfile +++ b/doc/Gemfile @@ -7,12 +7,12 @@ source "https://rubygems.org" # # This will help ensure the proper Jekyll version is running. # Happy Jekylling! -#gem "jekyll", "~> 4.3.3" +gem "jekyll", "~> 4.3.3" # This is the default theme for new Jekyll sites. You may change this to anything you like. gem "minima", "~> 2.5" # If you want to use GitHub Pages, remove the "gem "jekyll"" above and # uncomment the line below. To upgrade, run `bundle update github-pages`. -gem "github-pages", "~> 231", group: :jekyll_plugins +# gem "github-pages", group: :jekyll_plugins # If you have any plugins, put them here! group :jekyll_plugins do gem "jekyll-feed", "~> 0.12" @@ -31,4 +31,3 @@ 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] - diff --git a/doc/Gemfile.lock b/doc/Gemfile.lock index 45c3b15..bfb388f 100644 --- a/doc/Gemfile.lock +++ b/doc/Gemfile.lock @@ -1,212 +1,55 @@ GEM remote: https://rubygems.org/ specs: - activesupport (7.1.3.4) - base64 - bigdecimal - concurrent-ruby (~> 1.0, >= 1.0.2) - connection_pool (>= 2.2.5) - drb - i18n (>= 1.6, < 2) - minitest (>= 5.1) - mutex_m - tzinfo (~> 2.0) addressable (2.8.6) public_suffix (>= 2.0.2, < 6.0) - base64 (0.2.0) bigdecimal (3.1.8) - coffee-script (2.4.1) - coffee-script-source - execjs - coffee-script-source (1.12.2) colorator (1.1.0) - commonmarker (0.23.10) concurrent-ruby (1.3.3) - connection_pool (2.4.1) - dnsruby (1.72.1) - simpleidn (~> 0.2.1) - drb (2.2.1) em-websocket (0.5.3) eventmachine (>= 0.12.9) http_parser.rb (~> 0) - ethon (0.16.0) - ffi (>= 1.15.0) eventmachine (1.2.7) - execjs (2.9.1) - faraday (2.9.1) - faraday-net_http (>= 2.0, < 3.2) - faraday-net_http (3.1.0) - net-http ffi (1.17.0) ffi (1.17.0-arm64-darwin) ffi (1.17.0-x86_64-darwin) forwardable-extended (2.6.0) - gemoji (4.1.0) - github-pages (231) - github-pages-health-check (= 1.18.2) - jekyll (= 3.9.5) - jekyll-avatar (= 0.8.0) - jekyll-coffeescript (= 1.2.2) - jekyll-commonmark-ghpages (= 0.4.0) - jekyll-default-layout (= 0.1.5) - jekyll-feed (= 0.17.0) - jekyll-gist (= 1.5.0) - jekyll-github-metadata (= 2.16.1) - 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.13.0) - kramdown (= 2.4.0) - kramdown-parser-gfm (= 1.1.0) - liquid (= 4.0.4) - mercenary (~> 0.3) - minima (= 2.5.1) - nokogiri (>= 1.13.6, < 2.0) - rouge (= 3.30.0) - terminal-table (~> 1.4) - github-pages-health-check (1.18.2) - addressable (~> 2.3) - dnsruby (~> 1.60) - octokit (>= 4, < 8) - public_suffix (>= 3.0, < 6.0) - typhoeus (~> 1.3) - html-pipeline (2.14.3) - activesupport (>= 2) - nokogiri (>= 1.4) + google-protobuf (4.27.1) + bigdecimal + rake (>= 13) + google-protobuf (4.27.1-arm64-darwin) + bigdecimal + rake (>= 13) + google-protobuf (4.27.1-x86_64-darwin) + bigdecimal + rake (>= 13) http_parser.rb (0.8.0) i18n (1.14.5) concurrent-ruby (~> 1.0) - jekyll (3.9.5) + jekyll (4.3.3) addressable (~> 2.4) colorator (~> 1.0) em-websocket (~> 0.5) - i18n (>= 0.7, < 2) - jekyll-sass-converter (~> 1.0) + i18n (~> 1.0) + jekyll-sass-converter (>= 2.0, < 4.0) jekyll-watch (~> 2.0) - kramdown (>= 1.17, < 3) + kramdown (~> 2.3, >= 2.3.1) + kramdown-parser-gfm (~> 1.0) liquid (~> 4.0) - mercenary (~> 0.3.3) + mercenary (>= 0.3.6, < 0.5) pathutil (~> 0.9) - rouge (>= 1.7, < 4) + rouge (>= 3.0, < 5.0) safe_yaml (~> 1.0) - jekyll-avatar (0.8.0) - jekyll (>= 3.0, < 5.0) - jekyll-coffeescript (1.2.2) - coffee-script (~> 2.2) - coffee-script-source (~> 1.12) - jekyll-commonmark (1.4.0) - commonmarker (~> 0.22) - jekyll-commonmark-ghpages (0.4.0) - commonmarker (~> 0.23.7) - jekyll (~> 3.9.0) - jekyll-commonmark (~> 1.4.0) - rouge (>= 2.0, < 5.0) - jekyll-default-layout (0.1.5) - jekyll (>= 3.0, < 5.0) + terminal-table (>= 1.8, < 4.0) + webrick (~> 1.7) jekyll-feed (0.17.0) jekyll (>= 3.7, < 5.0) - jekyll-gist (1.5.0) - octokit (~> 4.2) - jekyll-github-metadata (2.16.1) - jekyll (>= 3.4, < 5.0) - octokit (>= 4, < 7, != 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-sass-converter (3.0.0) + sass-embedded (~> 1.54) 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.13.0) - gemoji (>= 3, < 5) - html-pipeline (~> 2.2) - jekyll (>= 3.0, < 5.0) kramdown (2.4.0) rexml kramdown-parser-gfm (1.1.0) @@ -215,56 +58,42 @@ GEM listen (3.9.0) rb-fsevent (~> 0.10, >= 0.10.3) rb-inotify (~> 0.9, >= 0.9.10) - mercenary (0.3.6) - mini_portile2 (2.8.7) + mercenary (0.4.0) minima (2.5.1) jekyll (>= 3.5, < 5.0) jekyll-feed (~> 0.9) jekyll-seo-tag (~> 2.1) - minitest (5.23.1) - mutex_m (0.2.0) - net-http (0.4.1) - uri - nokogiri (1.16.6) - mini_portile2 (~> 2.8.2) - racc (~> 1.4) - nokogiri (1.16.6-arm64-darwin) - racc (~> 1.4) - nokogiri (1.16.6-x86_64-darwin) - racc (~> 1.4) - octokit (4.25.1) - faraday (>= 1, < 3) - sawyer (~> 0.9) pathutil (0.16.2) forwardable-extended (~> 2.6) public_suffix (5.0.5) - racc (1.8.0) + rake (13.2.1) rb-fsevent (0.11.2) rb-inotify (0.11.1) ffi (~> 1.0) rexml (3.3.0) strscan - rouge (3.30.0) - rubyzip (2.3.2) + rouge (4.3.0) 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.9.2) - addressable (>= 2.3.5) - faraday (>= 0.17.3, < 3) - simpleidn (0.2.3) + sass-embedded (1.77.5) + google-protobuf (>= 3.25, < 5.0) + rake (>= 13) + sass-embedded (1.77.5-aarch64-mingw-ucrt) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-arm64-darwin) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-x86-cygwin) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-x86-mingw-ucrt) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-x86_64-cygwin) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-x86_64-darwin) + google-protobuf (>= 3.25, < 5.0) strscan (3.1.0) - terminal-table (1.8.0) - unicode-display_width (~> 1.1, >= 1.1.1) - typhoeus (1.4.1) - ethon (>= 0.9.0) - tzinfo (2.0.6) - concurrent-ruby (~> 1.0) - unicode-display_width (1.8.0) - uri (0.13.0) + terminal-table (3.0.2) + unicode-display_width (>= 1.1.1, < 3) + unicode-display_width (2.5.0) + webrick (1.8.1) PLATFORMS aarch64-mingw-ucrt @@ -276,8 +105,8 @@ PLATFORMS x86_64-darwin DEPENDENCIES - github-pages (~> 231) http_parser.rb (~> 0.6.0) + jekyll (~> 4.3.3) jekyll-feed (~> 0.12) minima (~> 2.5) tzinfo (>= 1, < 3) From e8f0bb92dddf296a7bfa4533a0af4944c445b5a3 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 10:48:32 -0400 Subject: [PATCH 10/29] Update docs.yml --- .github/workflows/docs.yml | 107 +++++++++++++------------------------ 1 file changed, 38 insertions(+), 69 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index a1234ab..8cc31f9 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -1,86 +1,55 @@ -on: - push: +# Sample workflow for building and deploying a Jekyll site to GitHub Pages +name: Deploy Jekyll with GitHub Pages dependencies preinstalled + +on: + # Runs on pushes targeting the default branch + push: branches: - - master - Update-versions -name: Build and deploy documentation + # Allows you to run this workflow manually from the Actions tab + workflow_dispatch: -# borrowed from https://github.com/teorth/pfr/blob/master/.github/workflows/push.yml -permissions: +# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages +permissions: contents: read pages: write id-token: write -jobs: - build_project: +# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued. +# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete. +concurrency: + group: "pages" + cancel-in-progress: false + +jobs: + # Build job + build: runs-on: ubuntu-latest - name: Build project steps: - - name: Checkout project + - name: Checkout uses: actions/checkout@v4 + - name: Setup Pages + uses: actions/configure-pages@v5 + - name: Build with Jekyll + uses: actions/jekyll-build-pages@v1 with: - fetch-depth: 0 - - - name: Print files to upstream - run: | - grep -r --files-without-match 'import HepLean' HepLean | sort > 1.txt - grep -r --files-with-match 'sorry' HepLean | sort > 2.txt - mkdir -p docs/_includes - comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/teorth\/HepLean\/blob\/master\/\1)/' > docs/_includes/files_to_upstream.md - rm 1.txt 2.txt - - # - 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 - - # - name: Build project - # run: ~/.elan/bin/lake -Kenv=dev build HepLean - - # - 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-HepLean* - # key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} - # restore-keys: | - # MathlibDoc- - - # - name: Build documentation - # run: ~/.elan/bin/lake -Kenv=dev build HepLean:docs - - #- name: Copy documentation to `docs/docs` - # run: | - # mv .lake/build/doc doc/docs - - - name: Bundle dependencies - uses: ruby/setup-ruby@v1 - with: - working-directory: doc - ruby-version: "3.1" # Not needed with a .ruby-version file - bundler-cache: true # runs 'bundle install' and caches installed gems automatically - - - - name: Bundle website - working-directory: doc - run: JEKYLL_ENV=production bundle exec jekyll build - - - name: Upload docs & blueprint artifact - uses: actions/upload-pages-artifact@v1 + source: ./doc + destination: ./doc/_site + - name: Upload artifact + uses: actions/upload-pages-artifact@v3 with: path: doc/_site + + # Deployment job + deploy: + environment: + name: github-pages + url: ${{ steps.deployment.outputs.page_url }} + runs-on: ubuntu-latest + needs: build + steps: - name: Deploy to GitHub Pages id: deployment - uses: actions/deploy-pages@v1 - - - + uses: actions/deploy-pages@v4 \ No newline at end of file From c7be7900804a9abc092ea08f11e6ecbdd24b4f66 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 10:56:11 -0400 Subject: [PATCH 11/29] update --- doc/Gemfile | 4 +- doc/Gemfile.lock | 257 +++++++++++++++++++++++++++++++++++++++-------- 2 files changed, 216 insertions(+), 45 deletions(-) diff --git a/doc/Gemfile b/doc/Gemfile index f01211b..efc9caa 100644 --- a/doc/Gemfile +++ b/doc/Gemfile @@ -7,12 +7,12 @@ source "https://rubygems.org" # # This will help ensure the proper Jekyll version is running. # Happy Jekylling! -gem "jekyll", "~> 4.3.3" +#gem "jekyll", "~> 4.3.3" # This is the default theme for new Jekyll sites. You may change this to anything you like. gem "minima", "~> 2.5" # If you want to use GitHub Pages, remove the "gem "jekyll"" above and # uncomment the line below. To upgrade, run `bundle update github-pages`. -# gem "github-pages", group: :jekyll_plugins +gem "github-pages", group: :jekyll_plugins # If you have any plugins, put them here! group :jekyll_plugins do gem "jekyll-feed", "~> 0.12" diff --git a/doc/Gemfile.lock b/doc/Gemfile.lock index bfb388f..d86ead3 100644 --- a/doc/Gemfile.lock +++ b/doc/Gemfile.lock @@ -1,55 +1,212 @@ GEM remote: https://rubygems.org/ specs: + activesupport (7.1.3.4) + base64 + bigdecimal + concurrent-ruby (~> 1.0, >= 1.0.2) + connection_pool (>= 2.2.5) + drb + i18n (>= 1.6, < 2) + minitest (>= 5.1) + mutex_m + tzinfo (~> 2.0) addressable (2.8.6) public_suffix (>= 2.0.2, < 6.0) + base64 (0.2.0) bigdecimal (3.1.8) + coffee-script (2.4.1) + coffee-script-source + execjs + coffee-script-source (1.12.2) colorator (1.1.0) + commonmarker (0.23.10) concurrent-ruby (1.3.3) + connection_pool (2.4.1) + dnsruby (1.72.1) + simpleidn (~> 0.2.1) + drb (2.2.1) em-websocket (0.5.3) eventmachine (>= 0.12.9) http_parser.rb (~> 0) + ethon (0.16.0) + ffi (>= 1.15.0) eventmachine (1.2.7) + execjs (2.9.1) + faraday (2.9.1) + faraday-net_http (>= 2.0, < 3.2) + faraday-net_http (3.1.0) + net-http ffi (1.17.0) ffi (1.17.0-arm64-darwin) ffi (1.17.0-x86_64-darwin) forwardable-extended (2.6.0) - google-protobuf (4.27.1) - bigdecimal - rake (>= 13) - google-protobuf (4.27.1-arm64-darwin) - bigdecimal - rake (>= 13) - google-protobuf (4.27.1-x86_64-darwin) - bigdecimal - rake (>= 13) + gemoji (4.1.0) + github-pages (231) + github-pages-health-check (= 1.18.2) + jekyll (= 3.9.5) + jekyll-avatar (= 0.8.0) + jekyll-coffeescript (= 1.2.2) + jekyll-commonmark-ghpages (= 0.4.0) + jekyll-default-layout (= 0.1.5) + jekyll-feed (= 0.17.0) + jekyll-gist (= 1.5.0) + jekyll-github-metadata (= 2.16.1) + 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.13.0) + kramdown (= 2.4.0) + kramdown-parser-gfm (= 1.1.0) + liquid (= 4.0.4) + mercenary (~> 0.3) + minima (= 2.5.1) + nokogiri (>= 1.13.6, < 2.0) + rouge (= 3.30.0) + terminal-table (~> 1.4) + github-pages-health-check (1.18.2) + addressable (~> 2.3) + dnsruby (~> 1.60) + octokit (>= 4, < 8) + public_suffix (>= 3.0, < 6.0) + typhoeus (~> 1.3) + html-pipeline (2.14.3) + activesupport (>= 2) + nokogiri (>= 1.4) http_parser.rb (0.8.0) i18n (1.14.5) concurrent-ruby (~> 1.0) - jekyll (4.3.3) + jekyll (3.9.5) addressable (~> 2.4) colorator (~> 1.0) em-websocket (~> 0.5) - i18n (~> 1.0) - jekyll-sass-converter (>= 2.0, < 4.0) + i18n (>= 0.7, < 2) + jekyll-sass-converter (~> 1.0) jekyll-watch (~> 2.0) - kramdown (~> 2.3, >= 2.3.1) - kramdown-parser-gfm (~> 1.0) + kramdown (>= 1.17, < 3) liquid (~> 4.0) - mercenary (>= 0.3.6, < 0.5) + mercenary (~> 0.3.3) pathutil (~> 0.9) - rouge (>= 3.0, < 5.0) + rouge (>= 1.7, < 4) safe_yaml (~> 1.0) - terminal-table (>= 1.8, < 4.0) - webrick (~> 1.7) + jekyll-avatar (0.8.0) + jekyll (>= 3.0, < 5.0) + jekyll-coffeescript (1.2.2) + coffee-script (~> 2.2) + coffee-script-source (~> 1.12) + jekyll-commonmark (1.4.0) + commonmarker (~> 0.22) + jekyll-commonmark-ghpages (0.4.0) + commonmarker (~> 0.23.7) + jekyll (~> 3.9.0) + jekyll-commonmark (~> 1.4.0) + rouge (>= 2.0, < 5.0) + jekyll-default-layout (0.1.5) + jekyll (>= 3.0, < 5.0) jekyll-feed (0.17.0) jekyll (>= 3.7, < 5.0) - jekyll-sass-converter (3.0.0) - sass-embedded (~> 1.54) + jekyll-gist (1.5.0) + octokit (~> 4.2) + jekyll-github-metadata (2.16.1) + jekyll (>= 3.4, < 5.0) + octokit (>= 4, < 7, != 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.13.0) + gemoji (>= 3, < 5) + html-pipeline (~> 2.2) + jekyll (>= 3.0, < 5.0) kramdown (2.4.0) rexml kramdown-parser-gfm (1.1.0) @@ -58,42 +215,56 @@ GEM listen (3.9.0) rb-fsevent (~> 0.10, >= 0.10.3) rb-inotify (~> 0.9, >= 0.9.10) - mercenary (0.4.0) + mercenary (0.3.6) + mini_portile2 (2.8.7) minima (2.5.1) jekyll (>= 3.5, < 5.0) jekyll-feed (~> 0.9) jekyll-seo-tag (~> 2.1) + minitest (5.23.1) + mutex_m (0.2.0) + net-http (0.4.1) + uri + nokogiri (1.16.6) + mini_portile2 (~> 2.8.2) + racc (~> 1.4) + nokogiri (1.16.6-arm64-darwin) + racc (~> 1.4) + nokogiri (1.16.6-x86_64-darwin) + racc (~> 1.4) + octokit (4.25.1) + faraday (>= 1, < 3) + sawyer (~> 0.9) pathutil (0.16.2) forwardable-extended (~> 2.6) public_suffix (5.0.5) - rake (13.2.1) + racc (1.8.0) rb-fsevent (0.11.2) rb-inotify (0.11.1) ffi (~> 1.0) rexml (3.3.0) strscan - rouge (4.3.0) + rouge (3.30.0) + rubyzip (2.3.2) safe_yaml (1.0.5) - sass-embedded (1.77.5) - google-protobuf (>= 3.25, < 5.0) - rake (>= 13) - sass-embedded (1.77.5-aarch64-mingw-ucrt) - google-protobuf (>= 3.25, < 5.0) - sass-embedded (1.77.5-arm64-darwin) - google-protobuf (>= 3.25, < 5.0) - sass-embedded (1.77.5-x86-cygwin) - google-protobuf (>= 3.25, < 5.0) - sass-embedded (1.77.5-x86-mingw-ucrt) - google-protobuf (>= 3.25, < 5.0) - sass-embedded (1.77.5-x86_64-cygwin) - google-protobuf (>= 3.25, < 5.0) - sass-embedded (1.77.5-x86_64-darwin) - google-protobuf (>= 3.25, < 5.0) + 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.9.2) + addressable (>= 2.3.5) + faraday (>= 0.17.3, < 3) + simpleidn (0.2.3) strscan (3.1.0) - terminal-table (3.0.2) - unicode-display_width (>= 1.1.1, < 3) - unicode-display_width (2.5.0) - webrick (1.8.1) + terminal-table (1.8.0) + unicode-display_width (~> 1.1, >= 1.1.1) + typhoeus (1.4.1) + ethon (>= 0.9.0) + tzinfo (2.0.6) + concurrent-ruby (~> 1.0) + unicode-display_width (1.8.0) + uri (0.13.0) PLATFORMS aarch64-mingw-ucrt @@ -105,8 +276,8 @@ PLATFORMS x86_64-darwin DEPENDENCIES + github-pages http_parser.rb (~> 0.6.0) - jekyll (~> 4.3.3) jekyll-feed (~> 0.12) minima (~> 2.5) tzinfo (>= 1, < 3) From 1743dc2bd237eca881473e659c2bc54c7d42c4c0 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 10:58:53 -0400 Subject: [PATCH 12/29] update --- doc/Gemfile | 2 +- doc/Gemfile.lock | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/Gemfile b/doc/Gemfile index efc9caa..6bd1845 100644 --- a/doc/Gemfile +++ b/doc/Gemfile @@ -15,7 +15,7 @@ gem "minima", "~> 2.5" gem "github-pages", group: :jekyll_plugins # If you have any plugins, put them here! group :jekyll_plugins do - gem "jekyll-feed", "~> 0.12" + gem "jekyll-feed", "~> 0.17" end # Windows and JRuby does not include zoneinfo files, so bundle the tzinfo-data gem diff --git a/doc/Gemfile.lock b/doc/Gemfile.lock index d86ead3..fa93ce7 100644 --- a/doc/Gemfile.lock +++ b/doc/Gemfile.lock @@ -278,7 +278,7 @@ PLATFORMS DEPENDENCIES github-pages http_parser.rb (~> 0.6.0) - jekyll-feed (~> 0.12) + jekyll-feed (~> 0.17) minima (~> 2.5) tzinfo (>= 1, < 3) tzinfo-data From 57708d11b7d21b81318115446440f00f31a0f0f7 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:00:12 -0400 Subject: [PATCH 13/29] update --- doc/Gemfile | 18 +----------------- doc/Gemfile.lock | 5 ----- 2 files changed, 1 insertion(+), 22 deletions(-) diff --git a/doc/Gemfile b/doc/Gemfile index 6bd1845..e14d70f 100644 --- a/doc/Gemfile +++ b/doc/Gemfile @@ -12,22 +12,6 @@ source "https://rubygems.org" gem "minima", "~> 2.5" # If you want to use GitHub Pages, remove the "gem "jekyll"" above and # uncomment the line below. To upgrade, run `bundle update github-pages`. -gem "github-pages", group: :jekyll_plugins +gem "github-pages" # If you have any plugins, put them here! -group :jekyll_plugins do - gem "jekyll-feed", "~> 0.17" -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", "< 3" - 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] diff --git a/doc/Gemfile.lock b/doc/Gemfile.lock index fa93ce7..e4cab78 100644 --- a/doc/Gemfile.lock +++ b/doc/Gemfile.lock @@ -277,12 +277,7 @@ PLATFORMS DEPENDENCIES github-pages - http_parser.rb (~> 0.6.0) - jekyll-feed (~> 0.17) minima (~> 2.5) - tzinfo (>= 1, < 3) - tzinfo-data - wdm (~> 0.1.1) BUNDLED WITH 2.5.13 From 59baa2685802a7ac80c906bc07b32d71e6817f52 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:03:31 -0400 Subject: [PATCH 14/29] test --- doc/Gemfile | 24 ++-- doc/Gemfile.lock | 270 ++++++++------------------------------------- doc/_config.yml | 4 +- doc/about.markdown | 6 - doc/index.markdown | 3 +- 5 files changed, 58 insertions(+), 249 deletions(-) delete mode 100644 doc/about.markdown diff --git a/doc/Gemfile b/doc/Gemfile index e14d70f..2085445 100644 --- a/doc/Gemfile +++ b/doc/Gemfile @@ -1,17 +1,9 @@ -source "https://rubygems.org" -# Hello! This is where you manage which Jekyll version is used to run. -# When you want to use a different version, change it below, save the -# file and run `bundle install`. Run Jekyll with `bundle exec`, like so: -# -# bundle exec jekyll serve -# -# This will help ensure the proper Jekyll version is running. -# Happy Jekylling! -#gem "jekyll", "~> 4.3.3" -# This is the default theme for new Jekyll sites. You may change this to anything you like. -gem "minima", "~> 2.5" -# If you want to use GitHub Pages, remove the "gem "jekyll"" above and -# uncomment the line below. To upgrade, run `bundle update github-pages`. -gem "github-pages" -# If you have any plugins, put them here! +# Gemfile +source 'https://rubygems.org' + +gem "jekyll", "~> 4.2" + +group :jekyll_plugins do + gem "jekyll-timeago", "~> 0.13.1" +end \ No newline at end of file diff --git a/doc/Gemfile.lock b/doc/Gemfile.lock index e4cab78..4ce0307 100644 --- a/doc/Gemfile.lock +++ b/doc/Gemfile.lock @@ -1,212 +1,53 @@ GEM remote: https://rubygems.org/ specs: - activesupport (7.1.3.4) - base64 - bigdecimal - concurrent-ruby (~> 1.0, >= 1.0.2) - connection_pool (>= 2.2.5) - drb - i18n (>= 1.6, < 2) - minitest (>= 5.1) - mutex_m - tzinfo (~> 2.0) addressable (2.8.6) public_suffix (>= 2.0.2, < 6.0) - base64 (0.2.0) bigdecimal (3.1.8) - coffee-script (2.4.1) - coffee-script-source - execjs - coffee-script-source (1.12.2) colorator (1.1.0) - commonmarker (0.23.10) concurrent-ruby (1.3.3) - connection_pool (2.4.1) - dnsruby (1.72.1) - simpleidn (~> 0.2.1) - drb (2.2.1) em-websocket (0.5.3) eventmachine (>= 0.12.9) http_parser.rb (~> 0) - ethon (0.16.0) - ffi (>= 1.15.0) eventmachine (1.2.7) - execjs (2.9.1) - faraday (2.9.1) - faraday-net_http (>= 2.0, < 3.2) - faraday-net_http (3.1.0) - net-http ffi (1.17.0) ffi (1.17.0-arm64-darwin) ffi (1.17.0-x86_64-darwin) forwardable-extended (2.6.0) - gemoji (4.1.0) - github-pages (231) - github-pages-health-check (= 1.18.2) - jekyll (= 3.9.5) - jekyll-avatar (= 0.8.0) - jekyll-coffeescript (= 1.2.2) - jekyll-commonmark-ghpages (= 0.4.0) - jekyll-default-layout (= 0.1.5) - jekyll-feed (= 0.17.0) - jekyll-gist (= 1.5.0) - jekyll-github-metadata (= 2.16.1) - 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.13.0) - kramdown (= 2.4.0) - kramdown-parser-gfm (= 1.1.0) - liquid (= 4.0.4) - mercenary (~> 0.3) - minima (= 2.5.1) - nokogiri (>= 1.13.6, < 2.0) - rouge (= 3.30.0) - terminal-table (~> 1.4) - github-pages-health-check (1.18.2) - addressable (~> 2.3) - dnsruby (~> 1.60) - octokit (>= 4, < 8) - public_suffix (>= 3.0, < 6.0) - typhoeus (~> 1.3) - html-pipeline (2.14.3) - activesupport (>= 2) - nokogiri (>= 1.4) + google-protobuf (4.27.1) + bigdecimal + rake (>= 13) + google-protobuf (4.27.1-arm64-darwin) + bigdecimal + rake (>= 13) + google-protobuf (4.27.1-x86_64-darwin) + bigdecimal + rake (>= 13) http_parser.rb (0.8.0) i18n (1.14.5) concurrent-ruby (~> 1.0) - jekyll (3.9.5) + jekyll (4.3.3) addressable (~> 2.4) colorator (~> 1.0) em-websocket (~> 0.5) - i18n (>= 0.7, < 2) - jekyll-sass-converter (~> 1.0) + i18n (~> 1.0) + jekyll-sass-converter (>= 2.0, < 4.0) jekyll-watch (~> 2.0) - kramdown (>= 1.17, < 3) + kramdown (~> 2.3, >= 2.3.1) + kramdown-parser-gfm (~> 1.0) liquid (~> 4.0) - mercenary (~> 0.3.3) + mercenary (>= 0.3.6, < 0.5) pathutil (~> 0.9) - rouge (>= 1.7, < 4) + rouge (>= 3.0, < 5.0) safe_yaml (~> 1.0) - jekyll-avatar (0.8.0) - jekyll (>= 3.0, < 5.0) - jekyll-coffeescript (1.2.2) - coffee-script (~> 2.2) - coffee-script-source (~> 1.12) - jekyll-commonmark (1.4.0) - commonmarker (~> 0.22) - jekyll-commonmark-ghpages (0.4.0) - commonmarker (~> 0.23.7) - jekyll (~> 3.9.0) - jekyll-commonmark (~> 1.4.0) - rouge (>= 2.0, < 5.0) - jekyll-default-layout (0.1.5) - jekyll (>= 3.0, < 5.0) - jekyll-feed (0.17.0) - jekyll (>= 3.7, < 5.0) - jekyll-gist (1.5.0) - octokit (~> 4.2) - jekyll-github-metadata (2.16.1) - jekyll (>= 3.4, < 5.0) - octokit (>= 4, < 7, != 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) + terminal-table (>= 1.8, < 4.0) + webrick (~> 1.7) + jekyll-sass-converter (3.0.0) + sass-embedded (~> 1.54) + jekyll-timeago (0.13.1) + mini_i18n (>= 0.8.0) jekyll-watch (2.2.1) listen (~> 3.0) - jemoji (0.13.0) - gemoji (>= 3, < 5) - html-pipeline (~> 2.2) - jekyll (>= 3.0, < 5.0) kramdown (2.4.0) rexml kramdown-parser-gfm (1.1.0) @@ -215,56 +56,39 @@ GEM listen (3.9.0) rb-fsevent (~> 0.10, >= 0.10.3) rb-inotify (~> 0.9, >= 0.9.10) - mercenary (0.3.6) - mini_portile2 (2.8.7) - minima (2.5.1) - jekyll (>= 3.5, < 5.0) - jekyll-feed (~> 0.9) - jekyll-seo-tag (~> 2.1) - minitest (5.23.1) - mutex_m (0.2.0) - net-http (0.4.1) - uri - nokogiri (1.16.6) - mini_portile2 (~> 2.8.2) - racc (~> 1.4) - nokogiri (1.16.6-arm64-darwin) - racc (~> 1.4) - nokogiri (1.16.6-x86_64-darwin) - racc (~> 1.4) - octokit (4.25.1) - faraday (>= 1, < 3) - sawyer (~> 0.9) + mercenary (0.4.0) + mini_i18n (0.9.0) pathutil (0.16.2) forwardable-extended (~> 2.6) public_suffix (5.0.5) - racc (1.8.0) + rake (13.2.1) rb-fsevent (0.11.2) rb-inotify (0.11.1) ffi (~> 1.0) rexml (3.3.0) strscan - rouge (3.30.0) - rubyzip (2.3.2) + rouge (4.3.0) 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.9.2) - addressable (>= 2.3.5) - faraday (>= 0.17.3, < 3) - simpleidn (0.2.3) + sass-embedded (1.77.5) + google-protobuf (>= 3.25, < 5.0) + rake (>= 13) + sass-embedded (1.77.5-aarch64-mingw-ucrt) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-arm64-darwin) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-x86-cygwin) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-x86-mingw-ucrt) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-x86_64-cygwin) + google-protobuf (>= 3.25, < 5.0) + sass-embedded (1.77.5-x86_64-darwin) + google-protobuf (>= 3.25, < 5.0) strscan (3.1.0) - terminal-table (1.8.0) - unicode-display_width (~> 1.1, >= 1.1.1) - typhoeus (1.4.1) - ethon (>= 0.9.0) - tzinfo (2.0.6) - concurrent-ruby (~> 1.0) - unicode-display_width (1.8.0) - uri (0.13.0) + terminal-table (3.0.2) + unicode-display_width (>= 1.1.1, < 3) + unicode-display_width (2.5.0) + webrick (1.8.1) PLATFORMS aarch64-mingw-ucrt @@ -276,8 +100,8 @@ PLATFORMS x86_64-darwin DEPENDENCIES - github-pages - minima (~> 2.5) + jekyll (~> 4.2) + jekyll-timeago (~> 0.13.1) BUNDLED WITH 2.5.13 diff --git a/doc/_config.yml b/doc/_config.yml index 1ab1755..49e9353 100644 --- a/doc/_config.yml +++ b/doc/_config.yml @@ -28,9 +28,7 @@ url: "" # the base hostname & protocol for your site, e.g. http://example.com github_username: HEPLean # Build settings -theme: minima -plugins: - - jekyll-feed + # Exclude from processing. # The following items will not be processed, by default. diff --git a/doc/about.markdown b/doc/about.markdown deleted file mode 100644 index 2e6534f..0000000 --- a/doc/about.markdown +++ /dev/null @@ -1,6 +0,0 @@ ---- -layout: page -title: About -permalink: /about/ ---- - diff --git a/doc/index.markdown b/doc/index.markdown index 3a952fa..4e3e0a5 100644 --- a/doc/index.markdown +++ b/doc/index.markdown @@ -4,5 +4,6 @@ layout: home --- -## Documentation + +# Documentation From 6c5610b104666c2751bb66cfa416b38f1ffd8587 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:05:14 -0400 Subject: [PATCH 15/29] Update docs.yml --- .github/workflows/docs.yml | 107 ++++++++++++++++++++++++------------- 1 file changed, 69 insertions(+), 38 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 8cc31f9..a1234ab 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -1,55 +1,86 @@ -# Sample workflow for building and deploying a Jekyll site to GitHub Pages -name: Deploy Jekyll with GitHub Pages dependencies preinstalled - -on: - # Runs on pushes targeting the default branch - push: +on: + push: branches: + - master - Update-versions - # Allows you to run this workflow manually from the Actions tab - workflow_dispatch: +name: Build and deploy documentation -# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages -permissions: +# borrowed from https://github.com/teorth/pfr/blob/master/.github/workflows/push.yml +permissions: contents: read pages: write id-token: write -# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued. -# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete. -concurrency: - group: "pages" - cancel-in-progress: false - -jobs: - # Build job - build: +jobs: + build_project: runs-on: ubuntu-latest + name: Build project steps: - - name: Checkout + - name: Checkout project uses: actions/checkout@v4 - - name: Setup Pages - uses: actions/configure-pages@v5 - - name: Build with Jekyll - uses: actions/jekyll-build-pages@v1 with: - source: ./doc - destination: ./doc/_site - - name: Upload artifact - uses: actions/upload-pages-artifact@v3 + fetch-depth: 0 + + - name: Print files to upstream + run: | + grep -r --files-without-match 'import HepLean' HepLean | sort > 1.txt + grep -r --files-with-match 'sorry' HepLean | sort > 2.txt + mkdir -p docs/_includes + comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/teorth\/HepLean\/blob\/master\/\1)/' > docs/_includes/files_to_upstream.md + rm 1.txt 2.txt + + # - 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 + + # - name: Build project + # run: ~/.elan/bin/lake -Kenv=dev build HepLean + + # - 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-HepLean* + # key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} + # restore-keys: | + # MathlibDoc- + + # - name: Build documentation + # run: ~/.elan/bin/lake -Kenv=dev build HepLean:docs + + #- name: Copy documentation to `docs/docs` + # run: | + # mv .lake/build/doc doc/docs + + - name: Bundle dependencies + uses: ruby/setup-ruby@v1 + with: + working-directory: doc + ruby-version: "3.1" # Not needed with a .ruby-version file + bundler-cache: true # runs 'bundle install' and caches installed gems automatically + + + - name: Bundle website + working-directory: doc + run: JEKYLL_ENV=production bundle exec jekyll build + + - name: Upload docs & blueprint artifact + uses: actions/upload-pages-artifact@v1 with: path: doc/_site - - # Deployment job - deploy: - environment: - name: github-pages - url: ${{ steps.deployment.outputs.page_url }} - runs-on: ubuntu-latest - needs: build - steps: - name: Deploy to GitHub Pages id: deployment - uses: actions/deploy-pages@v4 \ No newline at end of file + uses: actions/deploy-pages@v1 + + + From 9393262a7a362b50b939ac4e36840b07c1b17acd Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:15:31 -0400 Subject: [PATCH 16/29] update --- doc/Gemfile | 4 +--- doc/Gemfile.lock | 15 ++++++++++----- doc/_config.yml | 1 + 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/doc/Gemfile b/doc/Gemfile index 2085445..0e28c18 100644 --- a/doc/Gemfile +++ b/doc/Gemfile @@ -4,6 +4,4 @@ source 'https://rubygems.org' gem "jekyll", "~> 4.2" -group :jekyll_plugins do - gem "jekyll-timeago", "~> 0.13.1" -end \ No newline at end of file +gem "minima" \ No newline at end of file diff --git a/doc/Gemfile.lock b/doc/Gemfile.lock index 4ce0307..13af2bb 100644 --- a/doc/Gemfile.lock +++ b/doc/Gemfile.lock @@ -42,10 +42,12 @@ GEM safe_yaml (~> 1.0) terminal-table (>= 1.8, < 4.0) webrick (~> 1.7) + jekyll-feed (0.17.0) + jekyll (>= 3.7, < 5.0) jekyll-sass-converter (3.0.0) sass-embedded (~> 1.54) - jekyll-timeago (0.13.1) - mini_i18n (>= 0.8.0) + jekyll-seo-tag (2.8.0) + jekyll (>= 3.8, < 5.0) jekyll-watch (2.2.1) listen (~> 3.0) kramdown (2.4.0) @@ -57,10 +59,13 @@ GEM rb-fsevent (~> 0.10, >= 0.10.3) rb-inotify (~> 0.9, >= 0.9.10) mercenary (0.4.0) - mini_i18n (0.9.0) + minima (2.5.1) + jekyll (>= 3.5, < 5.0) + jekyll-feed (~> 0.9) + jekyll-seo-tag (~> 2.1) pathutil (0.16.2) forwardable-extended (~> 2.6) - public_suffix (5.0.5) + public_suffix (5.1.0) rake (13.2.1) rb-fsevent (0.11.2) rb-inotify (0.11.1) @@ -101,7 +106,7 @@ PLATFORMS DEPENDENCIES jekyll (~> 4.2) - jekyll-timeago (~> 0.13.1) + minima BUNDLED WITH 2.5.13 diff --git a/doc/_config.yml b/doc/_config.yml index 49e9353..a3ed2e1 100644 --- a/doc/_config.yml +++ b/doc/_config.yml @@ -28,6 +28,7 @@ url: "" # the base hostname & protocol for your site, e.g. http://example.com github_username: HEPLean # Build settings +theme: minima # Exclude from processing. From 4ba2aff12059d078de83e64018faff3a33c74b37 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:17:29 -0400 Subject: [PATCH 17/29] update --- doc/Gemfile | 2 +- doc/Gemfile.lock | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/Gemfile b/doc/Gemfile index 0e28c18..58ad681 100644 --- a/doc/Gemfile +++ b/doc/Gemfile @@ -4,4 +4,4 @@ source 'https://rubygems.org' gem "jekyll", "~> 4.2" -gem "minima" \ No newline at end of file +gem "minima", "~> 2.5.1" \ No newline at end of file diff --git a/doc/Gemfile.lock b/doc/Gemfile.lock index 13af2bb..36190ca 100644 --- a/doc/Gemfile.lock +++ b/doc/Gemfile.lock @@ -106,7 +106,7 @@ PLATFORMS DEPENDENCIES jekyll (~> 4.2) - minima + minima (~> 2.5.1) BUNDLED WITH 2.5.13 From b6f0db0e09685b06563636f66ad579f956ed079a Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:20:29 -0400 Subject: [PATCH 18/29] Update _config.yml --- doc/_config.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/_config.yml b/doc/_config.yml index a3ed2e1..2343757 100644 --- a/doc/_config.yml +++ b/doc/_config.yml @@ -29,7 +29,7 @@ github_username: HEPLean # Build settings theme: minima - +remote_theme: jekyll/minima # Exclude from processing. # The following items will not be processed, by default. From e4768007058add85b0f27e725965383dea2010a6 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:21:43 -0400 Subject: [PATCH 19/29] update --- doc/Gemfile | 2 +- doc/Gemfile.lock | 15 ++++++++++----- 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/doc/Gemfile b/doc/Gemfile index 58ad681..ec26d64 100644 --- a/doc/Gemfile +++ b/doc/Gemfile @@ -4,4 +4,4 @@ source 'https://rubygems.org' gem "jekyll", "~> 4.2" -gem "minima", "~> 2.5.1" \ No newline at end of file +gem "minima", git: "https://github.com/jekyll/minima" \ No newline at end of file diff --git a/doc/Gemfile.lock b/doc/Gemfile.lock index 36190ca..5d1f0ec 100644 --- a/doc/Gemfile.lock +++ b/doc/Gemfile.lock @@ -1,3 +1,12 @@ +GIT + remote: https://github.com/jekyll/minima + revision: 1d5286cf9a1aae34078420d183d560dd673d98b5 + specs: + minima (3.0.0.dev) + jekyll (>= 3.5, < 5.0) + jekyll-feed (~> 0.9) + jekyll-seo-tag (~> 2.1) + GEM remote: https://rubygems.org/ specs: @@ -59,10 +68,6 @@ GEM rb-fsevent (~> 0.10, >= 0.10.3) rb-inotify (~> 0.9, >= 0.9.10) mercenary (0.4.0) - minima (2.5.1) - jekyll (>= 3.5, < 5.0) - jekyll-feed (~> 0.9) - jekyll-seo-tag (~> 2.1) pathutil (0.16.2) forwardable-extended (~> 2.6) public_suffix (5.1.0) @@ -106,7 +111,7 @@ PLATFORMS DEPENDENCIES jekyll (~> 4.2) - minima (~> 2.5.1) + minima! BUNDLED WITH 2.5.13 From 9092282c582aceb639ebae5d56448bae46174d4c Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:24:05 -0400 Subject: [PATCH 20/29] Update _config.yml --- doc/_config.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/doc/_config.yml b/doc/_config.yml index 2343757..aae1005 100644 --- a/doc/_config.yml +++ b/doc/_config.yml @@ -28,7 +28,6 @@ url: "" # the base hostname & protocol for your site, e.g. http://example.com github_username: HEPLean # Build settings -theme: minima remote_theme: jekyll/minima # Exclude from processing. From af9f754ce72eb65d23f49bac933601b108d9e5dd Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:27:21 -0400 Subject: [PATCH 21/29] Update _config.yml --- doc/_config.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/_config.yml b/doc/_config.yml index aae1005..c1412f6 100644 --- a/doc/_config.yml +++ b/doc/_config.yml @@ -23,7 +23,7 @@ title: HepLean description: >- # this means to ignore newlines until "baseurl:" A project to digitalize results from high-energy physics into Lean 4. baseurl: "" # the subpath of your site, e.g. /blog -url: "" # the base hostname & protocol for your site, e.g. http://example.com +url: "https://heplean.github.io/HepLean/" # the base hostname & protocol for your site, e.g. http://example.com #twitter_username: jekyllrb github_username: HEPLean From 68ed619345d6b9bf477eb7d73d93748160a107b0 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:28:06 -0400 Subject: [PATCH 22/29] Update _config.yml --- doc/_config.yml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/doc/_config.yml b/doc/_config.yml index c1412f6..86e7de6 100644 --- a/doc/_config.yml +++ b/doc/_config.yml @@ -22,15 +22,14 @@ title: HepLean #email: your-email@example.com description: >- # this means to ignore newlines until "baseurl:" A project to digitalize results from high-energy physics into Lean 4. -baseurl: "" # the subpath of your site, e.g. /blog -url: "https://heplean.github.io/HepLean/" # the base hostname & protocol for your site, e.g. http://example.com +baseurl: "https://heplean.github.io/HepLean/" # the subpath of your site, e.g. /blog +url: "" # the base hostname & protocol for your site, e.g. http://example.com #twitter_username: jekyllrb github_username: HEPLean # Build settings -remote_theme: jekyll/minima +theme: minima -# 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". From 5f6daff2dffe9d475707b5352ce5749b743f66c3 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:29:19 -0400 Subject: [PATCH 23/29] Update _config.yml --- doc/_config.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/_config.yml b/doc/_config.yml index 86e7de6..0a45b87 100644 --- a/doc/_config.yml +++ b/doc/_config.yml @@ -22,8 +22,8 @@ title: HepLean #email: your-email@example.com description: >- # this means to ignore newlines until "baseurl:" A project to digitalize results from high-energy physics into Lean 4. -baseurl: "https://heplean.github.io/HepLean/" # the subpath of your site, e.g. /blog -url: "" # the base hostname & protocol for your site, e.g. http://example.com +baseurl: "/HepLean" # the subpath of your site, e.g. /blog +url: "https://heplean.github.io" # the base hostname & protocol for your site, e.g. http://example.com #twitter_username: jekyllrb github_username: HEPLean From 699dcf66e4c69d5c9258fa78453fc15a34f6f5ec Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:37:47 -0400 Subject: [PATCH 24/29] update-theme --- doc/Gemfile | 2 +- doc/Gemfile.lock | 17 +++-------------- doc/_config.yml | 2 +- 3 files changed, 5 insertions(+), 16 deletions(-) diff --git a/doc/Gemfile b/doc/Gemfile index ec26d64..7f834ca 100644 --- a/doc/Gemfile +++ b/doc/Gemfile @@ -4,4 +4,4 @@ source 'https://rubygems.org' gem "jekyll", "~> 4.2" -gem "minima", git: "https://github.com/jekyll/minima" \ No newline at end of file +gem "jekyll-theme-simplex" \ No newline at end of file diff --git a/doc/Gemfile.lock b/doc/Gemfile.lock index 5d1f0ec..9a42a59 100644 --- a/doc/Gemfile.lock +++ b/doc/Gemfile.lock @@ -1,12 +1,3 @@ -GIT - remote: https://github.com/jekyll/minima - revision: 1d5286cf9a1aae34078420d183d560dd673d98b5 - specs: - minima (3.0.0.dev) - jekyll (>= 3.5, < 5.0) - jekyll-feed (~> 0.9) - jekyll-seo-tag (~> 2.1) - GEM remote: https://rubygems.org/ specs: @@ -51,12 +42,10 @@ GEM safe_yaml (~> 1.0) terminal-table (>= 1.8, < 4.0) webrick (~> 1.7) - jekyll-feed (0.17.0) - jekyll (>= 3.7, < 5.0) jekyll-sass-converter (3.0.0) sass-embedded (~> 1.54) - jekyll-seo-tag (2.8.0) - jekyll (>= 3.8, < 5.0) + jekyll-theme-simplex (0.9.8.15) + jekyll (~> 4.0) jekyll-watch (2.2.1) listen (~> 3.0) kramdown (2.4.0) @@ -111,7 +100,7 @@ PLATFORMS DEPENDENCIES jekyll (~> 4.2) - minima! + jekyll-theme-simplex BUNDLED WITH 2.5.13 diff --git a/doc/_config.yml b/doc/_config.yml index 0a45b87..9d1433a 100644 --- a/doc/_config.yml +++ b/doc/_config.yml @@ -28,7 +28,7 @@ url: "https://heplean.github.io" # the base hostname & protocol for your site, e github_username: HEPLean # Build settings -theme: minima +theme: jekyll-theme-simplex # The following items will not be processed, by default. # Any item listed under the `exclude:` key here will be automatically added to From 89c1f72f86a018f0a2dc7c4734e8ba74485de356 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:39:29 -0400 Subject: [PATCH 25/29] return to minima theme --- doc/Gemfile | 2 +- doc/Gemfile.lock | 17 ++++++++++++++--- doc/_config.yml | 2 +- 3 files changed, 16 insertions(+), 5 deletions(-) diff --git a/doc/Gemfile b/doc/Gemfile index 7f834ca..ec26d64 100644 --- a/doc/Gemfile +++ b/doc/Gemfile @@ -4,4 +4,4 @@ source 'https://rubygems.org' gem "jekyll", "~> 4.2" -gem "jekyll-theme-simplex" \ No newline at end of file +gem "minima", git: "https://github.com/jekyll/minima" \ No newline at end of file diff --git a/doc/Gemfile.lock b/doc/Gemfile.lock index 9a42a59..5d1f0ec 100644 --- a/doc/Gemfile.lock +++ b/doc/Gemfile.lock @@ -1,3 +1,12 @@ +GIT + remote: https://github.com/jekyll/minima + revision: 1d5286cf9a1aae34078420d183d560dd673d98b5 + specs: + minima (3.0.0.dev) + jekyll (>= 3.5, < 5.0) + jekyll-feed (~> 0.9) + jekyll-seo-tag (~> 2.1) + GEM remote: https://rubygems.org/ specs: @@ -42,10 +51,12 @@ GEM safe_yaml (~> 1.0) terminal-table (>= 1.8, < 4.0) webrick (~> 1.7) + jekyll-feed (0.17.0) + jekyll (>= 3.7, < 5.0) jekyll-sass-converter (3.0.0) sass-embedded (~> 1.54) - jekyll-theme-simplex (0.9.8.15) - jekyll (~> 4.0) + jekyll-seo-tag (2.8.0) + jekyll (>= 3.8, < 5.0) jekyll-watch (2.2.1) listen (~> 3.0) kramdown (2.4.0) @@ -100,7 +111,7 @@ PLATFORMS DEPENDENCIES jekyll (~> 4.2) - jekyll-theme-simplex + minima! BUNDLED WITH 2.5.13 diff --git a/doc/_config.yml b/doc/_config.yml index 9d1433a..0a45b87 100644 --- a/doc/_config.yml +++ b/doc/_config.yml @@ -28,7 +28,7 @@ url: "https://heplean.github.io" # the base hostname & protocol for your site, e github_username: HEPLean # Build settings -theme: jekyll-theme-simplex +theme: minima # The following items will not be processed, by default. # Any item listed under the `exclude:` key here will be automatically added to From 8d399b576f0b91a3c1f20198f23edefe9edc294a Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:45:06 -0400 Subject: [PATCH 26/29] Update docs.yml --- .github/workflows/docs.yml | 50 +++++++++++++++++++------------------- 1 file changed, 25 insertions(+), 25 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index a1234ab..567b71b 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -30,36 +30,36 @@ jobs: comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/teorth\/HepLean\/blob\/master\/\1)/' > docs/_includes/files_to_upstream.md rm 1.txt 2.txt - # - 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: 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 + - name: Get cache + run: ~/.elan/bin/lake -Kenv=dev exe cache get || true - # - name: Build project - # run: ~/.elan/bin/lake -Kenv=dev build HepLean + - name: Build project + run: ~/.elan/bin/lake -Kenv=dev build HepLean - # - 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-HepLean* - # key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} - # restore-keys: | - # MathlibDoc- + - 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-HepLean* + key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} + restore-keys: | + MathlibDoc- - # - name: Build documentation - # run: ~/.elan/bin/lake -Kenv=dev build HepLean:docs + - name: Build documentation + run: ~/.elan/bin/lake -Kenv=dev build HepLean:docs - #- name: Copy documentation to `docs/docs` - # run: | - # mv .lake/build/doc doc/docs + - name: Copy documentation to `docs/docs` + run: | + mv .lake/build/doc doc/docs - name: Bundle dependencies uses: ruby/setup-ruby@v1 From b37b7640268a9276184b7f2c086b961e96defc9c Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 11:47:04 -0400 Subject: [PATCH 27/29] Update _config.yml --- doc/_config.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/_config.yml b/doc/_config.yml index 0a45b87..06c6ffe 100644 --- a/doc/_config.yml +++ b/doc/_config.yml @@ -19,7 +19,7 @@ # in the templates via {{ site.myvariable }}. title: HepLean -#email: your-email@example.com +email: HEPLean description: >- # this means to ignore newlines until "baseurl:" A project to digitalize results from high-energy physics into Lean 4. baseurl: "/HepLean" # the subpath of your site, e.g. /blog From 96083899fb2ecb37008d83ae4faf22e4f62b3f5c Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 12:11:11 -0400 Subject: [PATCH 28/29] docs: Update website --- doc/_config.yml | 13 ++++++++++--- doc/index.markdown | 5 ++++- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/doc/_config.yml b/doc/_config.yml index 06c6ffe..1cb2684 100644 --- a/doc/_config.yml +++ b/doc/_config.yml @@ -18,18 +18,25 @@ # You can create any custom variable you would like, and they will be accessible # in the templates via {{ site.myvariable }}. -title: HepLean -email: HEPLean +title: "HepLean: Digitalizing High-Energy Physics in Lean 4" +#email: HEPLean description: >- # this means to ignore newlines until "baseurl:" A project to digitalize results from high-energy physics into Lean 4. baseurl: "/HepLean" # the subpath of your site, e.g. /blog url: "https://heplean.github.io" # the base hostname & protocol for your site, e.g. http://example.com #twitter_username: jekyllrb -github_username: HEPLean +github_username: "HEPLean" # Build settings theme: minima +minima: + skin: solarized + +author: + name: HEPLean + email: " " + # 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". diff --git a/doc/index.markdown b/doc/index.markdown index 4e3e0a5..a3ea455 100644 --- a/doc/index.markdown +++ b/doc/index.markdown @@ -4,6 +4,9 @@ layout: home --- +[![](https://img.shields.io/badge/Documentation-blue)](https://heplean.github.io/HepLean/docs) +[![](https://img.shields.io/badge/GitHub-blue)](https://github.com/HEPLean/HepLean) -# Documentation +(This site is a work in progress. More to follow. Follow the links above to +the documentation page or GitHub.) From 26e7b44a6c295d1a3b2fae8ad17e691d6f76e356 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 15 Jun 2024 12:11:45 -0400 Subject: [PATCH 29/29] Update docs.yml --- .github/workflows/docs.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 567b71b..7485afd 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -2,7 +2,6 @@ on: push: branches: - master - - Update-versions name: Build and deploy documentation