Data by Lean

.github/workflows/deploy.yml

@@ -23,18 +23,16 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
-      - uses: denoland/setup-deno@v2
-        with:
-          deno-version: v2.x
-      - name: Generate HTML
-        run: deno run --allow-read --allow-write generate.ts
+      - uses: leanprover/lean-action@v1
+      - run: lake exe generate_pages
       - uses: actions/upload-pages-artifact@v4
         with:
           path: output
 
   deploy:
     needs: build
     runs-on: ubuntu-latest
+    if: github.ref == 'refs/heads/main'
     environment:
       name: github-pages
       url: ${{ steps.deployment.outputs.page_url }}

.gitignore

@@ -1,2 +1,5 @@
 # Output
-output/index.html
+output/*.html
+
+# Lake
+/.lake

ALF.lean

@@ -0,0 +1,2 @@
+import ALF.Authors
+import ALF.Bibliography

ALF/Authors.lean

@@ -0,0 +1,117 @@
+module
+
+public structure Author where
+  handle: String -- unique id for this namespace use handle or realname.
+  realname: Option String := none
+  github: Option String := none
+
+public section
+
+namespace Authors
+
+def «SnO2WMaN» : Author where
+  handle := "SnO2WMaN"
+  realname := "Mashu Noguchi"
+  github := "sno2wman"
+
+def «iehality» : Author where
+  handle := "Palalansoukî"
+  realname := "Shogo Saito"
+  github := "iehality"
+
+def «staroperator» : Author where
+  handle := "staroperator"
+  realname := "Dexin Zhang"
+  github := "staroperator"
+
+def «caitlindabrera» : Author where
+  handle := "caitlindabrera"
+  realname := "Caitlin D'Abrera"
+  github := "caitlindabrera"
+
+def «minchaowu» : Author where
+  handle := "minchaowu"
+  realname := "Minchao Wu"
+  github := "minchaowu"
+
+def «Rajeev Goré» : Author where
+  handle := "Rajeev Goré"
+  realname := "Rajeev Goré"
+
+def «ianshil» : Author where
+  handle := "ianshil"
+  realname := "Ian Shillito"
+  github := "ianshil"
+
+def «Revantha Ramanayake» : Author where
+  handle := "Revantha Ramanayake"
+  realname := "Revantha Ramanayake"
+
+def «znssong» : Author where
+  handle := "znssong"
+  realname := "Shuhao Song"
+  github := "znssong"
+
+def «YnirPaz» : Author where
+  handle := "YnirPaz"
+  realname := "Ynir Paz"
+  github := "YnirPaz"
+
+def «u5943321» : Author where
+  handle := "u5943321"
+  realname := "Yiming Xu"
+  github := "u5943321"
+
+def «Michael Norrish» : Author where
+  handle := "Michael Norrish"
+  realname := "Michael Norrish"
+
+def «Marco Maggesi» : Author where
+  handle := "Marco Maggesi"
+  realname := "Marco Maggesi"
+
+def «Cosimo Perini Brogi» : Author where
+  handle := "Cosimo Perini Brogi"
+  realname := "Cosimo Perini Brogi"
+
+def «ruplet» : Author where
+  handle := "ruplet"
+  realname := "Paweł Balawender"
+  github := "ruplet"
+
+def «Jesse Michael Han» : Author where
+  handle := "Jesse Michael Han"
+  realname := "Jesse Michael Han"
+
+def «Floris van Doorn» : Author where
+  handle := "Floris van Doorn"
+  realname := "Floris van Doorn"
+
+def «Janis Bailitis» : Author where
+  handle := "Janis Bailitis"
+  realname := "Janis Bailitis"
+
+def «Dominik Kirst» : Author where
+  handle := "Dominik Kirst"
+  realname := "Dominik Kirst"
+
+def «Yannick Forster» : Author where
+  handle := "Yannick Forster"
+  realname := "Yannick Forster"
+
+def «bbentzen» : Author where
+  handle := "bbentzen"
+  realname := "Bruno Bentzen"
+  github := "bbentzen"
+
+def «Huayu Guo» : Author where
+  handle := "Huayu Guo"
+  realname := "Huayu Guo"
+
+def «Dongheng Chen» : Author where
+  handle := "Dongheng Chen"
+  realname := "Dongheng Chen"
+
+end Authors
+
+end