Skip to content

chore: bump to Lean 4.26#49

Draft
RSoulatIOHK wants to merge 1 commit intochore-bump-lean-4.25from
chore-bump-lean-4.26
Draft

chore: bump to Lean 4.26#49
RSoulatIOHK wants to merge 1 commit intochore-bump-lean-4.25from
chore-bump-lean-4.26

Conversation

@RSoulatIOHK
Copy link
Collaborator

Very minimal bump to ensure building and no deprecation warnings

Description

Type of Change

  • Bug fix (non-breaking change fixing an issue)
  • New feature (non-breaking change adding functionality)
  • Breaking change (fix or feature causing existing functionality to change)
  • Documentation update
  • Performance improvement
  • Code refactoring
  • Test updates

Related Issue

Use any of the following for our ticket management to know which tickets to move to Done when PR is merged:

  • Fixes #(issue number)
  • Closes #(issue number)

Changes Made

  • Updated the Lean toolchain from version v4.25.0 to v4.26.0 in lean-toolchain, ensuring compatibility with the latest features and bug fixes.

  • In Blaster/Optimize/Rewriting/OptimizeString.lean, corrected the string construction in normStringValue by replacing String.mk elms.toList with String.ofList elms.toList as the former was being deprecated. Followed the tip given by the deprecation message.

Testing

Test Coverage

  • Added new tests for new functionality
  • Updated existing tests
  • All tests pass locally
  • For bug fixes: Added example to Tests/Issues/ folder

Documentation

  • README updated (if applicable)
  • Code comments added/updated
  • Doc comments added for new optimization/rewritting rules
  • My code follows the project's style guidelines
  • I have performed a self-review of my code
  • I have commented my code, particularly in hard-to-understand areas
  • I have made corresponding changes to the documentation
  • I have added tests that prove my fix is effective or that my feature works
  • New and existing unit tests pass locally with my changes using make check_all
  • For bug fixes: Original failing example added to Tests/Issues/ folder with reference to issue number

Additional Notes

Very minimal bump to ensure building and no deprecation warnings
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant