Trigger CI for leanprover/lean4#5835

.github/workflows/build.yml

@@ -54,4 +54,4 @@ jobs:
       - name: Don't 'import Lean', use precise imports
         if: always()
         run: |
-          ! (find . -name "*.lean" ! -path "./test/import_lean.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')
+          ! (find . -name "*.lean" ! -path "./BatteriesTest/import_lean.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')

.github/workflows/docs-deploy.yml

@@ -0,0 +1,38 @@
+name: Deploy Docs
+
+on:
+  workflow_dispatch:
+  schedule:
+    - cron: '0 10 * * *' # daily (UTC 10:00)
+
+permissions:
+  contents: write
+
+jobs:
+  deploy-docs:
+    runs-on: ubuntu-latest
+    if: github.repository_owner == 'leanprover-community'
+    steps:
+
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install Lean
+        uses: leanprover/lean-action@v1
+        with:
+          test: false
+          lint: false
+          use-github-cache: true
+
+      - name: Build Docs
+        working-directory: docs
+        run: lake build -q Batteries:docs
+
+      - name: Deploy Docs
+        run: |
+          git config user.name "leanprover-community-batteries-bot"
+          git config user.email "[email protected]"
+          git checkout -b docs
+          git add docs/doc docs/doc-data
+          git commit -m "chore: generate docs"
+          git push origin docs --force

.github/workflows/docs-release.yml

@@ -0,0 +1,46 @@
+name: Release Docs
+
+on:
+  push:
+    tags:
+      - "v[0-9]+.[0-9]+.[0-9]+"
+      - "v[0-9]+.[0-9]+.[0-9]+-rc[0-9]+"
+
+permissions:
+  contents: write
+
+jobs:
+  build-docs:
+    runs-on: ubuntu-latest
+    if: github.repository_owner == 'leanprover-community'
+    steps:
+
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install Lean
+        uses: leanprover/lean-action@v1
+        with:
+          test: false
+          lint: false
+          use-github-cache: true
+
+      - name: Build Docs
+        working-directory: docs
+        run: lake build -q Batteries:docs
+
+      - name: Compress Docs
+        working-directory: docs
+        env:
+          TAG_NAME: ${{ github.ref_name }}
+        run: |
+          tar -czf docs-${TAG_NAME}.tar.gz doc doc-data
+          zip -rq docs-${TAG_NAME}.zip doc doc-data
+
+      - name: Release Docs
+        uses: softprops/action-gh-release@v2
+        with:
+          files: |
+            docs/docs-${{ github.ref_name }}.tar.gz
+            docs/docs-${{ github.ref_name }}.zip
+          fail_on_unmatched_files: true

.github/workflows/labels-from-status.yml

@@ -0,0 +1,62 @@
+# This workflow assigns `awaiting-review` or `WIP` labels to new PRs, and it removes
+# `awaiting-review`, `awaiting-author`, or `WIP` label from closed PRs.
+# It does not modify labels for open PRs that already have one of the `awaiting-review`,
+# `awaiting-author`, or `WIP` labels.
+
+name: Label PR from status change
+
+permissions:
+  contents: read
+  pull-requests: write
+
+on:
+  pull_request:
+    types:
+      - closed
+      - opened
+      - reopened
+      - converted_to_draft
+      - ready_for_review
+    branches:
+      - main
+
+jobs:
+  auto-label:
+    if: github.repository_owner == 'leanprover-community'
+    runs-on: ubuntu-latest
+    steps:
+
+    - uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+
+    - name: Unlabel closed PR
+      if: github.event.pull_request.state == 'closed'
+      uses: actions-ecosystem/action-remove-labels@v1
+      with:
+        labels: |
+          WIP
+          awaiting-author
+          awaiting-review
+
+    - name: Label unlabeled draft PR as WIP
+      if: |
+        github.event.pull_request.state == 'open' &&
+        github.event.pull_request.draft &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-author') &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-review') &&
+        ! contains(github.event.pull_request.labels.*.name, 'WIP')
+      uses: actions-ecosystem/action-add-labels@v1
+      with:
+        labels: WIP
+
+    - name: Label unlabeled other PR as awaiting-review
+      if: |
+        github.event.pull_request.state == 'open' &&
+        ! github.event.pull_request.draft &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-author') &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-review') &&
+        ! contains(github.event.pull_request.labels.*.name, 'WIP')
+      uses: actions-ecosystem/action-add-labels@v1
+      with:
+        labels: awaiting-review

