suppress_compilation

Stream: mathlib4

[Sebastien Gouezel]

For the record, I have just tried the brand new suppress_compilation tactic in the tensor product file on master, and it breaks notation: if you open the file Mathlib.LinearAlgebra.TensorProduct, and add

import Mathlib.Tactic.SuppressCompilation
supress_compilation

then a few lines below

set_option quotPrecheck false in
scoped[TensorProduct] infixl:100 " ⊗ " => TensorProduct _

gives an error

unknown declaration 'TensorProduct.term_⊗_'
invalid syntax node kind 'TensorProduct.«term_⊗_»'

So it will be hard to use suppress_compilation on a larger scale in mathlib, unless some wizard (@Mac Malone ?) understands what is going on here.

[Sebastien Gouezel]

The problem is certainly that the notation expands to a def (see docs#TensorProduct.«term_⊗_») , but we don't want suppress_compilation to act on this def.

[Matthew Ballard]

I made lean4#2619 as another approach

[Mac Malone]

Matthew Ballard said:

I made lean4#2619 as another approach

I am confused. Wouldn't that approach break in the same way for situations like this?

[Matthew Ballard]

You are correct.

[Matthew Ballard]

Didn't read carefully and thought it was problem parsing the syntax

[Matthew Ballard]

But you can set_option compiler.suppress false in to work around.

[Matthew Ballard]

Not great still though

[Mac Malone]

@Sebastien Gouezel There are two ways I can think of to solve this at the moment:

• Sprinkle an unsupress_compilation in through the file on definitions like these that should still be compiled.
• Reorganized the file so that suppress_compilation can be used in the pure math sections but not in the places where computational components (like notation) are defined.

[Sebastien Gouezel]

Couldn't notation trigger the unsupress_compilation all by itself? (for instance set some flag that would desactivate the suppress_compilation behavior?)

[Matthew Ballard]

We could try it with notation3 but I don't think that will cover all of the cases. Can you parse the declName for «?

[Matthew Ballard]

Would something as silly as

| `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)?
    $(recKind?)? def $id $sig:optDeclSig $val:declVal $(term?)? $(decr?)?) => do
  if (toString id).containsSubstr "«".toSubstring then
    elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? $(⟨mkNullNode⟩) $(unsafe?)?
      $(recKind?)? def $id $sig:optDeclSig $val:declVal $(term?)? $(decr?)?)
  else elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)?
    $(recKind?)? def $id $sig:optDeclSig $val:declVal $(term?)? $(decr?)?)

work?

[Patrick Massot]

I remember a time where "silly" meant something else here... :older_man:

[Mac Malone]

Sebastien Gouezel said:

Couldn't notation trigger the unsupress_compilation all by itself? (for instance set some flag that would desactivate the suppress_compilation behavior?)

Yes, if more special casing is desirable. Here is extended version of my previous example which now excludes notation:

namespace ex2

def elabSuppressCompilationDecl : CommandElab := fun
| `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)? $(recKind?)?
    def $id $sig:optDeclSig $val:declVal $(term?)? $(decr?)?) => do
  elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)? $(recKind?)?
    def $id $sig:optDeclSig $val:declVal $(term?)? $(decr?)?)
| `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)? $(recKind?)?
    def $id $sig:optDeclSig $val:declVal deriving $derivs,* $(term?)? $(decr?)?) => do
  elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)? $(recKind?)?
    def $id $sig:optDeclSig $val:declVal deriving $derivs,* $(term?)? $(decr?)?)
| `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)? $(recKind?)?
    $(attrKind?)? instance $(prio?)? $(id?)? $sig:declSig $val:declVal $(term?)?) => do
  elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)? $(recKind?)?
    $(attrKind?)? instance $(prio?)? $(id?)? $sig:declSig $val:declVal $(term?)?)
| _ => throwUnsupportedSyntax

scoped syntax "unsuppress_compilation" (" in " command)? : command

def expandSuppressCompilationNotation : Macro := fun
| `($[$doc?:docComment]? $(attrs?)? $(attrKind)? notation $(prec?)? $(name?)? $(prio?)? $items* => $v) => do
  let defn ← expandNotation <| ← `($[$doc?:docComment]? $(attrs?)? $(attrKind)? notation $(prec?)? $(name?)? $(prio?)? $items* => $v)
  `(unsuppress_compilation in $(⟨defn⟩):command)
| _ => Macro.throwUnsupported

macro_rules
| `(unsuppress_compilation $[in $cmd?]?)  => do
  let declElab := mkCIdent ``elabSuppressCompilationDecl
  let notaMacro := mkCIdent ``expandSuppressCompilationNotation
  let attrCmds ← `(
    attribute [-command_elab] $declElab
    attribute [-macro] $notaMacro
  )
  if let some cmd := cmd? then
    `(section $attrCmds:command $cmd:command end)
  else
    return attrCmds

