Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore: update to Batteries
Browse files Browse the repository at this point in the history
fgdorais committed Jul 23, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
2 parents 8591d4c + d2b1546 commit e7c8075
Showing 261 changed files with 4,417 additions and 6,946 deletions.
6 changes: 3 additions & 3 deletions .docker/gitpod/Dockerfile
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# This is the Dockerfile for leanprover/std4
# This is the Dockerfile for leanprover-community/batteries
# This file is mostly copied from [mathlib4](https://github.com/leanprover-community/mathlib4/blob/master/.docker/gitpod/Dockerfile)

# gitpod doesn't support multiple FROM statements, (or rather, you can't copy from one to another)
@@ -23,8 +23,8 @@ RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[0
# install elan
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none

# install whichever toolchain std4 is currently using
RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover/std4/main/lean-toolchain)
# install whichever toolchain batteries is currently using
RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/batteries/main/lean-toolchain)

# install neovim (for any lean.nvim user), via tarball since the appimage doesn't work for some reason, and jammy's version is ancient
RUN curl -s -L https://github.com/neovim/neovim/releases/download/stable/nvim-linux64.tar.gz | tar xzf - && sudo mv nvim-linux64 /opt/nvim
26 changes: 7 additions & 19 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
@@ -14,26 +14,14 @@ jobs:
name: Build
runs-on: ubuntu-latest
steps:
- name: install elan
run: |
set -o pipefail
curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- uses: actions/checkout@v4

- name: build std
id: build
run: lake build -Kwerror

- name: test std
if: steps.build.outcome == 'success'
run: make test

- name: lint std
if: steps.build.outcome == 'success'
run: make lint
- id: lean-action
name: build, test, and lint batteries
uses: leanprover/lean-action@v1-beta
with:
build-args: '-Kwerror'
lint-module: 'Batteries'

- name: Check that all files are imported
run: lake env lean scripts/check_imports.lean
@@ -57,7 +45,7 @@ jobs:
- name: Check for long lines
if: always()
run: |
! (find Std -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
! (find Batteries -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
- name: Check for trailing whitespace
if: always()
2 changes: 1 addition & 1 deletion .github/workflows/merge_conflicts.yml
Original file line number Diff line number Diff line change
@@ -6,7 +6,7 @@ on:

jobs:
main:
if: github.repository_owner == 'leanprover'
if: github.repository_owner == 'leanprover-community'
runs-on: ubuntu-latest
steps:
- name: check if prs are dirty
2 changes: 1 addition & 1 deletion .github/workflows/nightly_bump_toolchain.yml
Original file line number Diff line number Diff line change
@@ -8,7 +8,7 @@ on:

jobs:
update-toolchain:
if: github.repository_owner == 'leanprover'
if: github.repository_owner == 'leanprover-community'
runs-on: ubuntu-latest

steps:
14 changes: 7 additions & 7 deletions .github/workflows/nightly_detect_failure.yml
Original file line number Diff line number Diff line change
@@ -22,12 +22,12 @@ jobs:
organization-url: 'https://leanprover.zulipchat.com'
to: 'nightly-testing'
type: 'stream'
topic: 'Std status updates'
topic: 'Batteries status updates'
content: |
❌ The latest CI for Std's [`nightly-testing`](https://github.com/leanprover/std4/tree/nightly-testing) branch has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}).
❌ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}).
# Whenever `nightly-testing` passes CI,
# push it to `nightly-testing-YYYY-MM-DD` so we have a known good version of Std on that nightly release.
# push it to `nightly-testing-YYYY-MM-DD` so we have a known good version of Batteries on that nightly release.
handle_success:
if: ${{ github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.head_branch == 'nightly-testing' }}
runs-on: ubuntu-latest
@@ -72,18 +72,18 @@ jobs:
'anchor': 'newest',
'num_before': 1,
'num_after': 0,
'narrow': [{'operator': 'stream', 'operand': 'nightly-testing'}, {'operator': 'topic', 'operand': 'Std status updates'}],
'narrow': [{'operator': 'stream', 'operand': 'nightly-testing'}, {'operator': 'topic', 'operand': 'Batteries status updates'}],
'apply_markdown': False
}
response = client.get_messages(request)
messages = response['messages']
if not messages or messages[0]['content'] != "✅ The latest CI for Std's branch#nightly-testing has succeeded!":
if not messages or messages[0]['content'] != "✅ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has succeeded!":
# Post the success message
request = {
'type': 'stream',
'to': 'nightly-testing',
'topic': 'Std status updates',
'content': "✅ The latest CI for Std's branch#nightly-testing has succeeded!"
'topic': 'Batteries status updates',
'content': "✅ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has succeeded!"
}
result = client.send_message(request)
print(result)
2 changes: 1 addition & 1 deletion .github/workflows/nightly_merge_master.yml
Original file line number Diff line number Diff line change
@@ -9,7 +9,7 @@ on:

