Skip to content

Conversation

@affeldt-aist
Copy link
Member

Motivation for this change

fixes #1687

I just observed that MathComp-Analysis 1.12.0 fails to compile with HB 1.7.0 and 1.7.1.
We could put the restriction in the opam file of analysis but since the restriction
is already in classical, I chose to modify classical only for the sake of simplicity, wdyt?

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@affeldt-aist affeldt-aist added this to the 1.13.0 milestone Jul 19, 2025
@affeldt-aist affeldt-aist requested a review from proux01 July 19, 2025 06:38
@affeldt-aist affeldt-aist added experiment 🧪 This issue/PR is very experimental build/continuous integration ⚙️ This issue/PR is about the build process or CI labels Jul 19, 2025
@proux01
Copy link
Collaborator

proux01 commented Jul 21, 2025

Thanks, we should probably add that bound to some CI bundle, otherwise we'll likely break it again in the future.

@proux01 proux01 merged commit 87451e9 into math-comp:master Jul 21, 2025
46 of 54 checks passed
yosakaon pushed a commit to yosakaon/analysis that referenced this pull request Dec 4, 2025
* fixes math-comp#1687

* fix other mentions of HB 1.7.0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

build/continuous integration ⚙️ This issue/PR is about the build process or CI experiment 🧪 This issue/PR is very experimental

Projects

None yet

Development

Successfully merging this pull request may close these issues.

MathComp-Analysis 1.12.0 requires at least HB 1.8.0

2 participants