awesome-logic-formalization/GeneratePages.lean at main · FormalizedFormalLogic/awesome-logic-formalization · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
import ALF
import MD4LeanTest.Parser

def escape (s : String) : String :=
  s.foldl
    (fun acc c =>
      acc ++
        match c with
        | '&' => "&amp;"
        | '<' => "&lt;"
        | '>' => "&gt;"
        | '"' => "&quot;"
        | '\'' => "&#39;"
        | _ => String.singleton c)
    ""

def renderAuthor (a : Author) : String :=
  let label := a.realname.getD a.handle
  match a.github with
  | some gh => s!"<a href=\"https://github.com/{gh}\" target=\"_blank\" rel=\"noopener\">{(escape label)}</a>"
  | none => (escape label)

def renderDescription (description : Option String) : String :=
  match description with
  | none => ""
  | some d =>
  let content := d.trimAscii.toString
  if content.isEmpty then "" else MD4Lean.renderHtml content |>.get!

structure RelatedLink where
  label : String
  slug : String

structure AppendixLink where
  label : String
  url : String

def renderCard
  (slug : String)
  (title : String)
  (authors : List Author)
  (tp : List TheoremProver)
  (tags : List Tag)
  (description : Option String := none)
  (related : List RelatedLink)
  (links : List AppendixLink)
  : String :=
  s!"
    <article class=\"card\" id=\"{slug}\">
      <header class=\"card-header\">
        <div class=\"card-title-row\">
          <h2 class=\"card-title\" title=\"{title}\">
            <a href=\"#{slug}\">{title}</a>
          </h2>
          <div>{String.intercalate "\n" $ tp.map $ λ t => s!"<span class=\"lang-badge {t.slug}\">{t.name}</span>"}</div>
        </div>
        <p class=\"card-authors\">{String.intercalate ", " $ authors.map renderAuthor}</p>
        <div class=\"card-tags\">{String.intercalate "\n" $ tags.map $ λ t => s!"<span class=\"tag {t.slug}\">{t.name}</span>"}</div>
      </header>
      <div class=\"card-body\">{renderDescription description}</div>
      <ul class=\"card-related\">{String.intercalate "\n" $ related.map $ λ r => s!"<li><a class=\"related-link\" href=\"#{r.slug}\">{r.label}</a></li>"}</ul>
      <footer class=\"card-footer\">
        {String.intercalate "\n" $ links.map $ λ l => s!"<a class=\"appendix-link\" href=\"{l.url}\" target=\"_blank\" rel=\"noopener\">{l.label}</a>"}
      </footer>
    </article>
  "

def renderRepoCard (r : Repository) : String :=
  renderCard
    (title := r.title)
    (slug := r.slug)
    (authors := r.authors)
    (tp := r.tp)
    (tags := r.tags)
    (description := r.description)
    (related := [])
    (links := [{ label := "GitHub", url := r.url.toUrl }])

def renderPublicationCard (p : Publication) : String :=
  renderCard
    (title := p.title)
    (slug := p.slug)
    (authors := p.authors)
    (tp := p.tp)
    (tags := p.tags)
    (description := p.abstract)
    (related := p.repositories.map $ λ r => { label := s!"{r.title}", slug := r.slug })
    (links :=
      (
        match p.doi with
        | some doi => [{ label := s!"DOI: {doi}", url := s!"https://doi.org/{doi}" }]
        | none => []
      )
    )

def main : IO Unit := do
  let outFile := "output/index.html"
  IO.FS.writeFile outFile $ s!"
    <!DOCTYPE html>
    <html lang=\"en\">
    <head>
      <meta charset=\"UTF-8\">
      <meta name=\"viewport\" content=\"width=device-width, initial-scale=1.0\">
      <meta name=\"description\" content=\"Bibliography of formalization/mechanization mainly related to mathematical logic.\" />
      <meta property=\"og:type\" content=\"website\" />
      <meta property=\"og:title\" content=\"Awesome Logic Formalization\" />
      <meta property=\"og:description\" content=\"Bibliography of formalization/mechanization mainly related to mathematical logic.\" />
      <meta property=\"og:url\" content=\"https://formalizedformallogic.github.io/awesome-logic-formalization\" />
      <meta property=\"og:image\" content=\"https://github.com/FormalizedFormalLogic.png\" />
      <meta name=\"twitter:card\" content=\"summary\" />
      <meta name=\"twitter:title\" content=\"Awesome Logic Formalization\" />
      <meta name=\"twitter:description\" content=\"Bibliography of formalization/mechanization mainly related to mathematical logic.\" />
      <link rel=\"stylesheet\" href=\"style.css\" />
      <title>Awesome Logic Formalization</title>
    </head>
    <body>
    <header class=\"site-header\">
      <h1>
        Awesome Logic Formalization
        <span class=\"entry-count\">{bibliography.length}</span>
      </h1>
      <p>
        Bibliography of formalization/mechanization mainly related to mathematical logic.
        If you want to add this, please submit a PR to our repository:
        <a href=\"https://github.com/FormalizedFormalLogic/awesome-logic-formalization\">
          https://github.com/FormalizedFormalLogic/awesome-logic-formalization
        </a>
      </p>
    </header>
    <main class=\"grid\">
      {
        String.intercalate "\n" $ bibliography.map $
          λ b => match b with
          | .repo r => renderRepoCard r
          | .pub  p => renderPublicationCard p
      }
    </main>
    </body>
    </html>
  "
  IO.println s!"Generated {outFile}"