[Merged by Bors] - refactor(Mathport): move mathport prelude to mathlib4

.github/workflows/build.yml

@@ -25,7 +25,7 @@ jobs:
 
       - name: update Mathlib.lean
         run: |
-          find Mathlib -not -type d | sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
+          find Mathlib -name "*.lean" | sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
       - name: build mathlib
         run: lake build

Mathlib.lean

@@ -30,6 +30,10 @@ import Mathlib.Init.SetNotation
 import Mathlib.Lean.LocalContext
 import Mathlib.Logic.Basic
 import Mathlib.Logic.Function.Basic
+import Mathlib.Mathport.Attributes
+import Mathlib.Mathport.Rename
+import Mathlib.Mathport.SpecialNames
+import Mathlib.Mathport.Syntax
 import Mathlib.Tactic.Basic
 import Mathlib.Tactic.Cache
 import Mathlib.Tactic.Coe

Mathlib/Mathport/Attributes.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Lean.Attributes
+
+namespace Lean.Attr
+
+initialize reflAttr : TagAttribute ← registerTagAttribute `refl "reflexive relation"
+initialize symmAttr : TagAttribute ← registerTagAttribute `symm "symmetric relation"
+initialize transAttr : TagAttribute ← registerTagAttribute `trans "transitive relation"
+initialize substAttr : TagAttribute ← registerTagAttribute `subst "substitution"
+
+initialize linterAttr : TagAttribute ←
+  registerTagAttribute `linter "Use this declaration as a linting test in #lint"
+
+initialize hintTacticAttr : TagAttribute ←
+  registerTagAttribute `hintTactic "A tactic that should be tried by `hint`."

Mathlib/Mathport/README.md

@@ -0,0 +1,22 @@
+Mathport prelude
+===
+
+This directory contains instructions for `mathport`,
+helping it to translate `mathlib` and align declarations and tactics with `mathlib4`.
+(These files were formerly part of `mathport`, in the directory `Mathport/Prelude/`.)
+
+`SpecialNames.lean`
+: Contains `#align X Y` statements, where `X` is an identifier from mathlib3
+  which should be aligned with the identifier `Y` from mathlib4.
+  Sometimes we need `#align` statements just to handle exceptions to casing rules,
+  but there are also many exceptional cases.
+
+`Syntax.lean`
+: Contains unimplemented stubs of tactics which need to be migrated from Lean3 to Lean4.
+  When porting tactics, you can move the relevant stubs to a new file and
+  use them as a starting point.
+  Please make sure this file stays in sync with new tactic implementations
+  (and in particular that the syntax is not defined twice).
+  Please preserve the syntax of existing mathlib tactics,
+  so that there are no unnecessary parse errors in the source files generated by `synport`.
+  It is fine to fail with an error message for unimplemented features for now.

Mathlib/Mathport/Rename.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Daniel Selsam
+-/
+import Lean
+
+namespace Mathlib.Prelude.Rename
+
+open Lean
+open System (FilePath)
+open Std (HashMap)
+
+abbrev RenameMap := HashMap Name Name
+
+def RenameMap.insertPair (m : RenameMap) : Name × Name → RenameMap
+  | (n3, n4) => m.insert n3 n4
+
+initialize renameExtension : SimplePersistentEnvExtension (Name × Name) RenameMap ←
+  registerSimplePersistentEnvExtension {
+    name          := `renameMapExtension
+    addEntryFn    := RenameMap.insertPair
+    addImportedFn := fun es => mkStateFromImportedEntries (RenameMap.insertPair) {} es
+  }
+
+def getRenameMap (env : Environment) : RenameMap := do
+  renameExtension.getState env
+
+def addNameAlignment (n3 n4 : Name) : CoreM Unit := do
+  modifyEnv fun env => renameExtension.addEntry env (n3, n4)
+
+open Lean.Elab Lean.Elab.Command
+
+syntax (name := align) "#align " ident ident : command
+
+@[commandElab align] def elabAlign : CommandElab
+  | `(#align%$tk $id3:ident $id4:ident) =>
+    liftCoreM $ addNameAlignment id3.getId id4.getId
+  | _ => throwUnsupportedSyntax
+
+syntax (name := lookup3) "#lookup3 " ident : command
+
+@[commandElab lookup3] def elabLookup3 : CommandElab
+  | `(#lookup3%$tk $id3:ident) => do
+    let n3 := id3.getId
+    match getRenameMap (← getEnv) |>.find? n3 with
+    | none    => logInfoAt tk s!"name `{n3} not found"
+    | some n4 => logInfoAt tk s!"{n4}"
+  | _ => throwUnsupportedSyntax
+
+end Mathlib.Prelude.Rename

Mathlib/Mathport/SpecialNames.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Daniel Selsam
+-/
+import Mathlib.Mathport.Rename
+
+namespace Mathlib.Prelude
+
+-- Note: we do not currently auto-align constants.
+#align quot Quot
+#align quot.mk Quot.mk
+#align quot.lift Quot.lift
+#align quot.ind Quot.ind
+
+-- Otherwise would be`OutParam` and `OptParam`!
+-- Note: we want `auto_param` to *not* align.
+#align out_param               outParam
+#align opt_param               optParam
+
+#align heq                     HEq
+
+#align punit                   PUnit
+#align pprod                   PProd
+
+#align has_coe Coe
+#align has_coe.coe Coe.coe
+
+#align has_coe_t CoeT
+#align has_coe_t.coe CoeT.coe
+
+#align has_coe_to_fun CoeFun
+#align has_coe_to_fun.coe CoeFun.coe
+
+#align has_coe_to_sort CoeSort
+#align has_coe_to_sort.coe CoeSort.coe
+
+#align has_le                  LE
+#align has_le.le               LE.le
+#align has_lt                  LT
+#align has_lt.lt               LT.lt
+
+#align has_beq                 BEq
+#align has_sizeof              SizeOf
+
+-- This otherwise causes filenames to clash
+#align category_theory.Kleisli CategoryTheory.KleisliCat
+
+-- TODO: backport?
+#align int.neg_succ_of_nat     Int.negSucc
+
+-- Generic 'has'-stripping
+-- Note: we don't currently strip automatically for various reasons.
+#align has_add       Add
+#align has_sub       Sub
+#align has_mul       Mul
+#align has_div       Div
+#align has_neg       Neg
+#align has_mod       Mod
+#align has_pow       Pow
+#align has_append    Append
+#align has_pure      Pure
+#align has_bind      Bind
+#align has_seq       Seq
+#align has_seq_left  SeqLeft
+#align has_seq_right SeqRight
+
+-- Implementation detail
+#align _sorry_placeholder_     _sorry_placeholder_
+
+
+
+end Mathlib.Prelude