Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Increase minimal version of Zarith #816

Merged
merged 1 commit into from
Sep 13, 2023

Conversation

Halbaroth
Copy link
Collaborator

@Halbaroth Halbaroth commented Sep 13, 2023

We have to increase the minimal version of Zarith. Indeed, the function Q.of_string does not support decimal notation before Zarith > 1.11. See ocaml/Zarith#65

This issue cannot be detected by the opam repository CI as the command dune build @runtest-ci isn't running by this CI and the issue occurs only using both a switch with lower bounds and the frontend dolmen.

I run tests locally and it should work now.

To prevent such situations from recurring, I suggest to use the alias runtest to run all the tests and runtest-something to run locally quick tests.

As soon as opam 2.2 is stable, I will modify the CI in order to check lower bounds.

I also add ppxlib < 0.30.0 as a conflict instead of a dependency.

We have to backport this PR again...

@Halbaroth Halbaroth added this to the 2.6.0 milestone Sep 13, 2023
@bclement-ocp
Copy link
Collaborator

Ah, indeed, good catch. Not sure I understand why this is not caught by dune build @runtest: this looks like a parsing issue and we should dune build @runtest should parse all the test files (we just don't run them with all the different solvers/options)?

@bclement-ocp
Copy link
Collaborator

Ah, indeed, good catch. Not sure I understand why this is not caught by dune build @runtest: this looks like a parsing issue and we should dune build @runtest should parse all the test files (we just don't run them with all the different solvers/options)?

Oh wait we generate tests with the runtest-quick target by default, not runtest. Yeah, the dolmen and legacy suites at least should be run on the runtest alias.

@Halbaroth Halbaroth merged commit 87b5253 into OCamlPro:next Sep 13, 2023
14 checks passed
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this pull request Sep 15, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants