DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #261 from HEPLean/NotesEdit

Browse source 
feat: Add links to codes in notes
This commit is contained in:
Joseph Tooby-Smith 2024-12-06 06:06:04 +00:00 • committed by GitHub
commit cd6f57350c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 59 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

8
HepLean/Meta/Notes/HTMLNote.lean
View file

@ -37,7 +37,13 @@ def HTMLNote.ofFormal (name : Name) : MetaM HTMLNote := do
let line ← Name.lineNumber name
let decl ← Name.getDeclString name
let fileName ← Name.fileName name
let content := "<pre><code>" ++ decl ++ "</code></pre>"
let webAddress : String ← Name.toGitHubLink fileName line
let content :=
"<div class=\"code-block-container\">"
++ "<a href=\"" ++ webAddress ++ "\" class=\"code-button\">View/Improve</a>"
++"<pre><code>"
++ decl ++
"</code></pre></div>"
pure { content := content, fileName := fileName, line := line }
/-- An informal definition or lemma to html for a note. -/

39
HepLean/Meta/Notes/ToHTML.lean
View file

@ -99,6 +99,33 @@ def informalDefStyle : String :=
</style>
"
/-- The html styles for code button. -/
def codeButton : String := "
<style>
.code-block-container {
position: relative;
}
.code-button {
position: absolute; /* Position relative to the parent */
top: 5px; /* Distance from the top of the block */
right: 5px; /* Distance from the right of the block */
background-color: rgba(220, 53, 69, 0.4);
color: white; /* White text */
border: none; /* No border for the button */
padding: 5px 10px; /* Padding for the button */
text-decoration: none; /* Remove underline from the link */
border-radius: 5px; /* Rounded corners for the button */
font-size: 12px; /* Smaller font size */
cursor: pointer; /* Pointer cursor on hover */
}
.code-button:hover {
background-color: #0056b3;
}
</style>
"
/-- The header to the html code. -/
def headerHTML : String :=
"---
@ -106,7 +133,7 @@ layout: default
---
<!DOCTYPE html>
<html>
<head>" ++ codeBlockHTML ++ informalDefStyle ++ "</head>
<head>" ++ codeBlockHTML ++ informalDefStyle ++ codeButton ++ "</head>
</head>
<body>"
@ -120,11 +147,13 @@ def titleHTML : String :=
def leanNote : String := "
<br>
<div style=\"border: 1px solid black; padding: 10px;\">
<p>Note: These are are not ordinary notes. They are created using an automated theorem
prover called Lean. Lean formally checks definitions, theorems and proofs for correctness.
These notes are part of a much larger project called HepLean, which aims to digitalize
<p>Note: These are are not ordinary notes. They are created using an interactive theorem
prover called <a href=\"https://lean-lang.org\">Lean</a>.
Lean formally checks definitions, theorems and proofs for correctness.
These notes are part of a much larger project called
<a href=\"https://github.com/HEPLean/HepLean\">HepLean</a>., which aims to digitalize
high energy physics into Lean. Please consider contributing to this project.
<br>
<br><br>
Please provide feedback or suggestions for improvements by creating a GitHub issue
<a href=\"https://github.com/HEPLean/HepLean/issues\">here</a>.
</p>

17
HepLean/PerturbationTheory/Wick/Species.lean
View file

@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
-/
import Mathlib.Logic.Function.Basic
import HepLean.Meta.Informal.Basic
import HepLean.Meta.Notes.Basic
/-!
# Wick Species
@ -19,10 +20,26 @@ for a theory, and calculate their corresponding Feynman diagrams.
/-! TODO: There should be some sort of notion of a group action on a Wick Species. -/
namespace Wick
note "
<h2>Wick Species</h2>
To do perturbation theory for a quantum field theory, we need a quantum field theory, or
at least enough data from a quantum field theory to write down necessary constructions.
The first bit of data we need is a type of fields `𝓯`. We also need to know what fields
are dual to what other fields, for example in a complex scalar theory `φ` is dual to `φ†`.
We can encode this information in an involution `ξ : 𝓯 → 𝓯`.
<br><br>
...
<br><br>
This necessary information to do perturbation theory is encoded in a `Wick Species`, which
we define as:
"
/-- The basic structure needed to write down Wick contractions for a theory and
calculate the corresponding Feynman diagrams.
WARNING: This definition is not yet complete. -/
@[note_attr]
structure Species where
/-- The color of Field operators which appear in a theory.
One may wish to call these `half-edges`, however we restrict this terminology

1
scripts/MetaPrograms/notes.lean
View file

@ -18,6 +18,7 @@ def pertubationTheory : NoteFile where
abstract := "Notes on perturbation theory in quantum field theory."
authors := ["Joseph Tooby-Smith"]
files := [
`HepLean.PerturbationTheory.Wick.Species,
`HepLean.PerturbationTheory.Wick.Algebra,
`HepLean.PerturbationTheory.Wick.Contract
]