From 16554ebe68c9d58a963fcbf80c7bc5a05cad7268 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 14 Feb 2025 08:56:51 +0000 Subject: [PATCH] refactor: website --- .github/workflows/build.yml | 6 +++--- .github/workflows/docs.yml | 6 +++--- docs/TODOList.html | 2 +- docs/WebsiteInstructions.md | 10 ++++----- docs/_config.yml | 4 ++-- docs/index.markdown | 41 +++++++++++++++++++------------------ lakefile.toml | 2 +- scripts/stats.lean | 4 ++-- 8 files changed, 38 insertions(+), 37 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 4b88b24..484bcd1 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -31,7 +31,7 @@ jobs: run: | lake exe cache get - - name: build HepLean + - name: build PhysLean id: build uses: liskin/gh-problem-matcher-wrap@v3 with: @@ -43,13 +43,13 @@ jobs: run: | bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports" - - name: runLinter on HepLean + - name: runLinter on PhysLean if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }} id: lint uses: liskin/gh-problem-matcher-wrap@v3 with: linters: gcc - run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter HepLean + run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter PhysLean style_lint: name: Python based style linter diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index ac5bbb9..a76252e 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -39,7 +39,7 @@ jobs: run: lake -Kenv=dev exe cache get || true - name: Build project - run: lake -Kenv=dev build HepLean + run: lake -Kenv=dev build PhysLean - name: make TODO list run : lake exe TODO_to_yml mkFile @@ -72,13 +72,13 @@ jobs: .lake/build/doc/Std .lake/build/doc/Mathlib .lake/build/doc/declarations - !.lake/build/doc/declarations/declaration-data-HepLean* + !.lake/build/doc/declarations/declaration-data-PhysLean* key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} restore-keys: | MathlibDoc- - name: Build documentation - run: lake -Kenv=dev build HepLean:docs + run: lake -Kenv=dev build PhysLean:docs - name: Copy documentation to `docs/docs` run: | diff --git a/docs/TODOList.html b/docs/TODOList.html index cd6b5a1..f9917b8 100644 --- a/docs/TODOList.html +++ b/docs/TODOList.html @@ -3,7 +3,7 @@ layout: default ---

TODO list

-This file is created automatically using `TODO ...` commands within HepLean. +This file is created automatically using `TODO ...` commands within PhysLean. Feel free to tackle any of the items here. {% for entry in site.data.TODO %} diff --git a/docs/WebsiteInstructions.md b/docs/WebsiteInstructions.md index ebd7db7..6ad6156 100644 --- a/docs/WebsiteInstructions.md +++ b/docs/WebsiteInstructions.md @@ -1,7 +1,7 @@ -# HepLean website +# PhysLean website -The HepLean website is made using [Jeykll](https://jekyllrb.com) and is generated via the workflow +The PhysLean website is made using [Jeykll](https://jekyllrb.com) and is generated via the workflow `./.github/docs.yml`. ## Hosting the website locally @@ -9,11 +9,11 @@ The HepLean website is made using [Jeykll](https://jekyllrb.com) and is generate The installation instructions for jekyll can be found [here](https://jekyllrb.com/docs/installation/#requirements). Once jekyll is installed: -- navigate your terminal to the `./docs` directory of HepLean using e.g. `cd ./docs`. +- navigate your terminal to the `./docs` directory of PhysLean using e.g. `cd ./docs`. - Run `bundle exec jekyll serve` - Open `http://localhost:4000` in your webbrowser. -## HepLean domain +## PhysLean domain -The HepLean website is hosted at `https://heplean.com`. This domain is registered via +The PhysLean website is hosted at `https://heplean.com`. This domain is registered via squarespace domains by Joseph Tooby-Smith. diff --git a/docs/_config.yml b/docs/_config.yml index 9a29ced..eb6538b 100644 --- a/docs/_config.yml +++ b/docs/_config.yml @@ -18,10 +18,10 @@ # You can create any custom variable you would like, and they will be accessible # in the templates via {{ site.myvariable }}. -title: "HepLean: Digitalizing High-Energy Physics in Lean 4" +title: "PhysLean: Digitalizing 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. + A project to digitalize results from physics into Lean 4. baseurl: "" # the subpath of your site, e.g. /blog url: "https://heplean.com" # the base hostname & protocol for your site, e.g. http://example.com #twitter_username: jekyllrb diff --git a/docs/index.markdown b/docs/index.markdown index adc80d5..e3b88c3 100644 --- a/docs/index.markdown +++ b/docs/index.markdown @@ -12,22 +12,23 @@
Screenshot of Wick's theorem implementation in HepLean

- The above screenshot demonstrates how theorems are formalized in HepLean. + The above screenshot demonstrates how theorems are formalized in PhysLean.

