alreadydone

Q: What is causing CI to hang after completing the "lint mathlib" step when run on branches of forks of @leanprover-community/mathlib4 ? Answer after browsing the repository thoroughly.

A: Upon reviewing the repository and its scripts, certain patterns and possible causes of CI hanging after the "lint mathlib" step when run on forks can be identified:

Probable Cause:

1. Fork and Remote Configuration:

   • Functions like gh_get_all_forks, gh_find_mathlib_fork, and gh_get_mathlib_fork in scripts/githelper.py involve verifying remotes for forks. If these functions encounter errors or inconsistencies in how the forks are set up or synchronized, it might lead to issues in downstream processes during the CI pipeline.

2. Error Handling in Fork Migration:

alreadydone

Me:

Please find the original quote of the following Chinese translation:

我们千万不能跟自己说：由于想进入这个厉害的产业，所以必须在制片人的期望和自身的期望之间做出妥协，也就是一方面假装顺应他的要求而精心构思歌舞片或黑色电影，但另一方面又在里面放入一点自己的小想法，因为光是这样想，就已未战先败。我们应当跟自己说：我要给他们草草做一件绝对真诚的东西，以至于最终竟发出了真实的光芒，并展现出一股巨大的力量；我将要向他们证明，真实是可盈利的，而且我的真实是唯一的真实。[……]务必要疯狂地怀抱雄心，且还要疯狂地真诚……

---

DeepSeek: Retrieved 39 webpages

alreadydone

I'll break down this Lean code line by line:

elab tk:"#trans_imports" stx:(str)? : command => do

• This line defines a custom Lean elaborator (command) named #trans_imports
• tk:"#trans_imports" specifies the syntax for invoking this command
• stx:(str)? means the command optionally takes a string argument
• : command => indicates this is a command-level elaborator
• do starts a do-block for sequential imperative-style operations

alreadydone

Q: In Lean 4, how do I write a tactic that adds a fixed list of lemmas to a simp call?

A: Here is one way to write a tactic in Lean 4 that adds a fixed list of lemmas to a simp call:

import tactic

-- List of lemmas we want to add
def my_simp_lemmas : list name := [`foo, `bar, `baz]

alreadydone

import Mathlib.Algebra.Algebra.Basic
import Mathlib.Algebra.Polynomial.Basic
import Mathlib.Algebra.Polynomial.Degree.Definitions
import Mathlib.Algebra.Polynomial.Degree.Operations
import Mathlib.Algebra.Polynomial.Eval.Coeff
import Mathlib.Data.ZMod.Defs
import Mathlib.Tactic.SuppressCompilation

open scoped Polynomial
open Polynomial (C X)

alreadydone

2023-11-22T02:15:59.7794991Z error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/build/lib /home/lean/.elan/toolchains/leanprover--lean4---v4.3.0-rc2/bin/lean -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false ./././Mathlib/CategoryTheory/Sites/Grothendieck.lean -R ././. -o ./.lake/build/lib/Mathlib/CategoryTheory/Sites/Grothendieck.olean -i ./.lake/build/lib/Mathlib/CategoryTheory/Sites/Grothendieck.ilean -c ./.lake/build/ir/Mathlib/CategoryTheory/Sites/Grothendieck.c
2023-11-22T02:15:59.7802783Z error: stdout:
2023-11-22T02:15:59.7805141Z ##[error]./././Mathlib/CategoryTheory/Sites/Grothendieck.lean:309:66: error: application type mismatch
2023-11-22T02:15:59.7806652Z   completeLatticeOfInf
2023-11-22T02:15:59.7806982Z     (WithTop
2023-11-22T02:15:59.8263195Z

alreadydone

import Mathlib.Topology.Covering
import Mathlib.Topology.Instances.AddCircle

open Topology

variable {E X A : Type*} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A]

/- Note: WeaklyLocallyCompact + T2 actually implies LocallyCompact. -/
@[to_additive] lemma coveringMulAction_of_properlyDiscontinuousSMul {Γ T}
    [TopologicalSpace T] [SMul Γ T] (cont : ∀ g : Γ, Continuous (fun t : T ↦ g • t))

alreadydone

/-
Copyright (c) 2023 Junyan Xu. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Junyan Xu
-/
import Mathlib.Topology.Covering
import Mathlib.Topology.Homotopy.Path
import Mathlib.Topology.UnitInterval
/-!

alreadydone

Before adding instance `covariantClass_le_of_lt`:

[Elab.command] [1.263200s] set_option profiler true in
    @[simp]
    theorem le_sub_one_iff {n : ℕ} {k : Fin (n + 1)} : k ≤ k - 1 ↔ k = 0 :=
      by
      cases n
      · simp [fin_one_eq_zero k]
      rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm, sub_eq_iff_eq_add]
      simp ▼

alreadydone

HPC cluster node with Intel(R) Xeon(R) CPU E7-8860 v4 @ 2.20GHz or AMD EPYC 7543 32-Core Processor:
both the original (float64) and the float32 versions always yield 0.0
blas_info:
    libraries = ['cblas', 'blas', 'cblas', 'blas']
    library_dirs = ['/usr/local/Anaconda/envs/py3.9/lib']
    include_dirs = ['/usr/local/Anaconda/envs/py3.9/include']
    language = c
    define_macros = [('HAVE_CBLAS', None)]
blas_opt_info:
    define_macros = [('NO_ATLAS_INFO', 1), ('HAVE_CBLAS', None)]