Zulip Chat Archive

Stream: FLT-regular

Topic: instances

Eric Rodriguez (Jul 14 2022 at 16:58):

we're having big issues with the issues in file#number_theory/cyclotomic/basic:

/- The `fails_quickly` linter reports: -/
/- TYPE CLASS SEARCHES TIMED OUT.
The following instances are part of a loop, or an excessively long search.
It is common that the loop occurs in a different class than the one flagged below,
but usually an instance that is part of the loop is also flagged.
To debug:
(1) run `scripts/mk_all.sh` and create a file with `import all` and
`set_option trace.class_instances true`
(2) Recreate the state shown in the error message. You can do this easily by copying the type of
the instance (the output of `#check @my_instance`), turning this into an example and removing the
last argument in square brackets. Prove the example using `by apply_instance`.
For example, if `additive.topological_add_group` raises an error, run

example {G : Type*} [topological_space G] [group G] : topological_add_group (additive G) :=
by apply_instance

(3) What error do you get?
(3a) If the error is "tactic.mk_instance failed to generate instance",
there might be nothing wrong. But it might take unreasonably long for the type-class inference to
fail. Check the trace to see if type-class inference takes any unnecessary long unexpected turns.
If not, feel free to increase the value in the definition of the linter `fails_quickly`.
(3b) If the error is "maximum class-instance resolution depth has been reached" there is almost
certainly a loop in the type-class inference. Find which instance causes the type-class inference to
go astray, and fix that instance. -/
#check @is_cyclotomic_extension.number_field /- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
State:
S : set ℕ+,
K : Type w,
L : Type z,
_inst_4 : field K,
_inst_5 : field L,
_inst_6 : algebra K L,
h : number_field K,
_inst_7 : fintype ↥S
⊢ number_field L -/
#check @cyclotomic_field.char_zero /- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
State:
n : ℕ+,
K : Type w,
_inst_4 : field K
⊢ char_zero (cyclotomic_field n K) -/
#check @cyclotomic_field.is_cyclotomic_extension /- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
State:
n : ℕ+,
K : Type w,
_inst_4 : field K
⊢ is_cyclotomic_extension {n} K (cyclotomic_field n K) -/
#check @is_alg_closed_of_char_zero.is_cyclotomic_extension /- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
State:
K : Type w,
_inst_4 : field K,
_inst_7 : is_alg_closed K,
S : set ℕ+
⊢ is_cyclotomic_extension S K K -/

/- The `dangerous_instance` linter reports: -/
/- DANGEROUS INSTANCES FOUND.
These instances are recursive, and create a new type-class problem which will have metavariables.
Possible solution: remove the instance attribute or make it a local instance instead.

Currently this linter does not check whether the metavariables only occur in arguments marked with `out_param`, in which case this linter gives a false positive. -/
#check @is_cyclotomic_extension.number_field /- The following arguments become metavariables. argument 1: (S : set ℕ+), argument 2: (K : Type w) -/
#check @is_cyclotomic_extension.finite_dimensional /- The following arguments become metavariables. argument 1: (S : set ℕ+) -/
#check @is_cyclotomic_extension.is_galois /- The following arguments become metavariables. argument 1: (n : ℕ+) -/

/- The `instance_priority` linter reports: -/
/- DANGEROUS INSTANCE PRIORITIES.
The following instances always apply, and therefore should have a priority < 1000.
If you don't know what priority to choose, use priority 100.
See note [lower instance priority] for instructions to change the priority. -/
#check @is_cyclotomic_extension.number_field /- set priority below 1000 -/
#check @is_cyclotomic_extension.finite_dimensional /- set priority below 1000 -/
#check @is_cyclotomic_extension.is_galois /- set priority below 1000 -/

I have tried to patch this by setting all of these mentioned things to priority 100, but it doesn't even seem to be enough to define the class group (in the branch failing_instances, see regular_primes.lean

Eric Rodriguez (Jul 14 2022 at 16:59):

the lint output is run at the bottom of the file; the reason we didn't see this before is because this only happens when the localised instances are opened, which is not done for mathlib's standard lint_all step.

Chris Birkbeck (Jul 14 2022 at 17:04):

I don't really understand these issues, but I'm also having trouble with our cycl_rat.lean file. If I open it it starts to use up all of my RAM

Chris Birkbeck (Jul 14 2022 at 17:04):

I don't know if its at all related

Eric Rodriguez (Jul 14 2022 at 17:08):

did you build the project before opening that file? i think it's farily deep in the imports

Chris Birkbeck (Jul 14 2022 at 17:08):

I thought I did. Let me try again.

Chris Birkbeck (Jul 14 2022 at 17:11):

So yeah even building before doesn't help. Its weird because the orange bars disappear but the RAM usage just keeps going up and up

Eric Rodriguez (Jul 14 2022 at 17:12):

yikes, I can't repro that but can't be good either:/

Chris Birkbeck (Jul 14 2022 at 17:18):

Oh ok fixed. I dunno what it was, but I hadn't noticed my local version was behind, so after pulling and building its now working fine

Riccardo Brasca (Jul 14 2022 at 17:29):

So do we have a problem or not?

Chris Birkbeck (Jul 14 2022 at 17:30):

I think my problem was unrelated to what Eric was talking about. But I don't understand his problem

Riccardo Brasca (Jul 14 2022 at 17:31):

@Eric Rodriguez where did you get the error? CI seems happy

Eric Rodriguez (Jul 14 2022 at 17:32):

just stick #lint at the end of the file

Eric Rodriguez (Jul 14 2022 at 17:33):

CI won't mind because these are all localised instances, and these locales don't get opened to lint

Riccardo Brasca (Jul 14 2022 at 17:37):

With the current master I get

/- Checking 50 declarations (plus 32 automatically generated ones) in the current file with 26 linters -/

/- The `fintype_finite` linter reports: -/
/- USES OF `fintype` SHOULD BE REPLACED WITH `casesI nonempty_fintype _` IN THE PROOF. -/
#check @is_cyclotomic_extension.finite /- The following `fintype` hypotheses should be replaced with
                      `casesI nonempty_fintype _` in the proof. argument 8: [h₁ : fintype ↥S] -/
#check @is_cyclotomic_extension.number_field /- The following `fintype` hypotheses should be replaced with
                      `casesI nonempty_fintype _` in the proof. argument 8: [_inst_7 : fintype ↥S] -/
#check @is_cyclotomic_extension.integral /- The following `fintype` hypotheses should be replaced with
                      `casesI nonempty_fintype _` in the proof. argument 9: [_inst_9 : fintype ↥S] -/
#check @is_cyclotomic_extension.finite_dimensional /- The following `fintype` hypotheses should be replaced with
                      `casesI nonempty_fintype _` in the proof. argument 5: [_inst_7 : fintype ↥S] -/

Eric Rodriguez (Jul 14 2022 at 17:38):

try maybe putting open_locale cyclotomic before it?

Riccardo Brasca (Jul 14 2022 at 17:39):

