/-

From https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Lean4.20autocomplete

Will have to keep on fiddling the topic of meta-programming, syntax and dealing with files in Lean

related:

- https://github.com/utensil/LeanBlueprintExample/blob/main/Exe/Decls.lean
- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/get.20filename.20.2B.20pos

-/

import Lean.Meta.Tactic.TryThis
open Lean.Meta.Tactic

namespace Mathlib.Tactic.imp

open Lean Elab Command FuzzyMatching System

Infer module name of source file name.

def moduleNameOfFileName (fname : FilePath) (rootDir : Option FilePath) : IO Name := do
  Lean.initSearchPath (<- Lean.findSysroot) [(<-IO.currentDir) / "lake-packages/mathlib/"]
  let fname ← IO.FS.realPath fname
  let rootDir ← match rootDir with
    | some rootDir => pure rootDir
    | none         => IO.currentDir
  let mut rootDir ← realPathNormalized rootDir
  if !rootDir.toString.endsWith System.FilePath.pathSeparator.toString then
    rootDir := ⟨rootDir.toString ++ System.FilePath.pathSeparator.toString⟩
  if !rootDir.toString.isPrefixOf fname.normalize.toString then
    throw $ IO.userError s!"input file '{fname}' must be contained in root directory ({rootDir})"
  -- NOTE: use `fname` instead of `fname.normalize` to preserve casing on all platforms
  let fnameSuffixComponents := fname.withExtension "" |>.components.drop (rootDir.components.length + 1)
  let modName    := fnameSuffixComponents.foldl Name.mkStr Name.anonymous
  pure modName

A syntax that allows strings to be printed without surrounding them by guillemets «...».

declare_syntax_cat write_me_output_stx

@[inherit_doc 
Parser.Category.write_me_output_stx: Parser.Category
Parser.Category.write_me_output_stx
Warning: Parser.Category.write_me_output_stx does not have a doc string]
syntax "import " 
ident: Parser.Parser
ident : 
write_me_output_stx: Parser.Category
write_me_output_stx

imp <string> tries to find a file matching Mathlib.<string>. It prints a list of candidates, taking the names from Mathlib.lean. If there is only one candidate, it suggests import Mathlib.<uniqueCandidate> as a Try this.

Using imp! <string> uses fuzzy-matching, rather than exact matching.

elab (name := 
commandImp!: ParserDescr
commandImp!) 
tk: Syntax
tk
Warning: unused variable `tk`
note: this linter can be disabled with `set_option linter.unusedVariables false`:"imp" 
fz: Option (TSyntax Name.anonymous)
fz:("!")? 
na: TSyntax `ident
na:(
colGt: optParam String "checkColGt" → Parser.Parser
colGt 
ident: Parser.Parser
ident) : 
command: Parser.Category
command => do
  let 
inp: String
inp := 
na: TSyntax `ident
na.
getId: Ident → Name
getId.
toString: Name → optParam Bool true → (optParam (String → Bool) fun x => false) → String
toString
  let 
dat: Array String
dat := 
(← IO.FS.lines ".lake/packages/mathlib/Mathlib.lean"): Array String
(← 
IO.FS.lines: FilePath → IO (Array String)
IO.FS.lines
(← IO.FS.lines ".lake/packages/mathlib/Mathlib.lean"): Array String
 
".lake/packages/mathlib/Mathlib.lean": String
".lake/packages/mathlib/Mathlib.lean"
(← IO.FS.lines ".lake/packages/mathlib/Mathlib.lean"): Array String
).
map: {α β : Type} → (α → β) → Array α → Array β
map (
String.drop: String → Nat → String
String.drop · 15)
  let 
cands: Array String
cands := 
dat: Array String
dat.
filter: {α : Type} → (α → Bool) → (as : Array α) → optParam Nat 0 → optParam Nat as.size → Array α
filter <| (if 
fz: Option (TSyntax Name.anonymous)
fz.
isSome: {α : Type} → Option α → Bool
isSome then 
fuzzyMatch: String → String → optParam Float 0.2 → Bool
fuzzyMatch else 
String.isPrefixOf: String → String → Bool
String.isPrefixOf) 
inp: String
inp

  
liftTermElabM: {α : Type} → TermElabM α → CommandElabM α
liftTermElabM do
    
