comment out MagmaLawExt.addEntry call that majorly slows down the bui…

…ld (#465) #427 has caused builds to become much slower. If I comment out two lines that it added, as in this PR, build times become reasonable again. This is a stopgap until we understand the source of the slowness.
teorth · Oct 9, 2024 · c27789e · c27789e
1 parent 94aeec5
commit c27789e
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/equational_theories/EquationsCommand.lean b/equational_theories/EquationsCommand.lean
@@ -90,8 +90,10 @@ elab mods:declModifiers tk:"equation " i:num " := " tsyn:term : command => do
   elabCommand (← `(command| abbrev%$tk $thmName : ∀ (G : Type _) [$inst : Magma G], G ⊧ $lawIdent ↔ $eqIdent G :=
                     fun G _ ↦ Iff.trans (Law.satisfies_fin_satisfies_nat G $finLawIdent).symm ($finThmName G)))
   -- register the law
-  modifyEnv (magmaLawExt.addEntry · (lawName, ← (mkNatMagmaLaw lawName).run
-    { env := (← getEnv), opts := (← getOptions) }))
+  -- (The following two lines have been commented out because they cause the build to become very slow.
+  -- See https://github.com/teorth/equational_theories/issues/464.)
+  --modifyEnv (magmaLawExt.addEntry · (lawName, ← (mkNatMagmaLaw lawName).run
+  --  { env := (← getEnv), opts := (← getOptions) }))
   Command.liftTermElabM do
     -- TODO: This will go wrong if we are in a namespace. Is this really needed, or is there
     -- a way to pass the current position already to the `(command|` above?