lean#703 noncomputable!

Stream: PR reviews

[Kyle Miller]

This is a PR to add the ability to completely turn off the noncomputability checker and the VM compiler. There are two user-visible features: the noncomputable! modifier for definitions and the noncomputable! theory command (for when you really mean it).

The current noncomputable theory is sort of misleading in that it actually just causes Lean to ignore whether you applied noncomputable correctly. It still VM compiles things it thinks are computable. To avoid this, you can do noncomputable! theory at the top of your file and never see another noncomputability checker or VM compilation error ever again.

I'm posting this message as an RFC, and there are some more details in the PR message at lean#703. I believe this is a completely reverse-compatible change.

[Mario Carneiro]

I don't think it would be a good idea to use this in mathlib, I think it will increase the number of VM error messages

[Mario Carneiro]

plus this will be another thing to support in mathport, I'm not sure lean 4 has what we need

[Kyle Miller]

Why do you think it would increase the number of VM error messages? This causes declarations to be marked noncomputable in the environment, so nothing VM compiled could ever use them.

[Mario Carneiro]

until you try to use anything from the file in the next file down

[Kyle Miller]

Regarding Lean 4, isn't noncomputable! equivalent to its noncomputable?

[Mario Carneiro]

we need to support all three settings with this version

[Kyle Miller]

Mario Carneiro said:

until you try to use anything from the file in the next file down

How so?

[Kyle Miller]

For mathport, you can replace noncomputable theory with explicit noncomputables, and all the information you need is in the noncomputability marking in the environment, I'm pretty sure.

[Mario Carneiro]

synport does syntax porting, it does not do syntactic transformations like that unless they reflect the user's intent

[Kyle Miller]

What are you porting noncomputable theory to then?

[Mario Carneiro]

noncomputable section I believe

[Kyle Miller]

That means it's all completely not compiled, right? So if that behavior remains the same in Lean 4, both noncomputable theory and noncomputable! theory can become noncomputable section

[Mario Carneiro]

no, this works

noncomputable section

def foo := 1
#eval foo

[Mario Carneiro]

only the noncomputable modifier on defs forces noncomputable

[Mario Carneiro]

I think that "don't compile anything in this section" is dangerous because tactics might want to create and compile auxiliary defs in a section

[Mario Carneiro]

noncomputable is also incompatible with partial/unsafe

[Kyle Miller]

I'm still not sure what you're referring to about VM error messages

-- mod1.lean
noncomputable! def n : ℕ := 37

-- mod2.lean
import mod1

#print n
/-
noncomputable def n : ℕ :=
37
-/

def m := n
/- definition 'm' is noncomputable, it depends on 'n' -/

[Mario Carneiro]

I have occasionally hit issues with noncomputable lemma foo := 1 definitions in old lean 3 (which is also essentially "force noncomputable")

[Mario Carneiro]

luckily this pattern is used very rarely so it hasn't been a problem but I guess this will make it more common

[Mario Carneiro]

The issue being that a thing that really should be computable has accidentally been marked noncomputable

[Mario Carneiro]

it's very annoying to fix this when the thing is an auxiliary def

[Mario Carneiro]

in fact I'm pretty sure all current issues with noncomputable theory not just working are of this form

[Kyle Miller]

What kinds of things happen when you have noncomputable lemmas?

[Mario Carneiro]

Note that it's a noncomputable lemma which has a type which is data

[Mario Carneiro]

i.e. the thing that you get linter warnings about

[Mario Carneiro]

unfortunately I can't remember the details, but it is something along the lines of the VM not finding a definition it is supposed to

[Mario Carneiro]

Can you give an example where noncomputable! is the right thing to do?

[Mario Carneiro]

as far as I see it noncomputable theory is the correct option if you never want to think about computability

[Kyle Miller]

This is for people like @Kevin Buzzard where they don't care if the VM compiler runs, and he's been reporting examples with timeout errors that as far as I can tell all come from exponential blowups in VM compiler preprocessing steps

[Mario Carneiro]

maybe there are bugs in the implementation but spec-wise it has exactly the right semantics

[Kyle Miller]

They've been using force_noncomputable as a stop-gap

[Kyle Miller]

These are also things that they're never going to evaluate, so why waste cycles VM compiling them?

[Kyle Miller]

or checking whether they could be VM compiled?

[Mario Carneiro]

Okay, that works for noncomputable! on an individual def but not a whole section

[Mario Carneiro]

I would use it only when there is a definite gain

[Mario Carneiro]

and also fix the noncomputable checker to not be slow if that's the issue

