| warning: Mathlib/Algebra/AddConstMap/Basic.lean:407:2: `@[simps]` generated lemma `AddConstMap.toEnd_apply : ⇑toEnd = DFunLike.coe` where the type of the LHS | |
| (G →+c[a✝¹, a✝¹] G) → Function.End G | |
| is not definitionally equal to the type of the RHS | |
| (G →+c[a✝¹, a✝¹] G) → G → G | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Algebra/Subalgebra/MulOpposite.lean:149:2: `@[simps]` generated lemma `Subalgebra.algEquivOpMop_apply : S.algEquivOpMop a✝ = | |
| MulOpposite.op (S.addEquivOp a✝)` where the type of the LHS | |
| (↥S.op)ᵐᵒᵖ | |
| is not definitionally equal to the type of the RHS |
ZEN大学「ZMC（ZEN Mathematics Center; ZEN数学センター）」新プロジェクト「LANA」の発表
| #!/usr/bin/env bash | |
| set -uo pipefail | |
| PASS=0 | |
| FAIL=0 | |
| run_expect_success() { | |
| echo " \$ $*" | |
| output=$("$@" 2>&1) | |
| if [ $? -eq 0 ]; then |
| #!/usr/bin/env bash | |
| set -uo pipefail | |
| PASS=0 | |
| FAIL=0 | |
| run_expect_success() { | |
| echo " \$ $*" | |
| output=$("$@" 2>&1) | |
| if [ $? -eq 0 ]; then |
| #!/usr/bin/env bash | |
| # Mark as "viewed" any file in a PR whose diff only adds/removes | |
| # "set_option backward.isDefEq.respectTransparency false in" or | |
| # "set_option backward.whnf.reducibleClassField false in". | |
| # Usage: ./mark-set-option-viewed.sh [owner/repo] [pr-number] | |
| # Requires: gh (GitHub CLI), python3 | |
| REPO="${1:-leanprover-community/mathlib4-nightly-testing}" | |
| PR="${2:-201}" |
| #!/usr/bin/env python3 | |
| """ | |
| Mathlib CI timing report. | |
| Fetches recent CI run data from GitHub Actions and produces a report showing: | |
| - Per-step timing for the Build job (in execution order) | |
| - Grouped timing summary | |
| - All jobs overview | |
| - Linear regression of build time vs cache misses |
| #!/bin/bash | |
| # Mathlib Build Benchmark on Hetzner Cloud | |
| # | |
| # Prerequisites: | |
| # 1. Install hcloud CLI: https://github.com/hetznercloud/cli/releases | |
| # macOS: brew install hcloud | |
| # Linux: apt install hcloud-cli (or download binary from releases page) | |
| # 2. export HCLOUD_TOKEN="your-api-token-here" | |
| # 3. Account needs dedicated core quota >= 48 (runs sequentially) | |
| # |
| [semireducible] AbsoluteValue.comp : AbsoluteValue → AbsoluteValue (shared: MulHom) | |
| [semireducible] AddCon.comap : AddCon → AddCon (shared: Setoid) | |
| [semireducible] AddCon.prod : AddCon → AddCon (shared: Setoid) | |
| [semireducible] AddConstEquiv.symm : AddConstEquiv → AddConstEquiv (shared: Equiv, AddConstMap) | |
| [semireducible] AddConstEquiv.trans : AddConstEquiv → AddConstEquiv (shared: Equiv, AddConstMap) | |
| [semireducible] AddEquiv.mapMatrix : AddEquiv → AddEquiv (shared: AddHom, Equiv) | |
| [semireducible] AddEquiv.prodCongr : AddEquiv → AddEquiv (shared: AddHom, Equiv) | |
| [semireducible] AddEquiv.symm : AddEquiv → AddEquiv (shared: AddHom, Equiv) | |
| [semireducible] AddEquiv.toContinuousAddEquiv : AddEquiv → ContinuousAddEquiv (shared: AddHom, Equiv) | |
| [semireducible] AddEquiv.toLinearEquiv : AddEquiv → LinearEquiv (shared: AddHom, Equiv) |
| name | mark-pr-files-viewed |
|---|---|
| description | Mark files as viewed in a GitHub PR, filtering by a predicate on the diff. Use when the user asks to mark files as viewed, dismiss trivial changes, or batch-review PR files matching a pattern. |
Use when the user asks to mark files as viewed in a GitHub PR, typically filtering by some predicate on the diff (e.g., "only whitespace changes", "only toolchain bumps", "only import changes").