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

Merge pull request #155 from HEPLean/informal_defs

Browse source 
feat: Add dependency graph
This commit is contained in:
Joseph Tooby-Smith 2024-09-17 07:48:33 -04:00 • committed by GitHub
commit 6773a5c824
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 193 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

10
.github/workflows/docs.yml vendored
View file

@ -21,6 +21,11 @@ jobs:
with:
fetch-depth: 0
- name: Install Graphviz
run: sudo apt-get update && sudo apt-get install -y graphviz
- name: Verify Graphviz Installation
run: dot -V
##################
# Remove this section if you don't want docs to be made
- name: Install elan
@ -40,7 +45,10 @@ jobs:
run : lake exe find_TODOs mkFile
- name: make list of informal proofs and lemmas
run : lake exe informal mkFile
run : lake exe informal mkFile mkDot
- name: Generate svg from dot
run : dot -Tsvg -o ./docs/graph.svg ./docs/InformalDot.dot
- name: Get doc cache
uses: actions/cache@v3

55
HepLean/SpaceTime/WeylFermion/Basic.lean
View file

@ -14,6 +14,9 @@ import HepLean.Meta.Informal
## The definition of Weyl fermion vector spaces.
We define the vector spaces corresponding to different types of Weyl fermions.
Note: We should prevent casting between these vector spaces.
-/
informal_definition leftHandedWeylFermion where
@ -76,10 +79,58 @@ informal_definition leftAltWeylFermionContraction where
standard basis (i.e. the dot product)."
physics :≈ "The contraction of a left-handed Weyl fermion with a right-handed Weyl fermion.
In index notation this is ψ_a φ^a."
ref :≈ "https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf"
deps :≈ [``leftHandedWeylFermion, ``altLeftHandedWeylFermion]
informal_lemma leftAltWeylFermionContraction_invariant where
math :≈ "The contraction leftAltWeylFermionContraction is invariant with respect to
the action of SL(2,C) on leftHandedWeylFermion and altLeftHandedWeylFermion."
deps :≈ [`leftAltWeylFermionContraction]
deps :≈ [``leftAltWeylFermionContraction]
informal_definition altLeftWeylFermionContraction where
math :≈ "The linear map from altLeftHandedWeylFermion ⊗ leftHandedWeylFermion to ℂ given by
summing over components of altLeftHandedWeylFermion and leftHandedWeylFermion in the
standard basis (i.e. the dot product)."
physics :≈ "The contraction of a left-handed Weyl fermion with a right-handed Weyl fermion.
In index notation this is φ^a ψ_a ."
deps :≈ [``leftHandedWeylFermion, ``altLeftHandedWeylFermion]
informal_lemma leftAltWeylFermionContraction_symm_altLeftWeylFermionContraction where
math :≈ "The linear map altLeftWeylFermionContraction is leftAltWeylFermionContraction composed
with the braiding of the tensor product."
deps :≈ [``leftAltWeylFermionContraction, ``altLeftWeylFermionContraction]
informal_lemma altLeftWeylFermionContraction_invariant where
math :≈ "The contraction altLeftWeylFermionContraction is invariant with respect to
the action of SL(2,C) on leftHandedWeylFermion and altLeftHandedWeylFermion."
deps :≈ [``altLeftWeylFermionContraction]
informal_definition rightAltWeylFermionContraction where
math :≈ "The linear map from rightHandedWeylFermion ⊗ altRightHandedWeylFermion to ℂ given by
summing over components of rightHandedWeylFermion and altRightHandedWeylFermion in the
standard basis (i.e. the dot product)."
physics :≈ "The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
In index notation this is ψ_{dot a} φ^{dot a}."
deps :≈ [``rightHandedWeylFermion, ``altRightHandedWeylFermion]
informal_lemma rightAltWeylFermionContraction_invariant where
math :≈ "The contraction rightAltWeylFermionContraction is invariant with respect to
the action of SL(2,C) on rightHandedWeylFermion and altRightHandedWeylFermion."
deps :≈ [``rightAltWeylFermionContraction]
informal_definition altRightWeylFermionContraction where
math :≈ "The linear map from altRightHandedWeylFermion ⊗ rightHandedWeylFermion to ℂ given by
summing over components of altRightHandedWeylFermion and rightHandedWeylFermion in the
standard basis (i.e. the dot product)."
physics :≈ "The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
In index notation this is φ^{dot a} ψ_{dot a}."
deps :≈ [``rightHandedWeylFermion, ``altRightHandedWeylFermion]
informal_lemma rightAltWeylFermionContraction_symm_altRightWeylFermionContraction where
math :≈ "The linear map altRightWeylFermionContraction is rightAltWeylFermionContraction composed
with the braiding of the tensor product."
deps :≈ [``rightAltWeylFermionContraction, ``altRightWeylFermionContraction]
informal_lemma altRightWeylFermionContraction_invariant where
math :≈ "The contraction altRightWeylFermionContraction is invariant with respect to
the action of SL(2,C) on rightHandedWeylFermion and altRightHandedWeylFermion."
deps :≈ [``altRightWeylFermionContraction]

160
scripts/MetaPrograms/informal.lean
View file

@ -44,13 +44,36 @@ def depToWebString (d : Name) : MetaM String := do
(mod.toString.replace "." "/") ++ ".lean"
pure s!" * [{d}]({webPath}#L{lineNo})"
/-- Takes a `ConstantInfo` corresponding to a `InformalLemma` and returns
the corresponding `InformalLemma`. -/
unsafe def constantInfoToInformalLemma (c : ConstantInfo) : MetaM InformalLemma := do
match c with
| ConstantInfo.defnInfo c =>
Lean.Meta.evalExpr' InformalLemma ``InformalLemma c.value
| _ => panic! "Passed constantInfoToInformalLemma a `ConstantInfo` that is not a `InformalLemma`"
/-- Takes a `ConstantInfo` corresponding to a `InformalDefinition` and returns
the corresponding `InformalDefinition`. -/
unsafe def constantInfoToInformalDefinition (c : ConstantInfo) : MetaM InformalDefinition := do
match c with
| ConstantInfo.defnInfo c =>
Lean.Meta.evalExpr' InformalDefinition ``InformalDefinition c.value
| _ => panic! "Passed constantInfoToInformalDefinition a
`ConstantInfo` that is not a `InformalDefinition`"
unsafe def informalDependencies (c : ConstantInfo) : MetaM (Array Name) := do
if Informal.isInformalLemma c then
let informal ← constantInfoToInformalLemma c
pure informal.dependencies.toArray
else if Informal.isInformalDef c then
let informal ← constantInfoToInformalDefinition c
pure informal.dependencies.toArray
else
pure #[]
unsafe def informalLemmaToString (c : Import × ConstantInfo) : MetaM String := do
let lineNo ← getLineNumber c.2.name
let informalLemma ←
match c.2 with
| ConstantInfo.defnInfo c =>
Lean.Meta.evalExpr' InformalLemma ``InformalLemma c.value
| _ => panic! "This should not happen"
let informalLemma ← constantInfoToInformalLemma c.2
let dep ← informalLemma.dependencies.mapM fun d => depToString d
pure s!"
Informal lemma: {informalLemma.name}
@ -63,11 +86,7 @@ Informal lemma: {informalLemma.name}
unsafe def informalLemmaToWebString (c : Import × ConstantInfo) : MetaM String := do
let lineNo ← getLineNumber c.2.name
let informalLemma ←
match c.2 with
| ConstantInfo.defnInfo c =>
Lean.Meta.evalExpr' InformalLemma ``InformalLemma c.value
| _ => panic! "This should not happen"
let informalLemma ← constantInfoToInformalLemma c.2
let dep ← informalLemma.dependencies.mapM fun d => depToWebString d
let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++
(c.1.module.toString.replace "." "/") ++ ".lean"
@ -81,11 +100,7 @@ unsafe def informalLemmaToWebString (c : Import × ConstantInfo) : MetaM String
unsafe def informalDefToString (c : Import × ConstantInfo) : MetaM String := do
let lineNo ← getLineNumber c.2.name
let informalDef ←
match c.2 with
| ConstantInfo.defnInfo c =>
Lean.Meta.evalExpr' InformalDefinition ``InformalDefinition c.value
| _ => panic! "This should not happen"
let informalDef ← constantInfoToInformalDefinition c.2
let dep ← informalDef.dependencies.mapM fun d => depToString d
pure s!"
Informal def: {informalDef.name}
@ -97,11 +112,7 @@ Informal def: {informalDef.name}
unsafe def informalDefToWebString (c : Import × ConstantInfo) : MetaM String := do
let lineNo ← getLineNumber c.2.name
let informalDef ←
match c.2 with
| ConstantInfo.defnInfo c =>
Lean.Meta.evalExpr' InformalDefinition ``InformalDefinition c.value
| _ => panic! "This should not happen"
let informalDef ← constantInfoToInformalDefinition c.2
let dep ← informalDef.dependencies.mapM fun d => depToWebString d
let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++
(c.1.module.toString.replace "." "/") ++ ".lean"
@ -141,14 +152,19 @@ There is an implicit invitation to the reader to contribute to the formalization
"
unsafe def importToString (i : Import) : MetaM String := do
/-- Takes an import and outputs the list of `ConstantInfo` corresponding
to an informal definition or lemma in that import, sorted by line number. -/
def importToInformal (i : Import) : MetaM (Array (Import × ConstantInfo)) := do
let constants ← getConst i
let constants := constants.filter (fun c => ¬ Lean.Name.isInternalDetail c.2.name)
let informalConst := constants.filter fun c => Informal.isInformal c.2
let informalConstLineNo ← informalConst.mapM fun c => getLineNumber c.2.name
let informalConstWithLineNo := informalConst.zip informalConstLineNo
let informalConstWithLineNoSort := informalConstWithLineNo.qsort (fun a b => a.2 < b.2)
let informalConst := informalConstWithLineNoSort.map (fun c => c.1)
return informalConstWithLineNoSort.map (fun c => c.1)
unsafe def importToString (i : Import) : MetaM String := do
let informalConst ← importToInformal i
let informalPrint ← (informalConst.mapM informalToString).run'
if informalPrint.isEmpty then
pure ""
@ -156,19 +172,99 @@ unsafe def importToString (i : Import) : MetaM String := do
pure ("\n\n" ++ i.module.toString ++ "\n" ++ String.intercalate "\n\n" informalPrint.toList)
unsafe def importToWebString (i : Import) : MetaM String := do
let constants ← getConst i
let constants := constants.filter (fun c => ¬ Lean.Name.isInternalDetail c.2.name)
let informalConst := constants.filter fun c => Informal.isInformal c.2
let informalConstLineNo ← informalConst.mapM fun c => getLineNumber c.2.name
let informalConstWithLineNo := informalConst.zip informalConstLineNo
let informalConstWithLineNoSort := informalConstWithLineNo.qsort (fun a b => a.2 < b.2)
let informalConst := informalConstWithLineNoSort.map (fun c => c.1)
let informalConst ← importToInformal i
let informalPrint ← (informalConst.mapM informalToWebString).run'
if informalPrint.isEmpty then
pure ""
else
pure ("\n\n## " ++ i.module.toString ++ "\n" ++ String.intercalate "\n\n" informalPrint.toList)
section dotFile
/-!
## Making the dot file for dependency graph.
-/
/-- Turns a formal definition or lemma into a node of a dot graph. -/
def formalToNode (d : Name) : MetaM String := do
let lineNo ← getLineNumber d
let mod ← getModule d
let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++
(mod.toString.replace "." "/") ++ ".lean"
pure s!"\"{d}\"[label=\"{d}\", shape=box, style=filled, fillcolor=green,
href=\"{webPath}#L{lineNo}\"]"
unsafe def informalLemmaToNode (c : Import × ConstantInfo) : MetaM String := do
let lineNo ← getLineNumber c.2.name
let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++
(c.1.module.toString.replace "." "/") ++ ".lean"
pure s!"\"{c.2.name}\"[label=\"{c.2.name}\", shape=ellipse, style=filled, fillcolor=orange,
href=\"{webPath}#L{lineNo}\"]"
unsafe def informalDefToNode (c : Import × ConstantInfo) : MetaM String := do
let lineNo ← getLineNumber c.2.name
let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++
(c.1.module.toString.replace "." "/") ++ ".lean"
pure s!"\"{c.2.name}\"[label=\"{c.2.name}\", shape=box, style=filled, fillcolor=orange,
href=\"{webPath}#L{lineNo}\"]"
unsafe def informalToNode (c : Import × ConstantInfo) : MetaM String := do
if Informal.isInformalLemma c.2 then
informalLemmaToNode c
else if Informal.isInformalDef c.2 then
informalDefToNode c
else
pure ""
unsafe def informalLemmaToEdges (c : Import × ConstantInfo) : MetaM (String) := do
let informalLemma ← constantInfoToInformalLemma c.2
let deps := informalLemma.dependencies
let edge := deps.map (fun d => s!"\"{d}\" -> \"{c.2.name}\"")
pure (String.intercalate "\n" edge)
unsafe def informalDefToEdges (c : Import × ConstantInfo) : MetaM (String) := do
let informalDef ← constantInfoToInformalDefinition c.2
let deps := informalDef.dependencies
let edge := deps.map (fun d => s!"\"{d}\" -> \"{c.2.name}\"")
pure (String.intercalate "\n" edge)
unsafe def informalToEdges (c : Import × ConstantInfo) : MetaM (String) := do
if Informal.isInformalLemma c.2 then
informalLemmaToEdges c
else if Informal.isInformalDef c.2 then
informalDefToEdges c
else
pure ""
unsafe def mkDot (imports : Array Import) : MetaM String := do
let informal ← imports.mapM importToInformal
let informal := informal.flatten
let deps ← (informal.map (fun c => c.2)).mapM informalDependencies
let deps := deps.flatten
let informal_name := informal.map (fun c => c.2.name)
let formal_deps := deps.filter (fun d => d ∉ informal_name)
let formal_nodes ← formal_deps.mapM formalToNode
let header := "strict digraph G {
bgcolor=\"lightyellow\";
label=\"Informal dependency graph for HepLean\";
labelloc=\"t\";
labeljust=\"l\";"
let footer := "}"
let nodes := String.intercalate "\n" formal_nodes.toList
let informalLemmaNodes ← informal.mapM informalToNode
let informalNodes := String.intercalate "\n" informalLemmaNodes.toList
let edges ← informal.mapM informalToEdges
let edges := String.intercalate "\n" edges.toList
pure (header ++ "\n" ++ nodes ++ "\n" ++ informalNodes ++ "\n" ++ edges ++ "\n" ++ footer)
end dotFile
/-!
## Main function
-/
unsafe def main (args : List String) : IO UInt32 := do
initSearchPath (← findSysroot)
let mods : Name := `HepLean
@ -187,4 +283,10 @@ unsafe def main (args : List String) : IO UInt32 := do
let out := String.intercalate "\n" importWebString.toList
IO.println (s!"Informal file made.")
IO.FS.writeFile fileOut (informalFileHeader ++ out)
/- Making the dot file. -/
if "mkDot" ∈ args then
let dot ← CoreM.withImportModules #[`HepLean] (mkDot imports).run'
let dotFile : System.FilePath := {toString := "./docs/InformalDot.dot"}
IO.FS.writeFile dotFile dot
IO.println (s!"Dot file made.")
pure 0