jobs:
merge-to-nightly:
if: github.repository_owner == 'leanprover'
if: github.repository_owner == 'leanprover-community'
runs-on: ubuntu-latest
steps:
- name: Checkout repository
2 changes: 1 addition & 1 deletion .vscode/copyright.code-snippets
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
{
"Copyright header for std": {
"Copyright header for batteries": {
"scope": "lean4",
"prefix": "copyright",
"body": [
110 changes: 110 additions & 0 deletions Batteries.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,110 @@
import Batteries.Classes.BEq
import Batteries.Classes.Cast
import Batteries.Classes.Order
import Batteries.Classes.RatCast
import Batteries.Classes.SatisfiesM
import Batteries.CodeAction
import Batteries.CodeAction.Attr
import Batteries.CodeAction.Basic
import Batteries.CodeAction.Deprecated
import Batteries.CodeAction.Misc
import Batteries.Control.ForInStep
import Batteries.Control.ForInStep.Basic
import Batteries.Control.ForInStep.Lemmas
import Batteries.Control.Lemmas
import Batteries.Control.Nondet.Basic
import Batteries.Data.Array
import Batteries.Data.AssocList
import Batteries.Data.BinaryHeap
import Batteries.Data.BinomialHeap
import Batteries.Data.BitVec
import Batteries.Data.Bool
import Batteries.Data.ByteArray
import Batteries.Data.Char
import Batteries.Data.DList
import Batteries.Data.Fin
import Batteries.Data.HashMap
import Batteries.Data.Int
import Batteries.Data.LazyList
import Batteries.Data.List
import Batteries.Data.MLList
import Batteries.Data.Nat
import Batteries.Data.Option
import Batteries.Data.PairingHeap
import Batteries.Data.RBMap
import Batteries.Data.Range
import Batteries.Data.Rat
import Batteries.Data.String
import Batteries.Data.Sum
import Batteries.Data.Thunk
import Batteries.Data.UInt
import Batteries.Data.UnionFind
import Batteries.Lean.AttributeExtra
import Batteries.Lean.Delaborator
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.Meta.AssertHypotheses
import Batteries.Lean.Meta.Basic
import Batteries.Lean.Meta.Clear
import Batteries.Lean.Meta.DiscrTree
import Batteries.Lean.Meta.Expr
import Batteries.Lean.Meta.Inaccessible
import Batteries.Lean.Meta.InstantiateMVars
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.SMap
import Batteries.Lean.Syntax
import Batteries.Lean.System.IO
import Batteries.Lean.TagAttribute
import Batteries.Lean.Util.EnvSearch
import Batteries.Lean.Util.Path
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
import Batteries.Tactic.Classical
import Batteries.Tactic.Congr
import Batteries.Tactic.Exact
import Batteries.Tactic.Init
import Batteries.Tactic.Instances
import Batteries.Tactic.Lemma
import Batteries.Tactic.Lint
import Batteries.Tactic.Lint.Basic
import Batteries.Tactic.Lint.Frontend
import Batteries.Tactic.Lint.Misc
import Batteries.Tactic.Lint.Simp
import Batteries.Tactic.Lint.TypeClass
import Batteries.Tactic.NoMatch
import Batteries.Tactic.OpenPrivate
import Batteries.Tactic.PermuteGoals
import Batteries.Tactic.PrintDependents
import Batteries.Tactic.PrintPrefix
import Batteries.Tactic.SeqFocus
import Batteries.Tactic.ShowUnused
import Batteries.Tactic.SqueezeScope
import Batteries.Tactic.Unreachable
import Batteries.Tactic.Where
import Batteries.Test.Internal.DummyLabelAttr
import Batteries.Util.Cache
import Batteries.Util.CheckTactic
import Batteries.Util.ExtendedBinder
import Batteries.Util.LibraryNote
import Batteries.Util.Pickle
import Batteries.Util.ProofWanted
import Batteries.WF
5 changes: 0 additions & 5 deletions Std/Classes/BEq.lean → Batteries/Classes/BEq.lean
Original file line number Diff line number Diff line change
@@ -16,8 +16,3 @@ class PartialEquivBEq (α) [BEq α] : Prop where
symm : (a : α) == b → b == a
/-- Transitivity for `BEq`. If `a == b` and `b == c` then `a == c`. -/
trans : (a : α) == b → b == c → a == c

@[simp] theorem beq_eq_false_iff_ne [BEq α] [LawfulBEq α]
(a b : α) : (a == b) = false ↔ a ≠ b := by
rw [ne_eq, ← beq_iff_eq a b]
cases a == b <;> decide
2 changes: 1 addition & 1 deletion Std/Classes/Cast.lean → Batteries/Classes/Cast.lean
Original file line number Diff line number Diff line change
@@ -3,7 +3,7 @@ Copyright (c) 2014 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Gabriel Ebner
-/
import Std.Util.LibraryNote
import Batteries.Util.LibraryNote

library_note "coercion into rings"
/--
Loading

0 comments on commit e7c8075

Please sign in to comment.