2024-07-15 09:35:36 -04:00
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
2025-02-14 08:50:24 +00:00
import PhysLean.Meta.Informal.Post
2025-02-03 11:57:28 +00:00
import Mathlib.Lean.CoreM
2024-07-15 09:35:36 -04:00
/-!
2025-02-14 08:50:24 +00:00
# PhysLean Stats
2024-07-15 09:35:36 -04:00
2025-02-14 08:50:24 +00:00
This file concerns with statistics of PhysLean.
2024-07-15 09:35:36 -04:00
-/
2025-02-14 08:50:24 +00:00
open Lean System Meta PhysLean
2024-07-15 09:35:36 -04:00
2024-11-11 11:23:27 +00:00
def getStats : MetaM String := do
let noDefsVal ← noDefs
let noLemmasVal ← noLemmas
let noImportsVal ← noImports
let noDefsNoDocVal ← noDefsNoDocString
let noLemmasNoDocVal ← noLemmasNoDocString
let noLinesVal ← noLines
2024-11-12 07:11:57 +00:00
let noInformalLemmasVal ← noInformalLemmas
2024-11-11 11:23:27 +00:00
let s := s!"
2024-11-12 07:11:57 +00:00
Number of Files 📄: {noImportsVal}
Number of lines 💻: {noLinesVal}
Number of Definitions (incl. instances): {noDefsVal - noInformalLemmasVal}
- Of which {noDefsNoDocVal} do not have doc-strings
Number of Lemmas: {noLemmasVal + noInformalLemmasVal}
- Of which {noLemmasNoDocVal} do not have doc-strings"
2024-11-11 11:23:27 +00:00
pure s
2024-07-15 09:35:36 -04:00
2024-11-11 11:23:27 +00:00
unsafe def Stats.toHtml : MetaM String := do
let noDefsVal ← noDefs
let noLemmasVal ← noLemmas
let noImportsVal ← noImports
let noDefsNoDocVal ← noDefsNoDocString
let noLemmasNoDocVal ← noLemmasNoDocString
let noLinesVal ← noLines
let noInformalDefsVal ← noInformalDefs
let noInformalLemmasVal ← noInformalLemmas
2024-11-11 11:38:33 +00:00
let noTODOsVal ← noTODOs
let noFilesWithTODOsVal ← noFilesWithTODOs
2024-11-11 11:23:27 +00:00
let header := "---
layout: default
---
<!DOCTYPE html>
<html>
<head>
2025-02-14 08:50:24 +00:00
<title>Stats for PhysLean</title>
2024-11-11 11:23:27 +00:00
<meta name=\"viewport\" content=\"width=device-width, initial-scale=1.0\">
<style>
/* Style the progress bar to be wider and take up more space */
progress {
width: 80%; /* Adjust to take up more horizontal space */
height: 30px; /* Increase height to make it wider */
appearance: none; /* Remove default browser styles */
}
2024-07-15 09:35:36 -04:00
2024-11-11 11:23:27 +00:00
/* Change the color for WebKit browsers (Chrome, Safari, etc.) */
progress::-webkit-progress-bar {
background-color: #f3f3f3; /* Background color */
border-radius: 5px;
overflow: hidden;
}
2024-07-15 09:35:36 -04:00
2024-11-11 11:23:27 +00:00
progress::-webkit-progress-value {
background-color: #157878; /* Change this to your desired color */
border-radius: 5px;
}
2024-07-15 09:35:36 -04:00
2024-11-11 11:23:27 +00:00
/* Change the color for Firefox */
progress::-moz-progress-bar {
background-color: #157878; /* Change this to your desired color */
}
</style>
</head>
<body>"
let body := s!"
2025-02-14 08:50:24 +00:00
<h1>Stats for PhysLean</h1>
2024-11-11 11:23:27 +00:00
<h3>Number of Files 📄: {noImportsVal}</h3>
<h3>Number of lines 💻: {noLinesVal}</h3>
<h3>Number of Definitions (incl. instances): {noDefsVal - noInformalLemmasVal}</h3>
<p>- Of which {noDefsVal - noDefsNoDocVal- noInformalLemmasVal} have doc-strings:</p>
<progress value=\"{noDefsVal - noDefsNoDocVal- noInformalLemmasVal}\" max=\"{noDefsVal- noInformalLemmasVal}\"></progress>
2024-11-11 11:38:33 +00:00
<p>- Of which {noDefsVal - noInformalLemmasVal - noInformalDefsVal} are not <a href=\"https://heplean.github.io/HepLean/InformalGraph.html\">informal definitions</a>:</p>
2024-11-11 11:23:27 +00:00
<progress value=\"{noDefsVal - noInformalLemmasVal - noInformalDefsVal}\" max=\"{noDefsVal - noInformalLemmasVal}\"></progress>
2024-07-15 09:35:36 -04:00
2024-11-11 11:23:27 +00:00
<h3>Number of Lemmas: {noLemmasVal + noInformalLemmasVal}</h3>
<p>- Of which {noLemmasVal - noLemmasNoDocVal + noInformalLemmasVal} have doc-strings:</p>
<progress value=\"{noLemmasVal - noLemmasNoDocVal + noInformalLemmasVal}\" max=\"{noLemmasVal + noInformalLemmasVal}\"></progress>
2024-11-11 11:38:33 +00:00
<p>- Of which {noLemmasVal} are not <a href=\"https://heplean.github.io/HepLean/InformalGraph.html\">informal lemmas</a>:</p>
2024-11-11 11:23:27 +00:00
<progress value=\"{noLemmasVal}\" max=\"{noLemmasVal + noInformalLemmasVal}\"></progress>
2024-11-11 11:38:33 +00:00
<h3>Number of <a href=\"https://heplean.github.io/HepLean/TODOList\">TODOs</a>: {noTODOsVal}</h3>
<p>- There are {noImportsVal - noFilesWithTODOsVal} (of {noImportsVal}) files which are TODO free:</p>
<progress value=\"{noImportsVal - noFilesWithTODOsVal}\" max=\"{noImportsVal}\"></progress>
2024-11-11 11:23:27 +00:00
"
let footer := "
</body>
</html>
"
pure (header ++ "\n" ++ body ++ "\n" ++ footer)
2024-07-15 09:35:36 -04:00
2024-11-11 11:23:27 +00:00
unsafe def main (args : List String) : IO UInt32 := do
let _ ← noImports
2025-02-14 08:56:51 +00:00
let statString ← CoreM.withImportModules #[`PhysLean] (getStats).run'
2024-11-11 11:23:27 +00:00
println! statString
if "mkHTML" ∈ args then
2025-02-14 08:56:51 +00:00
let html ← CoreM.withImportModules #[`PhysLean] (Stats.toHtml).run'
2024-11-11 11:23:27 +00:00
let htmlFile : System.FilePath := {toString := "./docs/Stats.html"}
IO.FS.writeFile htmlFile html
IO.println (s!"HTML file made.")
2024-07-15 09:35:36 -04:00
pure 0