cands: Array String
cands.
toList: {α : Type} → Array α → List α
toList.
forM: {m : Type → Type} → [inst : Monad m] → {α : Type} → List α → (α → m PUnit) → m PUnit
forM fun 
imp: String
imp => do
      let 
impS: Name
impS ← 
moduleNameOfFileName: FilePath → Option FilePath → IO Name
moduleNameOfFileName (
".lake/packages/mathlib/Mathlib/": String
".lake/packages/mathlib/Mathlib/" ++ 
imp: String
imp.
replace: String → String → String → String
replace 
".": String
"." 
"/": String
"/" ++ 
".lean": String
".lean") 
".lake/packages/mathlib/": String
".lake/packages/mathlib/"
      let 
imp: TSyntax `write_me_output_stx
imp : 
TSyntax: SyntaxNodeKinds → Type
TSyntax 
`write_me_output_stx: Name
`write_me_output_stx ← `(write_me_output_stx| import $(
mkIdent: Name → Ident
mkIdent 
impS: Name
impS))
      let 
stx: Syntax
stx ← 
getRef: {m : Type → Type} → [self : MonadRef m] → m Syntax
getRef
      
TryThis.addSuggestion: Syntax →
  TryThis.Suggestion →
    optParam (Option Syntax) none → optParam String "Try this: " → optParam (Option String) none → MetaM Unit
TryThis.addSuggestion 
stx: Syntax
stx 
imp: TSyntax `write_me_output_stx
imp


@[inherit_doc 
commandImp!: ParserDescr
commandImp!
Warning: commandImp! does not have a doc string]
macro "imp!" 
na: TSyntax `ident
na:(
colGt: optParam String "checkColGt" → Parser.Parser
colGt 
ident: Parser.Parser
ident) : 
command: Parser.Category
command => `(
command: Parser.Category
command| imp ! $
na: TSyntax `ident
na)

end Mathlib.Tactic.imp

