From dcdd6dfb9b14d88b363b9c11b60ed47ac79fdd45 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 10 Aug 2022 15:15:58 +0000
Subject: [PATCH] Add a symbol export script and build artifact caching

---
 .github/workflows/lean_build.yml |  52 +++++++++++++-
 .gitpod.yml                      |   5 +-
 export.lean                      | 117 +++++++++++++++++++++++++++++++
 3 files changed, 170 insertions(+), 4 deletions(-)
 create mode 100644 export.lean

diff --git a/.github/workflows/lean_build.yml b/.github/workflows/lean_build.yml
index 2be23f4e8..ad852282f 100644
--- a/.github/workflows/lean_build.yml
+++ b/.github/workflows/lean_build.yml
@@ -9,7 +9,7 @@ jobs:
     steps:
 
     - name: checkout project
-      uses: actions/checkout@v2
+      uses: actions/checkout@v3
       with:
         fetch-depth: 0
 
@@ -17,5 +17,51 @@ jobs:
       if: github.ref == 'refs/heads/master'
       uses: leanprover-contrib/update-versions-action@master
 
-    - name: build project
-      uses: leanprover-contrib/lean-build-action@master
+    - name: Install elan
+      run: |
+        set -o pipefail
+        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+        ~/.elan/bin/lean --version
+        echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+    - name: install Python
+      uses: actions/setup-python@v1
+      with:
+        python-version: 3.8
+
+    - name: Install leanproject
+      run: |
+        python3 -m pip install --user pipx
+        python3 -m pipx ensurepath
+        source ~/.profile
+        pipx install mathlibtools
+
+    - name: Set up olean cache
+      uses: actions/cache@v3
+      with:
+        path: _cache
+        key: oleans
+
+    - name: Configure
+      run: |
+        leanpkg configure
+        leanproject get-mathlib-cache
+        leanproject get-cache --fallback=download-first || true
+
+    - name: Build
+      run: |
+        lean --json --make src | python3 _target/deps/mathlib/scripts/detect_errors.py
+
+    - name: Save olean cache
+      run: |
+        leanproject mk-cache
+
+    - name: Export symbols
+      run: |
+        leanproject mk-all
+        lean --run export.lean > lean-decl-info.tex
+
+    - uses: actions/upload-artifact@v3
+      with:
+        name: lean-decl-info
+        path: lean-decl-info.tex
diff --git a/.gitpod.yml b/.gitpod.yml
index aea699ac0..b754c6358 100644
--- a/.gitpod.yml
+++ b/.gitpod.yml
@@ -5,4 +5,7 @@ vscode:
     - jroesch.lean
 
 tasks:
-  - command: . /home/gitpod/.profile && leanproject get-mathlib-cache
+  - before: . /home/gitpod/.profile
+  - init: |
+      leanproject get-mathlib-cache
+      lean --make src
diff --git a/export.lean b/export.lean
new file mode 100644
index 000000000..1ade01640
--- /dev/null
+++ b/export.lean
@@ -0,0 +1,117 @@
+/- This file exports file and line information for use in LaTeX references. -/
+
+import all
+
+import tactic.core
+
+open tactic
+
+meta structure decl_info :=
+(name : name)
+(filename : string)
+(line : ℕ)
+
+meta def process_decl (e : environment) (d : declaration) : tactic (option decl_info) :=
+do
+  ff ← d.in_current_file | return none,
+  let decl_name := d.to_name,
+  -- allow linking to private names
+  let (internal, short_name) := if (`_private).is_prefix_of decl_name
+                    then (ff, decl_name.update_prefix decl_name.get_prefix.get_prefix)
+                    else (decl_name.is_internal ∨ d.is_auto_generated e, decl_name),
+  ff ← pure internal | return none,
+  some filename ← return (e.decl_olean decl_name) | return none,
+  let parts := filename.split (= '/'),
+  some ⟨line, _⟩ ← return (e.decl_pos decl_name) | return none,
+  return $ some ⟨short_name, filename, line⟩
+
+/-- Split a path into an optional parent component and filename -/
+def path_split (path : string) : option string × string :=
+match (path.split (= '/')).reverse with
+| [] := (none, "/")
+| [a] := (none, a)
+| (a :: as) := ("/".intercalate as.reverse, a)
+end
+
+/-- Split a lean path into a project/parent pair -/
+def project_file_split (path : string) : io (option string × string) :=
+do
+  (parent, some rest, tt) ← (io.iterate (some path, (none : option string), ff) $ λ state, do {
+    (some p, old_rest, ff) ← pure state | pure none,
+    (parent, rest) ← pure (path_split p),
+    let rest := (match old_rest with
+    | some r := rest ++ "/" ++ r
+    | none := rest
+    end),
+    some parent ← pure parent | pure (some (parent, old_rest, tt)),
+    found ← io.fs.file_exists (parent ++ "/leanpkg.toml"),
+    if !found && "/lib/lean/library".is_suffix_of p then
+      pure (some (none, some rest, tt))
+    else
+      pure (some (parent, some rest, found)) }),
+  pure (parent, rest)
+
+/-- A version of `list.map` for `io` that does not consume the whole stack -/
+def list.mmap_io {α β : Type*} (f : α → io β) (l : list α) : io (list β) :=
+do
+  (_, bs) ← io.iterate (l, ([] : list β)) (λ state, do {
+    (a :: as, bs) ← pure state | return none,
+    b ← f a,
+    return (some (as, b :: bs))
+  }),
+  pure bs
+
+/-- A version of `list.mfoldl` for `io` that does not consume the whole stack -/
+def list.mfoldl_io {s α : Type*} (f : s → α → io s) (x : s) (l : list α) : io s :=
+prod.snd <$> io.iterate (l, x) (λ state, do {
+  (a :: as, x) ← pure state | return none,
+  x' ← f x a,
+  return (some (as, x'))
+})
+
+def project_map (α : Type*) := rbmap (with_bot string) α
+
+meta def main : io unit :=
+do
+  let project_urls : project_map string := rbmap.from_list
+  [ (some "lean-ga", "https://github.com/pygae/lean-ga")
+  , (some "mathlib", "https://github.com/leanprover-community/mathlib")
+   --, (⊥, "https://github.com/leanprover-community/lean")
+    ],
+  let project_shas : project_map string := rbmap.from_list [
+    (⊥, lean.githash)
+  ],
+
+  infos ← io.run_tactic $ do
+  { e ← get_env,
+    e.get_decls.mmap (process_decl e) },
+  io.put_str_ln "\\makeatletter",
+  io.put_str_ln "",
+  io.put_str_ln "\\newcommand\\@leandef[4]{%",
+  io.put_str_ln "\\@namedef{lean-ref-proj@#1}{#2}%",
+  io.put_str_ln "\\@namedef{lean-ref-file@#1}{#3}%",
+  io.put_str_ln "\\@namedef{lean-ref-line@#1}{#4}%",
+  io.put_str_ln "}",
+  io.put_str_ln "",
+  project_shas ← infos.mfoldl_io (λ (shas : project_map string) (di : option decl_info), do
+  { some di ← pure di | pure shas,
+    (some p_dir, file) ← project_file_split di.filename | pure shas,
+    (_, p) ← pure (path_split p_dir),
+    -- skip projects without urls
+    some url ← pure (project_urls.find p) | pure shas,
+    io.put_str_ln (format!"\\@leandef{{{di.name}}}{{{p}}}{{{file}}}{{{di.line}}}").to_string,
+    none ← pure (shas.find p) | pure shas,
+    sha ← io.cmd { cmd := "git", args := ["rev-parse", "HEAD"], cwd := p_dir },
+    let sha := sha.pop_back,  -- remove trailing newline
+    pure (shas.insert p sha) })
+    project_shas,
+
+  io.put_str_ln "",
+  project_shas.to_list.mmap_io (λ sha : option string × string, do
+    some url ← pure (project_urls.find sha.1) | pure (),
+    some p ← pure sha.1 | pure (),
+    io.put_str_ln (format!"\\@namedef{{lean-ref-url@{p}}}{{{url}}}").to_string,
+    io.put_str_ln (format!"\\@namedef{{lean-ref-sha@{p}}}{{{sha.2}}}").to_string),
+
+  io.put_str_ln "",
+  io.put_str_ln "\\makeatother"