Batteries.lean

@@ -31,19 +31,21 @@ import Batteries.Data.PairingHeap
 import Batteries.Data.RBMap
 import Batteries.Data.Range
 import Batteries.Data.Rat
+import Batteries.Data.Stream
 import Batteries.Data.String
 import Batteries.Data.UInt
 import Batteries.Data.UnionFind
 import Batteries.Data.Vector
 import Batteries.Lean.AttributeExtra
-import Batteries.Lean.Delaborator
+import Batteries.Lean.EStateM
 import Batteries.Lean.Except
 import Batteries.Lean.Expr
 import Batteries.Lean.Float
 import Batteries.Lean.HashMap
 import Batteries.Lean.HashSet
 import Batteries.Lean.IO.Process
 import Batteries.Lean.Json
+import Batteries.Lean.LawfulMonad
 import Batteries.Lean.Meta.Basic
 import Batteries.Lean.Meta.DiscrTree
 import Batteries.Lean.Meta.Expr
@@ -53,11 +55,11 @@ import Batteries.Lean.Meta.SavedState
 import Batteries.Lean.Meta.Simp
 import Batteries.Lean.Meta.UnusedNames
 import Batteries.Lean.MonadBacktrack
-import Batteries.Lean.NameMap
 import Batteries.Lean.NameMapAttribute
 import Batteries.Lean.PersistentHashMap
 import Batteries.Lean.PersistentHashSet
 import Batteries.Lean.Position
+import Batteries.Lean.SatisfiesM
 import Batteries.Lean.Syntax
 import Batteries.Lean.System.IO
 import Batteries.Lean.TagAttribute
@@ -66,7 +68,6 @@ import Batteries.Linter
 import Batteries.Linter.UnnecessarySeqFocus
 import Batteries.Linter.UnreachableTactic
 import Batteries.Logic
-import Batteries.StdDeprecations
 import Batteries.Tactic.Alias
 import Batteries.Tactic.Basic
 import Batteries.Tactic.Case
@@ -93,9 +94,6 @@ import Batteries.Tactic.SqueezeScope
 import Batteries.Tactic.Trans
 import Batteries.Tactic.Unreachable
 import Batteries.Tactic.Where
-import Batteries.Test.Internal.DummyLabelAttr
-import Batteries.Test.Internal.DummyLibraryNote
-import Batteries.Test.Internal.DummyLibraryNote2
 import Batteries.Util.Cache
 import Batteries.Util.ExtendedBinder
 import Batteries.Util.LibraryNote

Batteries/Classes/SatisfiesM.lean

@@ -1,8 +1,11 @@
 /-
 Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
+Authors: Mario Carneiro, Kim Morrison
 -/
+import Batteries.Lean.EStateM
+import Batteries.Lean.Except
+import Batteries.Tactic.Lint
 
 /-!
 ## SatisfiesM
@@ -12,6 +15,13 @@ and enables Hoare-like reasoning over monadic expressions. For example, given a
 function `f : α → m β`, to say that the return value of `f` satisfies `Q` whenever
 the input satisfies `P`, we write `∀ a, P a → SatisfiesM Q (f a)`.
 
+For any monad equipped with `MonadSatisfying m`
+one can lift `SatisfiesM` to a monadic value in `Subtype`,
+using `satisfying x h : m {a // p a}`, where `x : m α` and `h : SatisfiesM p x`.
+This includes `Option`, `ReaderT`, `StateT`, and `ExceptT`, and the Lean monad stack.
+(Although it is not entirely clear one should treat the Lean monad stack as lawful,
+even though Lean accepts this.)
+
 ## Notes
 
 `SatisfiesM` is not yet a satisfactory solution for verifying the behaviour of large scale monadic