scoped macro "suppress_compilation" : command => do
  let declKind := mkIdent ``declaration
  let notaKind := mkIdent ``«notation»
  let declElab := mkCIdent ``elabSuppressCompilationDecl
  let notaMacro := mkCIdent ``expandSuppressCompilationNotation
  `(
  attribute [local command_elab $declKind] $declElab
  attribute [local macro $notaKind] $notaMacro
  )

suppress_compilation

def foo := "/"
/-- hi -/ def bar := foo -- works
@[simp] def baz := foo --- works

def root : System.FilePath where -- works
  toString := foo

instance : Inhabited String := ⟨foo⟩ --- works

notation "†" => Name.anonymous -- works

end ex2

def test := ex2.foo -- properly noncomputable (should error)

[Sebastien Gouezel]

Your code works great 99% of the time. I have extended it to also deal with example and abbrev, copying your pattern. There are still a few cases where it doesn't, though. One is with notation3, but this is not really surprising. Another one is with local notations: in the ex2 namespace of your post just above,

local notation "boubou" => Name.anonymous
#check boubou -- fails

doesn't work. I don't understand why, because you are forwarding attrKind.

[Sebastien Gouezel]

(Current state of things is in #7504)

[Mac Malone]

@Sebastien Gouezel local does not work because unsuppress_compilation uses a section. Here is approach without that:

namespace ex2

def elabSuppressCompilationDecl : CommandElab := fun
| `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)? $(recKind?)?
    def $id $sig:optDeclSig $val:declVal $(term?)? $(decr?)?) => do
  elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)? $(recKind?)?
    def $id $sig:optDeclSig $val:declVal $(term?)? $(decr?)?)
| `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)? $(recKind?)?
    def $id $sig:optDeclSig $val:declVal deriving $derivs,* $(term?)? $(decr?)?) => do
  elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)? $(recKind?)?
    def $id $sig:optDeclSig $val:declVal deriving $derivs,* $(term?)? $(decr?)?)
| `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)? $(recKind?)?
    $(attrKind?)? instance $(prio?)? $(id?)? $sig:declSig $val:declVal $(term?)?) => do
  elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)? $(recKind?)?
    $(attrKind?)? instance $(prio?)? $(id?)? $sig:declSig $val:declVal $(term?)?)
| _ => throwUnsupportedSyntax

scoped syntax "unsuppress_compilation" (" in " command)? : command

def expandSuppressCompilationNotation : Macro := fun
| `($[$doc?:docComment]? $(attrs?)? $(attrKind?)? notation $(prec?)? $(name?)? $(prio?)? $items* => $v) => do
  let defn ← expandNotation <| ← `($[$doc?:docComment]? $(attrs?)? $(attrKind?)? notation $(prec?)? $(name?)? $(prio?)? $items* => $v)
  `(unsuppress_compilation in $(⟨defn⟩):command)
| _ => Macro.throwUnsupported

scoped macro "suppress_compilation" : command => do
  let declKind := mkIdent ``declaration
  let notaKind := mkIdent ``«notation»
  let declElab := mkCIdent ``elabSuppressCompilationDecl
  let notaMacro := mkCIdent ``expandSuppressCompilationNotation
  `(
  attribute [local command_elab $declKind] $declElab
  attribute [local macro $notaKind] $notaMacro
  )

macro_rules
| `(unsuppress_compilation $[in $cmd?]?)  => do
  let declElab := mkCIdent ``elabSuppressCompilationDecl
  let notaMacro := mkCIdent ``expandSuppressCompilationNotation
  let attrCmds ← `(
    attribute [-command_elab] $declElab
    attribute [-macro] $notaMacro
  )
  if let some cmd := cmd? then
    `($attrCmds:command $cmd:command suppress_compilation)
  else
    return attrCmds

suppress_compilation

def foo := "/"
/-- hi -/ def bar := foo -- works
@[simp] def baz := foo --- works

def root : System.FilePath where -- works
  toString := foo

instance : Inhabited String := ⟨foo⟩ --- works

notation "†" => Name.anonymous -- works
local notation "†'" => Name.anonymous -- works

end ex2

def test := ex2.foo -- properly noncomputable (should error)

[Sebastien Gouezel]

Of course, thanks!

[Sebastien Gouezel]

For the record, I have benched the current version of the PR in which I suppress compilation in the tensor product file and downstream files. There are several files where the change is by -80% or better. This means that a very large proportion of the time spent on these files is currently for a useless step doing compilation to executable(?) code...

[Sebastien Gouezel]

https://github.com/leanprover-community/mathlib4/pull/7504#issuecomment-1747091342

[Sebastien Gouezel]

(All this can already be seen in #7281, of course).

[Kevin Buzzard]

Just to say that I agree with you that this fix is better than #7281, which was why I didn't even fix the merge conflict yet (well, that and the 320 undergraduates who I'm teaching for the next month...)