Merge pull request #64 from HEPLean/Update-versions

chore: Update website

.github/workflows/docs.yml

@@ -28,7 +28,8 @@ jobs:
           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
-      
+      ##################
+      # Remove this section if you don't want docs to be made
       - 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
 
@@ -59,7 +60,8 @@ jobs:
       - name: Copy documentation to `docs/docs`
         run: |
           mv .lake/build/doc doc/docs
-
+      #End Section
+      ##################
       - name: Bundle dependencies
         uses: ruby/setup-ruby@v1
         with:

HepLean/SpaceTime/LorentzGroup/Proper.lean

@@ -65,13 +65,11 @@ lemma detContinuous_eq_iff_det_eq (Λ Λ' : lorentzGroup) :
     <;> cases'  det_eq_one_or_neg_one Λ' with h2 h2
     <;> simp_all [h1, h2, h]
   rw [← toMul_zero, @Equiv.apply_eq_iff_eq] at h
-  change (0 : Fin 2) = (1 : Fin 2) at h
+  · change (0 : Fin 2) = (1 : Fin 2) at h
     simp only [Fin.isValue, zero_ne_one] at h
-  nth_rewrite 2 [← toMul_zero] at h
+  · change (1 : Fin 2) = (0 : Fin 2) at h
-  rw [@Equiv.apply_eq_iff_eq] at h
+    simp only [Fin.isValue, one_ne_zero] at h
-  change (1 : Fin 2) = (0 : Fin 2) at h
+  · intro h
-  simp [Fin.isValue, zero_ne_one] at h
-  intro h
     simp [detContinuous, h]
 
 

README.md

@@ -3,7 +3,7 @@
 [![](https://img.shields.io/badge/Read_The-Docs-green)](https://heplean.github.io/HepLean/)
 [![](https://img.shields.io/badge/PRs-Welcome-green)](https://github.com/HEPLean/HepLean/pulls)
 [![](https://img.shields.io/badge/Lean-Zulip-green)](https://leanprover.zulipchat.com)
-[![](https://img.shields.io/badge/Lean-v4.9.0_rc2-blue)](https://github.com/leanprover/lean4/releases/tag/v4.9.0-rc1)
+[![](https://img.shields.io/badge/Lean-v4.9.0--rc3-blue)](https://github.com/leanprover/lean4/releases/tag/v4.9.0-rc1)
 
 A project to digitalize high energy physics.
 

doc/Gemfile

@@ -1,7 +1,25 @@
-# Gemfile
+source "https://rubygems.org"
 
-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
 
-gem "jekyll", "~> 4.2"
+# 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
 
-gem "minima", git: "https://github.com/jekyll/minima"
+# 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"

doc/Gemfile.lock

@@ -1,64 +1,212 @@
-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:
+    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.2)
+      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)
+    gemoji (4.1.0)
-      bigdecimal
+    github-pages (231)
-      rake (>= 13)
+      github-pages-health-check (= 1.18.2)
-    google-protobuf (4.27.1-arm64-darwin)
+      jekyll (= 3.9.5)
-      bigdecimal
+      jekyll-avatar (= 0.8.0)
-      rake (>= 13)
+      jekyll-coffeescript (= 1.2.2)
-    google-protobuf (4.27.1-x86_64-darwin)
+      jekyll-commonmark-ghpages (= 0.4.0)
-      bigdecimal
+      jekyll-default-layout (= 0.1.5)
-      rake (>= 13)
+      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)
+      i18n (>= 0.7, < 2)
-      jekyll-sass-converter (>= 2.0, < 4.0)
+      jekyll-sass-converter (~> 1.0)
       jekyll-watch (~> 2.0)
-      kramdown (~> 2.3, >= 2.3.1)
+      kramdown (>= 1.17, < 3)
-      kramdown-parser-gfm (~> 1.0)
       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)
+    jekyll-avatar (0.8.0)
-      webrick (~> 1.7)
+      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)
+    jekyll-gist (1.5.0)
-      sass-embedded (~> 1.54)
+      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)
@@ -67,37 +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.24.0)
+    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.1.0)
-    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)
+    sass (3.7.4)
-      google-protobuf (>= 3.25, < 5.0)
+      sass-listen (~> 4.0.0)
-      rake (>= 13)
+    sass-listen (4.0.0)
-    sass-embedded (1.77.5-aarch64-mingw-ucrt)
+      rb-fsevent (~> 0.9, >= 0.9.4)
-      google-protobuf (>= 3.25, < 5.0)
+      rb-inotify (~> 0.9, >= 0.9.7)
-    sass-embedded (1.77.5-arm64-darwin)
+    sawyer (0.9.2)
-      google-protobuf (>= 3.25, < 5.0)
+      addressable (>= 2.3.5)
-    sass-embedded (1.77.5-x86-cygwin)
+      faraday (>= 0.17.3, < 3)
-      google-protobuf (>= 3.25, < 5.0)
+    simpleidn (0.2.3)
-    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)
+    terminal-table (1.8.0)
-      unicode-display_width (>= 1.1.1, < 3)
+      unicode-display_width (~> 1.1, >= 1.1.1)
-    unicode-display_width (2.5.0)
+    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)
     webrick (1.8.1)
 
 PLATFORMS
