Merge branch 'master' into adaptation-13956

Author: Garmelon

.downstream/build.py

@@ -61,6 +61,9 @@ class Args:
     lint: bool
     report: Path | None
     mappings: Path | None
+    gh_repo: str | None
+    gh_run_id: str | None
+    gh_run_attempt: str | None
 
 
 def main() -> None:
@@ -83,6 +86,19 @@ def main() -> None:
         metavar="DIR",
         help="write build mappings to DIR",
     )
+    parser.add_argument(
+        "--gh-repo",
+        metavar="OWNER/NAME",
+        help="GitHub repo full name, used in the build report",
+    )
+    parser.add_argument(
+        "--gh-run-id",
+        help="GitHub Actions run ID, used to link to the run in the build report",
+    )
+    parser.add_argument(
+        "--gh-run-attempt",
+        help="GitHub Actions run attempt, appended to the run link if given",
+    )
     args = parser.parse_args(namespace=Args())
 
     report_path = None if args.report is None else args.report.resolve()
@@ -96,6 +112,9 @@ def main() -> None:
     updater = Updater()
     subrepos = updater.topo_subrepos()
 
+    commit_sha = run("git", "rev-parse", "HEAD", capture=True).stdout.strip()
+    commit_message = run("git", "log", "-1", "--format=%s", capture=True).stdout.strip()
+
     run("lake", "--version")
 
     report_build = {}
@@ -116,6 +135,14 @@ def main() -> None:
     report = []
     report.append("# Build Report")
     report.append("")
+
+    if args.gh_repo is not None:
+        commit_url = f"https://github.com/{args.gh_repo}/commit/{commit_sha}"
+        report.append(f"For commit **[{commit_message}]({commit_url})**")
+    else:
+        report.append(f"For commit **{commit_message}** (`{commit_sha}`)")
+
+    report.append("")
     report.append("| Repo | Critical | Build | Test | Lint |")
     report.append("|------|----------|-------|------|------|")
     for subrepo in subrepos:
@@ -126,6 +153,13 @@ def main() -> None:
         lint = report_lint.get(subrepo.name, Status.SKIPPED)
         report.append(f"| {name} | {critical} | {build} | {test} | {lint} |")
 
+    if args.gh_run_id is not None:
+        run_url = f"https://github.com/{args.gh_repo}/actions/runs/{args.gh_run_id}"
+        if args.gh_run_attempt is not None:
+            run_url += f"/attempts/{args.gh_run_attempt}"
+        report.append("")
+        report.append(f"[View run]({run_url})")
+
     if report_path is not None:
         report_path.write_text("\n".join(report) + "\n")
 

.downstream/downstream/updater.py

@@ -6,7 +6,7 @@
 from subprocess import CalledProcessError
 
 from downstream.merge_tree_theirs import merge_tree_theirs
-from downstream.util import Subrepo, load_subrepos, normalize_url, run
+from downstream.util import Subrepo, github_full_name, load_subrepos, normalize_url, run
 
 
 class Updater:
@@ -22,7 +22,7 @@ def __init__(self) -> None:
         self.subrepos_by_name = {r.name: r for r in self.subrepos}
         self.subrepos_by_url = {r.url: r for r in self.subrepos}
 
-    def topo_subrepos(self) -> list[Subrepo]:
+    def dep_graph(self, external: bool = False) -> dict[str, set[str]]:
         graph: dict[str, set[str]] = {}
         for subrepo in self.subrepos:
             deps: set[str] = set()
@@ -33,8 +33,13 @@ def topo_subrepos(self) -> list[Subrepo]:
                 url = normalize_url(package["url"])
                 if dep := self.subrepos_by_url.get(url):
                     deps.add(dep.name)
+                elif external:
+                    deps.add(github_full_name(url) or url)
             graph[subrepo.name] = deps
+        return graph
 
+    def topo_subrepos(self) -> list[Subrepo]:
+        graph = self.dep_graph()
         order = TopologicalSorter(graph).static_order()
         return [self.subrepos_by_name[name] for name in order]
 
@@ -65,7 +70,10 @@ def restore_tree_to(self, tree: str, path: Path) -> None:
         )
 
     def fixup_subrepo_toolchain(self, subrepo: Subrepo) -> None:
+        subrepo_toolchain = (subrepo.path / "lean-toolchain").read_text().strip()
         for file in subrepo.path.glob("**/lean-toolchain"):
+            if file.read_text().strip() != subrepo_toolchain:
+                continue
             file.unlink()
             relative = Path("lean-toolchain").relative_to(file.parent, walk_up=True)
             file.symlink_to(relative)

