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:
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:
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
.
Last updated: Dec 20 2023 at 11:08 UTC