-# 1. Mission of HepLean +**PhysLean was formally called HepLean** +# 1. Mission of PhysLean -The mission of HepLean is to digitalize results, meaning definitions, theorems and calculations, from physics into Lean 4 with an initial focus on high energy physics and in a way which is useful to the broad physics community. +The mission of PhysLean is to digitalize results, meaning definitions, theorems and calculations, from physics into Lean 4 with an initial focus on high energy physics and in a way which is useful to the broad physics community. -# 2. Vision of HepLean +# 2. Vision of PhysLean -**Statement**: HepLean aspires to be the definitive formal repository for physics in Lean, akin to Mathlib for mathematics, with both the Lean and physics communities behind it and a potential formal collaboration. +**Statement**: PhysLean aspires to be the definitive formal repository for physics in Lean, akin to Mathlib for mathematics, with both the Lean and physics communities behind it and a potential formal collaboration. **Detailed Vision**: - A comprehensive repository for containing fundamental definitions, theorems, and calculations from physics. @@ -37,16 +38,16 @@ The mission of HepLean is to digitalize results, meaning definitions, theorems a - An intuitive set-up that aligns with the way physicists think and work. - A large and active team, with the potential for structured, high-energy physics-style collaborations. -# 3. Values of HepLean -The three core values of HepLean are: +# 3. Values of PhysLean +The three core values of PhysLean are: -- *Welcoming*: HepLean strives to foster an environment where contributors of all academic backgrounds and experience levels feel valued, supported, and empowered to make meaningful contributions. -- *Open and Transparent*: HepLean and its outputs will always be openly accessible, freely available, and developed with transparency to benefit the broader physics and Lean communities. -- *Accessibility and Practicality*: HepLean is designed to be intuitive, well-documented, and directly useful to physicists, regardless of their familiarity with formal methods. +- *Welcoming*: PhysLean strives to foster an environment where contributors of all academic backgrounds and experience levels feel valued, supported, and empowered to make meaningful contributions. +- *Open and Transparent*: PhysLean and its outputs will always be openly accessible, freely available, and developed with transparency to benefit the broader physics and Lean communities. +- *Accessibility and Practicality*: PhysLean is designed to be intuitive, well-documented, and directly useful to physicists, regardless of their familiarity with formal methods. -# 4. Potential impact of the HepLean +# 4. Potential impact of the PhysLean -HepLean has the potential to have the following impact on the physics community: +PhysLean has the potential to have the following impact on the physics community: - Make it easier to find results. - Make it easier to automate the creation of new results using e.g. machine learning methods. - Make it easier to check papers and results for mathematical correctness. @@ -55,27 +56,27 @@ HepLean has the potential to have the following impact on the physics community: # 5. Where to learn more -You can learn more about HepLean by reading: [2405.08863](https://inspirehep.net/literature/2787050), or contacting Joseph Tooby-Smith at: joseph at heplean dot com. +You can learn more about PhysLean by reading: [2405.08863](https://inspirehep.net/literature/2787050), or contacting Joseph Tooby-Smith at: joseph at heplean dot com. # 6. How to get involved -There are a number of different ways to get involved in HepLean depending on your background. +There are a number of different ways to get involved in PhysLean depending on your background. ## 6.1 Physicists -Physicists, who are not so familiar with Lean, can contribute by adding `informal_definition` and `informal_lemma` to HepLean. These are English written statements of results which can latter be formalised. Informal definitions and lemmas already in HepLean can be found (here)[https://heplean.github.io/HepLean/InformalGraph.html]. +Physicists, who are not so familiar with Lean, can contribute by adding `informal_definition` and `informal_lemma` to PhysLean. These are English written statements of results which can latter be formalised. Informal definitions and lemmas already in PhysLean can be found (here)[https://heplean.github.io/HepLean/InformalGraph.html]. Here are some tips when writing informal results: - For big theorems, break it down into lots of smaller lemmas. -- Place the informal result in HepLean in the appropriate file. +- Place the informal result in PhysLean in the appropriate file. - Add dependencies to the `informal_definition` or `informal_lemma`. - Write the `math` field of the informal result in sufficient detail that it can be understood by someone with little other context. -Physicists can also help by improving documentation on existing results in HepLean. +Physicists can also help by improving documentation on existing results in PhysLean. ## 6.2 Mathematicians with a Lean background Mathematicians and people with a Lean background can contribute in a number of ways: -- Help by formalising `informal_definition` and `informal_lemma` which are currently in HepLean. +- Help by formalising `informal_definition` and `informal_lemma` which are currently in PhysLean. - Help by golfing and refactoring code. ## 6.3 Computer scientists with a Lean background -There are a number of metaprograms and infrastructure projects which would improve HepLean. If you need help in this direction, please get in touch. +There are a number of metaprograms and infrastructure projects which would improve PhysLean. If you need help in this direction, please get in touch. diff --git a/lakefile.toml b/lakefile.toml index 5c6d31a..0acf410 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -34,7 +34,7 @@ name = "PhysLean" #git = "https://github.com/lean-dojo/LeanCopilot.git" #rev = "v1.4.1" -# lean_exe commands defined specifically for HepLean. +# lean_exe commands defined specifically for PhysLean. [[lean_exe]] name = "check_file_imports" diff --git a/scripts/stats.lean b/scripts/stats.lean index f525109..dbab31d 100644 --- a/scripts/stats.lean +++ b/scripts/stats.lean @@ -105,10 +105,10 @@ layout: default unsafe def main (args : List String) : IO UInt32 := do let _ ← noImports - let statString ← CoreM.withImportModules #[`HepLean] (getStats).run' + let statString ← CoreM.withImportModules #[`PhysLean] (getStats).run' println! statString if "mkHTML" ∈ args then - let html ← CoreM.withImportModules #[`HepLean] (Stats.toHtml).run' + let html ← CoreM.withImportModules #[`PhysLean] (Stats.toHtml).run' let htmlFile : System.FilePath := {toString := "./docs/Stats.html"} IO.FS.writeFile htmlFile html IO.println (s!"HTML file made.")