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

Merge pull request #173 from HEPLean/informal_defs

Browse source 
Create sitemap.xml
This commit is contained in:
Joseph Tooby-Smith 2024-09-30 13:54:42 +00:00 • committed by GitHub
commit 94ceb30da4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 36 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

10
docs/assets/css/style.scss
View file

@ -1,14 +1,18 @@
---
---
@import "{{ site.theme }}";
.page-header {
background-image: linear-gradient(42deg, #59837A, #2F4456);
background-image: linear-gradient(0deg, #2C3E50, #2C3E50);
}
body {
background-color: #E1DEC2;
background-color: #fff;
font-family: serif;
}
.main-content h1,
@ -18,4 +22,4 @@ body {
.main-content h5,
.main-content h6 {
color: #2F4456;
}
}

24
docs/sitemap.xml Normal file
View file

@ -0,0 +1,24 @@
<?xml version="1.0" encoding="UTF-8"?>
<urlset xmlns="http://www.sitemaps.org/schemas/sitemap/0.9">
<!-- Homepage -->
<url>
<loc>https://heplean.github.io/HepLean/</loc>
<changefreq>daily</changefreq>
<priority>1.0</priority>
</url>
<!-- TODO list -->
<url>
<loc>https://heplean.github.io/HepLean/TODOList</loc>
<changefreq>daily</changefreq>
<priority>0.8</priority>
</url>
<!-- Informal dependency graph -->
<url>
<loc>https://heplean.github.io/HepLean/InformalGraph</loc>
<changefreq>daily</changefreq>
<priority>0.8</priority>
</url>
</urlset>

8
scripts/MetaPrograms/informal.lean
View file

@ -384,7 +384,9 @@ unsafe def toHTML (imports : Array Import) : MetaM String := do
let nodes := String.intercalate "\n" formal_nodes.toList
let informalNodes ← informal.mapM (informalToHTML)
let informalNodes := String.intercalate "\n" informalNodes.toList
let header := "
let header := "---
layout: default
---
<!DOCTYPE html>
<html>
<head>
@ -418,7 +420,7 @@ unsafe def toHTML (imports : Array Import) : MetaM String := do
<p style=\"text-align: center;\">This graph only shows informal results (gray) and their direct formal dependencies (blue).
It does not show all results formalised into HepLean.</p>
<!-- Div to display the graph -->
<div id=\"graph\" style=\"width: 100vw; height: 75vh; border: 1px solid black\"></div>
<div id=\"graph\" style=\"width: 75vw; height: 75vh; border: 1px solid black\"></div>
<!-- Hidden divs containing the text to display when nodes are clicked -->
@ -430,7 +432,7 @@ unsafe def toHTML (imports : Array Import) : MetaM String := do
<script type=\"text/javascript\">
// Load the DOT file and render the graph
d3.text(\"InformalDot.dot\").then(function(dotSrc) {
var width = window.innerWidth;
var width = 0.75 * window.innerWidth;
var height = 0.75 * window.innerHeight;
// Initialize the graphviz renderer