@@ -110,8 +277,12 @@ PLATFORMS
   x86_64-darwin
 
 DEPENDENCIES
-  jekyll (~> 4.2)
+  github-pages
-  minima!
+  http_parser.rb (~> 0.6.0)
+  tzinfo (~> 1.2)
+  tzinfo-data
+  wdm (~> 0.1.1)
+  webrick (~> 1.7)
 
 BUNDLED WITH
    2.5.13

doc/_config.yml

@@ -26,16 +26,14 @@ 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"
+repository: HEPLean/HepLean
 
 # Build settings
-theme: minima
+remote_theme: pages-themes/cayman@v0.2.0
+plugins:
+  - jekyll-remote-theme
 
-minima:
+markdown: kramdown
-  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

doc/_layouts/default.html

@@ -0,0 +1,42 @@
+<!DOCTYPE html>
+<html lang="{{ site.lang | default: "en-US" }}">
+  <head>
+    <meta charset="UTF-8">
+
+{% seo %}
+    <link rel="preconnect" href="https://fonts.gstatic.com">
+    <link rel="preload" href="https://fonts.googleapis.com/css?family=Open+Sans:400,700&display=swap" as="style" type="text/css" crossorigin>
+    <meta name="viewport" content="width=device-width, initial-scale=1">
+    <meta name="theme-color" content="#157878">
+    <meta name="apple-mobile-web-app-status-bar-style" content="black-translucent">
+    <link rel="stylesheet" href="{{ '/assets/css/style.css?v=' | append: site.github.build_revision | relative_url }}">
+    {% include head-custom.html %}
+  </head>
+  <body>
+    <a id="skip-to-content" href="#content">Skip to the content.</a>
+
+    <header class="page-header" role="banner">
+      <h1 class="project-name">{{ page.title | default: site.title | default: site.github.repository_name }}</h1>
+      <h2 class="project-tagline">{{ page.description | default: site.description | default: site.github.project_tagline }}</h2>
+      <a href="https://heplean.github.io/HepLean/docs/" class="btn">Documentation</a>
+      {% if site.github.is_project_page %}
+        <a href="{{ site.github.repository_url }}" class="btn">View on GitHub</a>
+      {% endif %}
+      {% if site.show_downloads %}
+        <a href="{{ site.github.zip_url }}" class="btn">Download .zip</a>
+        <a href="{{ site.github.tar_url }}" class="btn">Download .tar.gz</a>
+      {% endif %}
+    </header>
+
+    <main id="content" class="main-content" role="main">
+      {{ content }}
+
+      <footer class="site-footer">
+        {% if site.github.is_project_page %}
+          <span class="site-footer-owner"><a href="{{ site.github.repository_url }}">{{ site.github.repository_name }}</a> is maintained by <a href="{{ site.github.owner_url }}">{{ site.github.owner_name }}</a>.</span>
+        {% endif %}
+        <span class="site-footer-credits">This page was generated by <a href="https://pages.github.com">GitHub Pages</a>.</span>
+      </footer>
+    </main>
+  </body>
+</html>

doc/assets/css/style.scss

@@ -0,0 +1,12 @@
+---
+---
+
+@import "{{ site.theme }}";
+
+.page-header {
+  background-image: linear-gradient(42deg, #59837A, #2F4456);
+}
+
+body {
+  background-color: #E1DEC2;
+}

doc/index.markdown

@@ -1,11 +1,11 @@
 ---
 # 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
+# To see the site locally:
+# Run 
 # To view changes run: bundle exec jekyll serve
-layout: home
+#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)
 
 (This site is a work in progress. More to follow. Follow the links above to 
 the documentation page or GitHub.)

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "15d42e1a92a80d0db5ca1c12123866ba392b9d76",
+   "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474",
+   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "03092720f68254315c95a5bf249c5f2cdef717d6",
+   "rev": "cd7c51790cac1a32c321373d45700290b3e8496c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -67,7 +67,7 @@
   {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
-   "rev": "d812b96744f9b60879cbfa9c436de2b95003db2a",
+   "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -76,25 +76,16 @@
   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "rev": "ef8b0ae5d48e7d5f5d538bf8d66f6cdc7daba296",
+   "rev": "87791b59c53be80a9a000eb2bcbf61f60a27b334",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hargonix/LeanInk",
-   "type": "git",
-   "subDir": null,
-   "rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f",
-   "name": "leanInk",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "doc-gen",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "b61771aaa8f15bce5e3a38aebeb6dda487f4f29c",
+   "rev": "1f51169609a3a7c448558c3d3eb353fb355c7025",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.lean.bak

@@ -1,17 +0,0 @@
-import Lake
-open Lake DSL
-
-package «hep_lean» {
-  -- add any package configuration options here
-}
-
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
-
-@[default_target]
-lean_lib «HepLean» {
-  -- add any library configuration options here
-}
-
-meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
-require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc2
+leanprover/lean4:v4.9.0-rc3