@@ -23,7 +33,7 @@ presumably requiring more syntactic support (and smarter `do` blocks) from Lean.
 Or it may be that such a solution will look different!
 This is an open research program, and for now one should not be overly ambitious using `SatisfiesM`.
 
-In particular lemmas about pure operations on data structures in `batteries` except for `HashMap`
+In particular lemmas about pure operations on data structures in `Batteries` except for `HashMap`
 should avoid `SatisfiesM` for now, so that it is easy to migrate to other approaches in future.
 -/
 
@@ -158,25 +168,133 @@ end SatisfiesM
   ⟨by revert x; intro | .ok _, ⟨.ok ⟨_, h⟩, rfl⟩, _, rfl => exact h,
    fun h => match x with | .ok a => ⟨.ok ⟨a, h _ rfl⟩, rfl⟩ | .error e => ⟨.error e, rfl⟩⟩
 
+theorem SatisfiesM_EStateM_eq :
+    SatisfiesM (m := EStateM ε σ) p x ↔ ∀ s a s', x.run s = .ok a s' → p a := by
+  constructor
+  · rintro ⟨x, rfl⟩ s a s' h
+    match w : x.run s with
+    | .ok a s' => simp at h; exact h.1
+    | .error e s' => simp [w] at h
+  · intro w
+    refine ⟨?_, ?_⟩
+    · intro s
+      match q : x.run s with
+      | .ok a s' => exact .ok ⟨a, w s a s' q⟩ s'
+      | .error e s' => exact .error e s'
+    · ext s
+      rw [EStateM.run_map, EStateM.run]
+      split <;> simp_all
+
 @[simp] theorem SatisfiesM_ReaderT_eq [Monad m] :
-    SatisfiesM (m := ReaderT ρ m) p x ↔ ∀ s, SatisfiesM p (x s) :=
+    SatisfiesM (m := ReaderT ρ m) p x ↔ ∀ s, SatisfiesM p (x.run s) :=
   (exists_congr fun a => by exact ⟨fun eq _ => eq ▸ rfl, funext⟩).trans Classical.skolem.symm
 
 theorem SatisfiesM_StateRefT_eq [Monad m] :
-    SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) := by simp
+    SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) := by simp [ReaderT.run]
 
 @[simp] theorem SatisfiesM_StateT_eq [Monad m] [LawfulMonad m] :
-    SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x s) := by
+    SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x.run s) := by
+  change SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x s)
   refine .trans ⟨fun ⟨f, eq⟩ => eq ▸ ?_, fun ⟨f, h⟩ => ?_⟩ Classical.skolem.symm
   · refine ⟨fun s => (fun ⟨⟨a, h⟩, s'⟩ => ⟨⟨a, s'⟩, h⟩) <$> f s, fun s => ?_⟩
     rw [← comp_map, map_eq_pure_bind]; rfl
   · refine ⟨fun s => (fun ⟨⟨a, s'⟩, h⟩ => ⟨⟨a, h⟩, s'⟩) <$> f s, funext fun s => ?_⟩
     show _ >>= _ = _; simp [← h]
 
 @[simp] theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] :
-    SatisfiesM (m := ExceptT ρ m) (α := α) p x ↔ SatisfiesM (m := m) (∀ a, · = .ok a → p a) x := by
+    SatisfiesM (m := ExceptT ρ m) (α := α) p x ↔
+      SatisfiesM (m := m) (∀ a, · = .ok a → p a) x.run := by
+  change _ ↔ SatisfiesM (m := m) (∀ a, · = .ok a → p a) x
   refine ⟨fun ⟨f, eq⟩ => eq ▸ ?_, fun ⟨f, eq⟩ => eq ▸ ?_⟩
   · exists (fun | .ok ⟨a, h⟩ => ⟨.ok a, fun | _, rfl => h⟩ | .error e => ⟨.error e, nofun⟩) <$> f
     show _ = _ >>= _; rw [← comp_map, map_eq_pure_bind]; congr; funext a; cases a <;> rfl
   · exists ((fun | ⟨.ok a, h⟩ => .ok ⟨a, h _ rfl⟩ | ⟨.error e, _⟩ => .error e) <$> f : m _)
     show _ >>= _ = _; simp [← comp_map, ← bind_pure_comp]; congr; funext ⟨a, h⟩; cases a <;> rfl