imp! Ring
Try this: import Ideal.AssociatedPrime
Try this: import Category.TopCommRingCat
Try this: import BigOperators.Ring
Try this: import BigOperators.Ring.List
Try this: import BigOperators.Ring.Multiset
Try this: import BigOperators.Ring.Nat
Try this: import BigOperators.RingEquiv
Try this: import Category.BoolRing
Try this: import Category.ModuleCat.ChangeOfRings
Try this: import Category.ModuleCat.Presheaf.ChangeOfRings
Try this: import Category.ModuleCat.Sheaf.ChangeOfRings
Try this: import Category.Ring.Adjunctions
Try this: import Category.Ring.Basic
Try this: import Category.Ring.Colimits
Try this: import Category.Ring.Constructions
Try this: import Category.Ring.FilteredColimits
Try this: import Category.Ring.Instances
Try this: import Category.Ring.Limits
Try this: import CharP.LocalRing
Try this: import DirectSum.Ring
Try this: import MvPolynomial.CommRing
Try this: import Order.BigOperators.Ring.Finset
Try this: import Order.BigOperators.Ring.List
Try this: import Order.BigOperators.Ring.Multiset
Try this: import Order.Hom.Ring
Try this: import Order.Nonneg.Ring
Try this: import Order.Positive.Ring
Try this: import Order.Ring.Abs
Try this: import Order.Ring.Basic
Try this: import Order.Ring.Canonical
Try this: import Order.Ring.Cast
Try this: import Order.Ring.Cone
Try this: import Order.Ring.Defs
Try this: import Order.Ring.Finset
Try this: import Order.Ring.InjSurj
Try this: import Order.Ring.Int
Try this: import Order.Ring.Nat
Try this: import Order.Ring.Opposite
Try this: import Order.Ring.Pow
Try this: import Order.Ring.Prod
Try this: import Order.Ring.Rat
Try this: import Order.Ring.Star
Try this: import Order.Ring.Synonym
Try this: import Order.Ring.Unbundled.Basic
Try this: import Order.Ring.Unbundled.Nonneg
Try this: import Order.Ring.Unbundled.Rat
Try this: import Order.Ring.WithTop
Try this: import Polynomial.GroupRingAction
Try this: import Polynomial.RingDivision
Try this: import Ring.Action.Basic
Try this: import Ring.Action.Field
Try this: import Ring.Action.Group
Try this: import Ring.Action.Invariant
Try this: import Ring.Action.Subobjects
Try this: import Ring.AddAut
Try this: import Ring.Aut
Try this: import Ring.Basic
Try this: import Ring.BooleanRing
Try this: import Ring.Center
Try this: import Ring.Centralizer
Try this: import Ring.CentroidHom
Try this: import Ring.Commute
Try this: import Ring.CompTypeclasses
Try this: import Ring.Defs
Try this: import Ring.Divisibility.Basic
Try this: import Ring.Divisibility.Lemmas
Try this: import Ring.Equiv
Try this: import Ring.Ext
Try this: import Ring.Fin
Try this: import Ring.Hom.Basic
Try this: import Ring.Hom.Defs
Try this: import Ring.Idempotents
Try this: import Ring.Identities
Try this: import Ring.InjSurj
Try this: import Ring.Int
Try this: import Ring.Invertible
Try this: import Ring.MinimalAxioms
Try this: import Ring.Nat
Try this: import Ring.NegOnePow
Try this: import Ring.Opposite
Try this: import Ring.Parity
Try this: import Ring.Pi
Try this: import Ring.Pointwise.Set
Try this: import Ring.Prod
Try this: import Ring.Rat
Try this: import Ring.Regular
Try this: import Ring.Semiconj
Try this: import Ring.Semireal.Defs
Try this: import Ring.Subring.Basic
Try this: import Ring.Subring.IntPolynomial
Try this: import Ring.Subring.MulOpposite
Try this: import Ring.Subring.Order
Try this: import Ring.Subring.Pointwise
Try this: import Ring.Subring.Units
Try this: import Ring.Subsemiring.Basic
Try this: import Ring.Subsemiring.MulOpposite
Try this: import Ring.Subsemiring.Order
Try this: import Ring.Subsemiring.Pointwise
Try this: import Ring.SumsOfSquares
Try this: import Ring.ULift
Try this: import Ring.Units
Try this: import Ring.WithZero
Try this: import RingQuot
Try this: import Star.RingQuot
Try this: import Star.StarRingHom
Try this: import Morphisms.RingHomProperties
Try this: import Complex.RemovableSingularity
Try this: import Normed.Ring.IsPowMulFaithful
Try this: import Normed.Ring.Seminorm
Try this: import Normed.Ring.SeminormFromBounded
Try this: import Normed.Ring.SeminormFromConst
Try this: import Normed.Ring.Ultra
Try this: import Normed.Ring.Units
Try this: import Additive.RuzsaCovering
Try this: import Nat.Cast.Order.Ring
Try this: import Ring
Try this: import Manifold.Sheaf.LocallyRingedSpace
Try this: import RingedSpace.Basic
Try this: import RingedSpace.LocallyRingedSpace
Try this: import RingedSpace.LocallyRingedSpace.HasColimits
Try this: import RingedSpace.LocallyRingedSpace.ResidueField
Try this: import RingedSpace.OpenImmersion
Try this: import RingedSpace.PresheafedSpace
Try this: import RingedSpace.PresheafedSpace.Gluing
Try this: import RingedSpace.PresheafedSpace.HasColimits
Try this: import RingedSpace.SheafedSpace
Try this: import RingedSpace.Stalks
Try this: import GroupAction.Ring
Try this: import Dimension.DivisionRing
Try this: import RootSystem.RootPairingCat
Try this: import Small.Ring
Try this: import Algebra.Ring.Basic
Try this: import Algebra.Ring.FreeCommRing
Try this: import Padics.RingHoms
Try this: import Filter.AtTopBot.Ring
Try this: import Filter.Ring
Try this: import AdicCompletion.Algebra
Try this: import AdicCompletion.AsTensorProduct
Try this: import AdicCompletion.Basic
Try this: import AdicCompletion.Exactness
Try this: import AdicCompletion.Functoriality
Try this: import Adjoin.Basic
Try this: import Adjoin.FG
Try this: import Adjoin.Field
Try this: import Adjoin.PowerBasis
Try this: import Adjoin.Tower
Try this: import AdjoinRoot
Try this: import AlgebraTower
Try this: import Algebraic
Try this: import AlgebraicIndependent
Try this: import Artinian
Try this: import Bezout
Try this: import Bialgebra.Basic
Try this: import Bialgebra.Equiv
Try this: import Bialgebra.Hom
Try this: import Binomial
Try this: import ChainOfDivisors
Try this: import ClassGroup
Try this: import Coalgebra.Basic
Try this: import Coalgebra.Equiv
Try this: import Coalgebra.Hom
Try this: import Coalgebra.TensorProduct
Try this: import Complex
Try this: import Congruence.Basic
Try this: import Congruence.BigOperators
Try this: import Congruence.Opposite
Try this: import Coprime.Basic
Try this: import Coprime.Ideal
Try this: import Coprime.Lemmas
Try this: import DedekindDomain.AdicValuation
Try this: import DedekindDomain.Basic
Try this: import DedekindDomain.Different
Try this: import DedekindDomain.Dvr
Try this: import DedekindDomain.Factorization
Try this: import DedekindDomain.FiniteAdeleRing
Try this: import DedekindDomain.Ideal
Try this: import DedekindDomain.IntegralClosure
Try this: import DedekindDomain.PID
Try this: import DedekindDomain.SInteger
Try this: import DedekindDomain.SelmerGroup
Try this: import Derivation.Basic
Try this: import Derivation.DifferentialRing
Try this: import Derivation.Lie
Try this: import Derivation.MapCoeffs
Try this: import Derivation.ToSquareZero
Try this: import DiscreteValuationRing.Basic
Try this: import DiscreteValuationRing.TFAE
Try this: import Discriminant
Try this: import DualNumber
Try this: import EisensteinCriterion
Try this: import EssentialFiniteness
Try this: import Etale.Basic
Try this: import EuclideanDomain
Try this: import Filtration
Try this: import FiniteLength
Try this: import FinitePresentation
Try this: import FiniteStability
Try this: import FiniteType
Try this: import Finiteness
Try this: import Fintype
Try this: import Flat.Algebra
Try this: import Flat.Basic
Try this: import Flat.CategoryTheory
Try this: import Flat.EquationalCriterion
Try this: import Flat.FaithfullyFlat
Try this: import Flat.Stability
Try this: import FractionalIdeal.Basic
Try this: import FractionalIdeal.Extended
Try this: import FractionalIdeal.Norm
Try this: import FractionalIdeal.Operations
Try this: import FreeCommRing
Try this: import FreeRing
Try this: import Generators
Try this: import GradedAlgebra.Basic
Try this: import GradedAlgebra.HomogeneousIdeal
Try this: import GradedAlgebra.HomogeneousLocalization
Try this: import GradedAlgebra.Noetherian
Try this: import GradedAlgebra.Radical
Try this: import HahnSeries.Addition
Try this: import HahnSeries.Basic
Try this: import HahnSeries.Multiplication
Try this: import HahnSeries.PowerSeries
Try this: import HahnSeries.Summable
Try this: import HahnSeries.Valuation
Try this: import Henselian
Try this: import HopfAlgebra
Try this: import Polynomial.Eisenstein.IsIntegral
Try this: import Ideal.Basic
Try this: import Ideal.Basis
Try this: import Ideal.Colon
Try this: import Ideal.Cotangent
Try this: import Ideal.IdempotentFG
Try this: import Ideal.IsPrimary
Try this: import Ideal.IsPrincipal
Try this: import Ideal.Maps
Try this: import Ideal.MinimalPrime
Try this: import Ideal.Norm
Try this: import Ideal.Operations
Try this: import Ideal.Over
Try this: import Ideal.Pointwise
Try this: import Ideal.Prod
Try this: import Ideal.Quotient
Try this: import Ideal.QuotientOperations
Try this: import Idempotents
Try this: import Int.Basic
Try this: import IntegralClosure.Algebra.Basic
Try this: import IntegralClosure.Algebra.Defs
Try this: import IntegralClosure.IntegralRestrict
Try this: import IntegralClosure.IntegrallyClosed
Try this: import IntegralClosure.IsIntegral.Basic
Try this: import IntegralClosure.IsIntegral.Defs
Try this: import IntegralClosure.IsIntegralClosure.Basic
Try this: import IntegralClosure.IsIntegralClosure.Defs
Try this: import IntegralDomain
Try this: import IsAdjoinRoot
Try this: import IsTensorProduct
Try this: import Jacobson
Try this: import JacobsonIdeal
Try this: import Kaehler.Basic
Try this: import Kaehler.CotangentComplex
Try this: import Kaehler.Polynomial
Try this: import KrullDimension.Basic
Try this: import KrullDimension.Field
Try this: import LaurentSeries
Try this: import LittleWedderburn
Try this: import LocalProperties.Basic
Try this: import LocalProperties.IntegrallyClosed
Try this: import LocalProperties.Reduced
Try this: import LocalRing.Basic
Try this: import LocalRing.Defs
Try this: import LocalRing.MaximalIdeal.Basic
Try this: import LocalRing.MaximalIdeal.Defs
Try this: import LocalRing.Module
Try this: import LocalRing.Quotient
Try this: import LocalRing.ResidueField.Basic
Try this: import LocalRing.ResidueField.Defs
Try this: import LocalRing.RingHom.Basic
Try this: import Localization.Algebra
Try this: import Localization.AsSubring
Try this: import Localization.AtPrime
Try this: import Localization.Away.AdjoinRoot
Try this: import Localization.Away.Basic
Try this: import Localization.Away.Lemmas
Try this: import Localization.BaseChange
Try this: import Localization.Basic
Try this: import Localization.Cardinality
Try this: import Localization.Defs
Try this: import Localization.Finiteness
Try this: import Localization.FractionRing
Try this: import Localization.Ideal
Try this: import Localization.Integer
Try this: import Localization.Integral
Try this: import Localization.InvSubmonoid
Try this: import Localization.LocalizationLocalization
Try this: import Localization.Module
Try this: import Localization.NormTrace
Try this: import Localization.NumDen
Try this: import Localization.Submodule
Try this: import MatrixAlgebra
Try this: import MaximalSpectrum
Try this: import Multiplicity
Try this: import MvPolynomial.Basic
Try this: import MvPolynomial.Homogeneous
Try this: import MvPolynomial.Ideal
Try this: import MvPolynomial.Localization
Try this: import MvPolynomial.Symmetric.Defs
Try this: import MvPolynomial.Symmetric.FundamentalTheorem
Try this: import MvPolynomial.Symmetric.NewtonIdentities
Try this: import MvPolynomial.Tower
Try this: import MvPolynomial.WeightedHomogeneous
Try this: import MvPowerSeries.Basic
Try this: import MvPowerSeries.Inverse
Try this: import MvPowerSeries.LexOrder
Try this: import MvPowerSeries.NoZeroDivisors
Try this: import MvPowerSeries.Trunc
Try this: import Nakayama
Try this: import Nilpotent.Basic
Try this: import Nilpotent.Defs
Try this: import Nilpotent.Lemmas
Try this: import Noetherian
Try this: import NonUnitalSubring.Basic
Try this: import NonUnitalSubsemiring.Basic
Try this: import Norm.Basic
Try this: import Norm.Defs
Try this: import NormTrace
Try this: import Nullstellensatz
Try this: import OreLocalization.Basic
Try this: import OreLocalization.OreSet
Try this: import OreLocalization.Ring
Try this: import OrzechProperty
Try this: import Perfection
Try this: import PiTensorProduct
Try this: import Polynomial.Basic
Try this: import Polynomial.Bernstein
Try this: import Polynomial.Chebyshev
Try this: import Polynomial.Content
Try this: import Polynomial.Cyclotomic.Basic
Try this: import Polynomial.Cyclotomic.Eval
Try this: import Polynomial.Cyclotomic.Expand
Try this: import Polynomial.Cyclotomic.Roots
Try this: import Polynomial.Dickson
Try this: import Polynomial.Eisenstein.Basic
Try this: import TensorProduct.Basic
Try this: import Polynomial.GaussLemma
Try this: import Polynomial.Hermite.Basic
Try this: import Polynomial.Hermite.Gaussian
Try this: import Polynomial.IntegralNormalization
Try this: import Polynomial.IrreducibleRing
Try this: import Polynomial.Nilpotent
Try this: import Polynomial.Opposites
Try this: import Polynomial.Pochhammer
Try this: import Polynomial.Quotient
Try this: import Polynomial.RationalRoot
Try this: import Polynomial.ScaleRoots
Try this: import Polynomial.Selmer
Try this: import Polynomial.SeparableDegree
Try this: import Polynomial.Tower
Try this: import Polynomial.Vieta
Try this: import Polynomial.Wronskian
Try this: import PolynomialAlgebra
Try this: import PowerBasis
Try this: import PowerSeries.Basic
Try this: import PowerSeries.Derivative
Try this: import PowerSeries.Inverse
Try this: import PowerSeries.Order
Try this: import PowerSeries.Trunc
Try this: import PowerSeries.WellKnown
Try this: import Presentation
Try this: import Prime
Try this: import PrimeSpectrum
Try this: import PrincipalIdealDomain
Try this: import QuotSMulTop
Try this: import QuotientNilpotent
Try this: import QuotientNoetherian
Try this: import Radical
Try this: import ReesAlgebra
Try this: import Regular.IsSMulRegular
Try this: import Regular.RegularSequence
Try this: import RingHom.Finite
Try this: import RingHom.FinitePresentation
Try this: import RingHom.FiniteType
Try this: import RingHom.Integral
Try this: import RingHom.Locally
Try this: import RingHom.StandardSmooth
Try this: import RingHom.Surjective
Try this: import RingHomProperties
Try this: import RingInvo
Try this: import RootsOfUnity.Basic
Try this: import RootsOfUnity.Complex
Try this: import RootsOfUnity.Lemmas
Try this: import RootsOfUnity.Minpoly
Try this: import SimpleModule
Try this: import SimpleRing.Basic
Try this: import SimpleRing.Defs
Try this: import Smooth.Basic
Try this: import Smooth.Kaehler
Try this: import Smooth.Pi
Try this: import Smooth.StandardSmooth
Try this: import Support
Try this: import SurjectiveOnStalks
Try this: import WittVector.Basic
Try this: import TensorProduct.MvPolynomial
Try this: import Trace.Basic
Try this: import Trace.Defs
Try this: import Trace.Quotient
Try this: import TwoSidedIdeal.Basic
Try this: import TwoSidedIdeal.BigOperators
Try this: import TwoSidedIdeal.Instances
Try this: import TwoSidedIdeal.Lattice
Try this: import TwoSidedIdeal.Operations
Try this: import UniqueFactorizationDomain
Try this: import Unramified.Basic
Try this: import Unramified.Derivations
Try this: import Unramified.Field
Try this: import Unramified.Finite
Try this: import Unramified.Pi
Try this: import Valuation.AlgebraInstances
Try this: import Valuation.Basic
Try this: import Valuation.ExtendToLocalization
Try this: import Valuation.Integers
Try this: import Valuation.Integral
Try this: import Valuation.Minpoly
Try this: import Valuation.PrimeMultiplicity
Try this: import Valuation.Quotient
Try this: import Valuation.RamificationGroup
Try this: import Valuation.RankOne
Try this: import Valuation.ValExtension
Try this: import Valuation.ValuationRing
Try this: import Valuation.ValuationSubring
Try this: import WittVector.Teichmuller
Try this: import WittVector.Compare
Try this: import WittVector.Defs
Try this: import WittVector.DiscreteValuationRing
Try this: import WittVector.Domain
Try this: import WittVector.Frobenius
Try this: import WittVector.FrobeniusFractionField
Try this: import WittVector.Identities
Try this: import WittVector.InitTail
Try this: import WittVector.IsPoly
Try this: import WittVector.Isocrystal
Try this: import WittVector.MulCoeff
Try this: import WittVector.MulP
Try this: import WittVector.StructurePolynomial
Try this: import Ring.Basic
Try this: import WittVector.Truncated
Try this: import WittVector.Verschiebung
Try this: import WittVector.WittPolynomial
Try this: import ZMod
Try this: import NoncommRing
Try this: import Ring
Try this: import Algebra.InfiniteSum.Ring
Try this: import Ring.Compare
Try this: import Ring.PNat
Try this: import Ring.RingNF
Try this: import Algebra.Ring.Ideal
Try this: import Algebra.Ring.Basic
Try this: import Algebra.UniformRing