fix(create_deprecated_modules): fix the build again#37391
fix(create_deprecated_modules): fix the build again#37391grunweg wants to merge 17 commits intoleanprover-community:masterfrom
Conversation
… to the string api One universe error remains (which causes a second error further below). A number of deprecation warnings seem not worth fixing right now.
PR summary cbd9a3d070Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
grunweg
added
CI
✅ PR Title Formatted CorrectlyThe title of this PR has been updated to match our commit style conventions. |
|
I added one more workaround of the same kind: now things are failing a few lines below, with the same error. Argh. |
Co-authored-by: damiano <[email protected]>
…o deprecatemodule
|
Has there been a recent change to how |
grunweg
changed the title
|
Yes, there have (good catch!). The |
|
I have cleaned up the code and annotated all warnings: from my side, this is good to go (and we should investigate the workarounds). |
|
I asked about the String API on zulip. |
|
Robin suggested a much nicer way to deal with the elaboration issue. \o/ |
adomani
left a comment
adomani
left a comment
There was a problem hiding this comment.
This seems to be converging to a much better use of the String API: thanks a lot!
adomani
left a comment
adomani
left a comment
There was a problem hiding this comment.
Very minor comments, none of which is required.
Co-authored-by: damiano <[email protected]>
This would have caught the errors fixed by leanprover-community#37391 much sooner. The list of scripts included in this PR is based on manual inspection of scripts/, and removing any which get run using any PR's CI run anyway.
This would have caught the errors fixed by leanprover-community#37391 much sooner. The list of scripts included in this PR is based on manual inspection of scripts/, and removing any which get run using any PR's CI run anyway.
2 participants
The code needed updating to the new String API; it failed to build before this PR.
This also removes uses of deprecated String API.
A future PR will add CI to ensure this script builds fine.
(Future future: can we test that we tested all .lean scripts? Or have a test which builds all .lean files in scripts?)
We need to annotate a type as
Charnow, perhaps because the default instances (from aCharto aSlice.Pattern) don't work out as well any more.