[Mario Carneiro]

You will also need a computable! modifier for when you want a computable def in a noncomputable! theory file, no?

[Kyle Miller]

Yeah, that's fair, and I'm not suggesting noncomputable! theory should be used in mathlib. The main feature here is the noncomputable! modifier, and I added the command since I was touching all this code anyway.

[Mario Carneiro]

(flashbacks to CSS !important)

[Kyle Miller]

I still don't see why we care about finding opportunities to VM compile theoretical definitions. Where would these ever be used?

Lean 4's noncomputability system seems to be much more robust, and it very likely noncomputable! and noncomputable could be translated to the same thing.

[Kyle Miller]

Mario Carneiro said:

and also fix the noncomputable checker to not be slow if that's the issue

The issue is that the definitions Kevin's shared are all computable, but the VM compiler is horrendously slow -- I poked around a bit, but it doesn't seem to be a good use of time trying to fix that.

[Mario Carneiro]

If this is being used to better express intent in the code than I have no issues with adding these things. But I would not recommend noncomputable! theory to people who don't know the tradeoffs

[Kyle Miller]

As far as I can tell, neither noncomputable! nor noncomputable! theory affects auxiliary definitions. This is either a bug or a feature, I suppose.

[Mario Carneiro]

that can be bad if an auxiliary definition refers to a user definition and everything in sight is noncomputable except the auxiliary

[Kyle Miller]

If it refers to the user definition, I think it will be marked noncomputable, too. They seem to be processed as if they were under noncomputable theory.

[Kyle Miller]

What might be a bug is that noncomputable! theory causes all lemmas to be marked noncomputable. Does that have any affect on anything?

[Mario Carneiro]

lemmas are always noncomputable

[Mario Carneiro]

like I said, noncomputable lemma is a way to get the effect of noncomputable! def in old lean 3

[Kyle Miller]

They're not marked noncomputable

[Kyle Miller]

noncomputable!
lemma foo1 : true := trivial

lemma foo2 : true := trivial

#print foo1
/-
noncomputable theorem foo1 : true :=
trivial
-/

#print foo2
/-
theorem foo2 : true :=
trivial
-/

[Mario Carneiro]

well, it might put the modifier on but it doesn't have code

[Mario Carneiro]

noncomputable lemma foo1 : nat := 1 -- incorrectly marked as noncomputable, but proceeds anyway
lemma foo2 : nat := 1
def foo3 : nat := 1

#eval foo1 -- no code
#eval foo2 -- no code
#eval foo3 -- 1

[Kyle Miller]

I'm not talking about a modifier here, but the noncomputable mark in the environment. That's what the #print command checks when deciding to write noncomputable, and it's also what things like the noncomputability checker use, or the VM compiler when deciding when to compile something

[Mario Carneiro]

This is the problem that occurs when the modifier does not match the presence of code:

lemma foo2 : nat := 1
def foo3 : nat := foo2
-- failed to generate bytecode for 'foo3'
-- code generation failed, VM does not have code for 'test.foo2'

[Mario Carneiro]

I see no good reason for these to ever differ

[Mario Carneiro]

i.e. all lemmas which produce data should be marked noncomputable

[Kyle Miller]

That seems like it's a bug in the noncomputability checker -- it should be able to tell when a declaration has no value

[Mario Carneiro]

well, currently you can't actually put noncomputable on a lemma, it just ignores it. With your version you can, so we should probably be consistent about what it means

[Kyle Miller]

For what it's worth, you can put noncomputable on a lemma, and it's not ignored:

import data.nat.lattice

noncomputable lemma foo : ℕ := Sup set.univ

This then correctly causes definitions that use it to need to be noncomputable as well:

def foo' := foo
-- definition 'foo'' is noncomputable, it depends on 'foo'

[Kyle Miller]

I guess what should happen is that get_noncomputable_reason should check whether it's a theorem with data. It already lets through definitions/theorems whose type is a Prop, so it might just need to require it if it's a theorem

[Kyle Miller]

@Mario Carneiro lean#704 addresses the "code generation failed" error when you use a theorem that produces data by having non-Prop theorems be marked as noncomputable. It's more restrictive than necessary and could also allow other computationally irrelevant types, but this was easiest and mathlib's linters don't allow them anyway.

[Kyle Miller]

Somewhere along the way I saw a commit message by Leo from many years ago, when the noncomputability checker was mostly built, saying that we should refactor things to use the VM compiler to determine noncomputability, otherwise it will be this endless task of trying to keep the checker and the compiler in sync. That's what Lean 4 does now, right?