+
+/--
+If a monad has `MonadSatisfying m`, then we can lift a `h : SatisfiesM (m := m) p x` predicate
+to monadic value `satisfying x p : m { x // p x }`.
+
+Reader, state, and exception monads have `MonadSatisfying` instances if the base monad does.
+-/
+class MonadSatisfying (m : Type u → Type v) [Functor m] [LawfulFunctor m] where
+  /-- Lift a `SatisfiesM` predicate to a monadic value. -/
+  satisfying {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) : m {a // p a}
+  /-- The value of the lifted monadic value is equal to the original monadic value. -/
+  val_eq {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) : Subtype.val <$> satisfying h = x
+
+export MonadSatisfying (satisfying)
+
+namespace MonadSatisfying
+
+instance : MonadSatisfying Id where
+  satisfying {α p x} h := ⟨x, by obtain ⟨⟨_, h⟩, rfl⟩ := h; exact h⟩
+  val_eq {α p x} h := rfl
+
+instance : MonadSatisfying Option where
+  satisfying {α p x?} h :=
+    have h' := SatisfiesM_Option_eq.mp h
+    match x? with
+    | none => none
+    | some x => some ⟨x, h' x rfl⟩
+  val_eq {α p x?} h := by cases x? <;> simp
+
+instance : MonadSatisfying (Except ε) where
+  satisfying {α p x?} h :=
+    have h' := SatisfiesM_Except_eq.mp h
+    match x? with
+    | .ok x => .ok ⟨x, h' x rfl⟩
+    | .error e => .error e
+  val_eq {α p x?} h := by cases x? <;> simp
+
+-- This will be redundant after nightly-2024-11-08.
+attribute [ext] ReaderT.ext
+
+instance [Monad m] [LawfulMonad m][MonadSatisfying m] : MonadSatisfying (ReaderT ρ m) where
+  satisfying {α p x} h :=
+    have h' := SatisfiesM_ReaderT_eq.mp h
+    fun r => satisfying (h' r)
+  val_eq {α p x} h := by
+    have h' := SatisfiesM_ReaderT_eq.mp h
+    ext r
+    rw [ReaderT.run_map, ← MonadSatisfying.val_eq (h' r)]
+    rfl
+
+instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateRefT' ω σ m) :=
+  inferInstanceAs <| MonadSatisfying (ReaderT _ _)
+
+-- This will be redundant after nightly-2024-11-08.
+attribute [ext] StateT.ext
+
+instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateT ρ m) where
+  satisfying {α p x} h :=
+    have h' := SatisfiesM_StateT_eq.mp h
+    fun r => (fun ⟨⟨a, r'⟩, h⟩ => ⟨⟨a, h⟩, r'⟩) <$> satisfying (h' r)
+  val_eq {α p x} h := by
+    have h' := SatisfiesM_StateT_eq.mp h
+    ext r
+    rw [← MonadSatisfying.val_eq (h' r), StateT.run_map]
+    simp [StateT.run]
+
+instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (ExceptT ε m) where
+  satisfying {α p x} h :=
+    let x' := satisfying (SatisfiesM_ExceptT_eq.mp h)
+    ExceptT.mk ((fun ⟨y, w⟩ => y.pmap fun a h => ⟨a, w _ h⟩) <$> x')
+  val_eq {α p x} h:= by
+    ext
+    rw [← MonadSatisfying.val_eq (SatisfiesM_ExceptT_eq.mp h)]
+    simp
+
+instance : MonadSatisfying (EStateM ε σ) where
+  satisfying {α p x} h :=
+    have h' := SatisfiesM_EStateM_eq.mp h
+    fun s => match w : x.run s with
+    | .ok a s' => .ok ⟨a, h' s a s' w⟩ s'
+    | .error e s' => .error e s'
+  val_eq {α p x} h := by
+    ext s
+    rw [EStateM.run_map, EStateM.run]
+    simp only
+    split <;> simp_all
+
+end MonadSatisfying