Let me try (BTW I wasn't aware of this fintype linter, does someone want to open a PR fixing the errors?)

Eric Rodriguez (Jul 14 2022 at 17:40):

(yes it's new, I'm not sure exactly how to change it, but we can definitely try to fix it)

Riccardo Brasca (Jul 14 2022 at 17:40):

OK, I get your error

Riccardo Brasca (Jul 14 2022 at 17:43):

I don't have time now to investigate this, I can do it tomorrow, but maybe there is just some loop I don't see

Eric Rodriguez (Jul 14 2022 at 17:43):

I see where some of them loop from, but I don't get some of the other loops

Riccardo Brasca (Jul 15 2022 at 13:26):

What is the loop you found?

Riccardo Brasca (Jul 15 2022 at 14:09):

Ah I see, there is at least one related to number_field and char_zero.

Eric Rodriguez (Jul 14 2022 at 16:58):

we're having big issues with the issues in file#number_theory/cyclotomic/basic:

/- The `fails_quickly` linter reports: -/
/- TYPE CLASS SEARCHES TIMED OUT.
The following instances are part of a loop, or an excessively long search.
It is common that the loop occurs in a different class than the one flagged below,
but usually an instance that is part of the loop is also flagged.
To debug:
(1) run `scripts/mk_all.sh` and create a file with `import all` and
`set_option trace.class_instances true`
(2) Recreate the state shown in the error message. You can do this easily by copying the type of
the instance (the output of `#check @my_instance`), turning this into an example and removing the
last argument in square brackets. Prove the example using `by apply_instance`.
For example, if `additive.topological_add_group` raises an error, run

example {G : Type*} [topological_space G] [group G] : topological_add_group (additive G) :=
by apply_instance

(3) What error do you get?
(3a) If the error is "tactic.mk_instance failed to generate instance",
there might be nothing wrong. But it might take unreasonably long for the type-class inference to
fail. Check the trace to see if type-class inference takes any unnecessary long unexpected turns.
If not, feel free to increase the value in the definition of the linter `fails_quickly`.
(3b) If the error is "maximum class-instance resolution depth has been reached" there is almost
certainly a loop in the type-class inference. Find which instance causes the type-class inference to
go astray, and fix that instance. -/
#check @is_cyclotomic_extension.number_field /- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
State:
S : set ℕ+,
K : Type w,
L : Type z,
_inst_4 : field K,
_inst_5 : field L,
_inst_6 : algebra K L,
h : number_field K,
_inst_7 : fintype ↥S
⊢ number_field L -/
#check @cyclotomic_field.char_zero /- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
State:
n : ℕ+,
K : Type w,
_inst_4 : field K
⊢ char_zero (cyclotomic_field n K) -/
#check @cyclotomic_field.is_cyclotomic_extension /- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
State:
n : ℕ+,
K : Type w,
_inst_4 : field K
⊢ is_cyclotomic_extension {n} K (cyclotomic_field n K) -/
#check @is_alg_closed_of_char_zero.is_cyclotomic_extension /- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
State:
K : Type w,
_inst_4 : field K,
_inst_7 : is_alg_closed K,
S : set ℕ+
⊢ is_cyclotomic_extension S K K -/

/- The `dangerous_instance` linter reports: -/
/- DANGEROUS INSTANCES FOUND.
These instances are recursive, and create a new type-class problem which will have metavariables.
Possible solution: remove the instance attribute or make it a local instance instead.

Currently this linter does not check whether the metavariables only occur in arguments marked with `out_param`, in which case this linter gives a false positive. -/
#check @is_cyclotomic_extension.number_field /- The following arguments become metavariables. argument 1: (S : set ℕ+), argument 2: (K : Type w) -/
#check @is_cyclotomic_extension.finite_dimensional /- The following arguments become metavariables. argument 1: (S : set ℕ+) -/
#check @is_cyclotomic_extension.is_galois /- The following arguments become metavariables. argument 1: (n : ℕ+) -/

/- The `instance_priority` linter reports: -/
/- DANGEROUS INSTANCE PRIORITIES.
The following instances always apply, and therefore should have a priority < 1000.
If you don't know what priority to choose, use priority 100.
See note [lower instance priority] for instructions to change the priority. -/
#check @is_cyclotomic_extension.number_field /- set priority below 1000 -/
#check @is_cyclotomic_extension.finite_dimensional /- set priority below 1000 -/
#check @is_cyclotomic_extension.is_galois /- set priority below 1000 -/

Eric Rodriguez (Jul 14 2022 at 16:59):

Chris Birkbeck (Jul 14 2022 at 17:04):

I don't really understand these issues, but I'm also having trouble with our cycl_rat.lean file. If I open it it starts to use up all of my RAM

Chris Birkbeck (Jul 14 2022 at 17:04):

I don't know if its at all related

Eric Rodriguez (Jul 14 2022 at 17:08):

did you build the project before opening that file? i think it's farily deep in the imports

Chris Birkbeck (Jul 14 2022 at 17:08):

I thought I did. Let me try again.

Chris Birkbeck (Jul 14 2022 at 17:11):

So yeah even building before doesn't help. Its weird because the orange bars disappear but the RAM usage just keeps going up and up

Eric Rodriguez (Jul 14 2022 at 17:12):

yikes, I can't repro that but can't be good either:/

Chris Birkbeck (Jul 14 2022 at 17:18):

Oh ok fixed. I dunno what it was, but I hadn't noticed my local version was behind, so after pulling and building its now working fine

Riccardo Brasca (Jul 14 2022 at 17:29):

So do we have a problem or not?

Chris Birkbeck (Jul 14 2022 at 17:30):

I think my problem was unrelated to what Eric was talking about. But I don't understand his problem

Riccardo Brasca (Jul 14 2022 at 17:31):

@Eric Rodriguez where did you get the error? CI seems happy

Eric Rodriguez (Jul 14 2022 at 17:32):

just stick #lint at the end of the file

Eric Rodriguez (Jul 14 2022 at 17:33):

CI won't mind because these are all localised instances, and these locales don't get opened to lint

Riccardo Brasca (Jul 14 2022 at 17:37):

With the current master I get

/- Checking 50 declarations (plus 32 automatically generated ones) in the current file with 26 linters -/

/- The `fintype_finite` linter reports: -/
/- USES OF `fintype` SHOULD BE REPLACED WITH `casesI nonempty_fintype _` IN THE PROOF. -/
#check @is_cyclotomic_extension.finite /- The following `fintype` hypotheses should be replaced with
                      `casesI nonempty_fintype _` in the proof. argument 8: [h₁ : fintype ↥S] -/
#check @is_cyclotomic_extension.number_field /- The following `fintype` hypotheses should be replaced with
                      `casesI nonempty_fintype _` in the proof. argument 8: [_inst_7 : fintype ↥S] -/
#check @is_cyclotomic_extension.integral /- The following `fintype` hypotheses should be replaced with
                      `casesI nonempty_fintype _` in the proof. argument 9: [_inst_9 : fintype ↥S] -/
#check @is_cyclotomic_extension.finite_dimensional /- The following `fintype` hypotheses should be replaced with
                      `casesI nonempty_fintype _` in the proof. argument 5: [_inst_7 : fintype ↥S] -/

Eric Rodriguez (Jul 14 2022 at 17:38):

try maybe putting open_locale cyclotomic before it?

Riccardo Brasca (Jul 14 2022 at 17:39):

Let me try (BTW I wasn't aware of this fintype linter, does someone want to open a PR fixing the errors?)

Eric Rodriguez (Jul 14 2022 at 17:40):

(yes it's new, I'm not sure exactly how to change it, but we can definitely try to fix it)

Riccardo Brasca (Jul 14 2022 at 17:40):

OK, I get your error

Riccardo Brasca (Jul 14 2022 at 17:43):

I don't have time now to investigate this, I can do it tomorrow, but maybe there is just some loop I don't see

Eric Rodriguez (Jul 14 2022 at 17:43):

I see where some of them loop from, but I don't get some of the other loops

Riccardo Brasca (Jul 15 2022 at 13:26):

What is the loop you found?

Riccardo Brasca (Jul 15 2022 at 14:09):

Ah I see, there is at least one related to number_field and char_zero.

Last updated: Dec 20 2023 at 11:08 UTC