.downstream/downstream/util.py

@@ -29,15 +29,18 @@ def run(
     )
 
 
-def normalize_url(url: str) -> str:
-    # GitHub URLs
-    if match := re.fullmatch(
+def github_full_name(url: str) -> str | None:
+    if m := re.fullmatch(
         r"(?:https://github\.com/|git@github\.com:|ssh://git@github\.com/)([^/]+/[^/.]+?)(?:\.git)?/?",
         url,
     ):
-        full_name = match.group(1)
-        return f"https://github.com/{full_name}"
+        return m.group(1)
+    return None
+
 
+def normalize_url(url: str) -> str:
+    if full_name := github_full_name(url):
+        return f"https://github.com/{full_name}"
     return url
 
 

.downstream/graph.py

@@ -0,0 +1,87 @@
+import os
+from argparse import ArgumentParser
+from pathlib import Path
+
+from downstream.updater import Updater
+
+
+def transitive_deps(graph: dict[str, set[str]], name: str) -> set[str]:
+    result: set[str] = set()
+    for dep in graph.get(name, set()):
+        result.add(dep)
+        result |= transitive_deps(graph, dep)
+    return result
+
+
+def indirect_deps(graph: dict[str, set[str]], name: str) -> set[str]:
+    result: set[str] = set()
+    for dep in graph.get(name, set()):
+        result |= transitive_deps(graph, dep)
+    return result
+
+
+def attrs_str(**kwargs: str) -> str:
+    if not kwargs:
+        return ""
+    return " [" + " ".join(f"{k}=<{v}>" for k, v in kwargs.items()) + "]"
+
+
+class Args:
+    downstream: Path
+    prune: bool
+    external: bool
+
+
+def main() -> None:
+    parser = ArgumentParser()
+    parser.add_argument("downstream", type=Path)
+    parser.add_argument(
+        "-p",
+        "--prune",
+        action="store_true",
+        help="omit edges already implied transitively",
+    )
+    parser.add_argument(
+        "-e",
+        "--external",
+        action="store_true",
+        help="also graph dependencies not listed in repos.toml",
+    )
+    args = parser.parse_args(namespace=Args())
+
+    os.chdir(args.downstream)
+    updater = Updater()
+    graph = updater.dep_graph(external=args.external)
+
+    external = {
+        dep
+        for deps in graph.values()
+        for dep in deps
+        if dep not in updater.subrepos_by_name
+    }
+
+    print("digraph G {")
+    print("  rankdir=LR;")
+    for subrepo in sorted(updater.subrepos, key=lambda r: r.name):
+        indirect = indirect_deps(graph, subrepo.name) if args.prune else set()
+
+        label = f'{subrepo.name}<BR/><FONT POINT-SIZE="8">{subrepo.rev}</FONT>'
+        attrs = {"label": label}
+        if subrepo.critical:
+            attrs["style"] = "filled"
+            attrs["color"] = "pink"
+        print(f'  "{subrepo.name}"{attrs_str(**attrs)};')
+
+        for dep in sorted(graph[subrepo.name]):
+            comment = "// " if dep in indirect else ""
+            print(f'  {comment}"{dep}" -> "{subrepo.name}";')
+
+    for name in sorted(external):
+        attrs = {"label": name, "style": "dashed", "color": "gray", "fontcolor": "gray"}
+        print(f'  "{name}"{attrs_str(**attrs)};')
+
+    print("}")
+
+
+if __name__ == "__main__":
+    main()

.github/workflows/build-post.yml

@@ -57,7 +57,7 @@ jobs:
             echo "::endgroup::"
           done
 
-  post-report:
+  post-report-pr:
     if:
       ${{ github.event.workflow_run.conclusion != 'cancelled' &&
       github.event.workflow_run.event == 'push' &&
@@ -90,13 +90,7 @@ jobs:
           github-token: ${{ github.token }}
           run-id: ${{ github.event.workflow_run.id }}
 
-      - name: Add run link to build report
-        env:
-          RUN_URL: ${{ github.event.workflow_run.html_url }}
-        run: |
-          echo -e "\n[View run]($RUN_URL)" >> "${{ runner.temp }}/report/report.md"
-
-      - name: Post build report
+      - name: Post build report to PR
         uses: ./.downstream/actions/status-message
         with:
           app-token: ${{ steps.app-token.outputs.token }}
@@ -105,6 +99,44 @@ jobs:
           body-path: ${{ runner.temp }}/report/report.md
           marker: build-report
 
+  post-report-zulip:
+    if:
+      ${{ github.event.workflow_run.conclusion != 'cancelled' &&
+      github.event.workflow_run.event == 'push' &&
+      github.event.workflow_run.head_branch == 'master' &&
+      github.event.workflow_run.run_attempt == 1 }}
+    runs-on: ubuntu-slim
+    permissions:
+      actions: read
+    steps:
+      - name: Download build report
+        uses: actions/download-artifact@v8
+        with:
+          name: build-report
+          path: ${{ runner.temp }}/report
+          github-token: ${{ github.token }}
+          run-id: ${{ github.event.workflow_run.id }}
+
+      - name: Read build report
+        id: read-report
+        run: |
+          {
+            echo "content<<REPORT_EOF"
+            cat "${{ runner.temp }}/report/report.md"
+            echo "REPORT_EOF"
+          } >> "$GITHUB_OUTPUT"
+
+      - name: Post build report to Zulip
+        uses: zulip/github-actions-zulip/send-message@v2
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: ${{ vars.ZULIP_EMAIL }}
+          organization-url: "https://leanprover.zulipchat.com"
+          type: "stream"
+          to: "nightly-testing"
+          topic: "downstream-lean4"
+          content: ${{ steps.read-report.outputs.content }}
+
   update-branches:
     if:
       ${{ github.event.workflow_run.conclusion == 'success' &&

.github/workflows/build.yml

@@ -39,7 +39,10 @@ jobs:
         run: |
           python3 .downstream/build.py . -tl \
             --report "$RUNNER_TEMP/report.md" \
-            --mappings "$RUNNER_TEMP/mappings"
+            --mappings "$RUNNER_TEMP/mappings" \
+            --gh-repo "${{ github.repository }}" \
+            --gh-run-id "${{ github.run_id }}" \
+            --gh-run-attempt "${{ github.run_attempt }}"
 
       - name: Add report to job summary
         if: ${{ !cancelled() }} # Even if build fails

ProofWidgets4/ProofWidgets/Component/MakeEditLink.lean

@@ -4,12 +4,16 @@ public import ProofWidgets.Component.Basic
 
 public meta section
 
+/-- Returns the number of bytes required to encode this `Char` in UTF-16. -/
+private def ProofWidgets.Internal.utf16Size (c : Char) : UInt32 :=
+  if c.val ≤ 0xFFFF then 1 else 2
+
 /-- Assuming that `s` is the content of a file starting at position `p`,
 advance `p` to the end of `s`. -/
 def Lean.Lsp.Position.advance (p : Position) (s : Substring.Raw) : Position :=
   let (nLinesAfter, lastLineUtf16Sz) := s.foldl
     (init := (0, 0))
-    fun (n, l) c => if c == '\n' then (n + 1, 0) else (n, l + c.utf16Size.toNat)
+    fun (n, l) c => if c == '\n' then (n + 1, 0) else (n, l + (ProofWidgets.Internal.utf16Size c).toNat)
   {
     line := p.line + nLinesAfter
     character := (if nLinesAfter == 0 then p.character else 0) + lastLineUtf16Sz

batteries/Batteries/Control/AlternativeMonad.lean

@@ -11,6 +11,7 @@ import all Init.Control.Option
 import all Init.Control.State
 import all Init.Control.Reader
 import all Init.Control.StateRef
+public import Lean.Meta.Basic
 
 @[expose] public section
 
@@ -203,3 +204,5 @@ instance [AlternativeMonad m] : LawfulAlternativeLift m (StateRefT' ω σ m) :=
   inferInstanceAs (LawfulAlternativeLift m (ReaderT (ST.Ref ω σ) m))
 
 end StateRefT'
+
+instance : AlternativeMonad Lean.Meta.MetaM where

batteries/Batteries/Data/BinaryHeap/Basic.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, François G. Dorais
 -/
 module
+/-
+Broken against lean4#13283.
 
 public section
 
@@ -183,3 +185,4 @@ where
         simp; exact Nat.sub_lt (Batteries.BinaryHeap.size_pos_of_max e) Nat.zero_lt_one
       loop a.popMax (out.push x)
   termination_by a.size
+-/

batteries/Batteries/Data/ByteArray.lean

@@ -78,7 +78,7 @@ theorem get_extract_aux {a : ByteArray} {start stop} (h : i < (a.extract start s
 
 @[simp] theorem get_extract {a : ByteArray} {start stop} (h : i < (a.extract start stop).size) :
     (a.extract start stop)[i] = a[start+i]'(get_extract_aux h) := by
-  simp [getElem_eq_data_getElem]; rfl
+  simp [getElem_eq_data_getElem]
 
 /-! ### ofFn -/