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

Locking the Dolmen to a dev commit #893

Merged
merged 1 commit into from
Oct 18, 2023

Conversation

Halbaroth
Copy link
Collaborator

@Halbaroth Halbaroth commented Oct 16, 2023

This commit locks the Dolmen used by AE to a specific commit in order to use the unreleased feature for custom statements (see #892).

I also notice that the with_cache in d_cnf was silently shadow by the same function from the module Expr of Dolmen. The signature of this latter changed recently. I fix it by using the with_cache from Dolmen. Notice that the hash table of the cache is hidden in the closure of with_cache and bv2nat and int2bv don't share their cache as before.

@Halbaroth Halbaroth added this to the 2.6.0 milestone Oct 16, 2023
Copy link
Collaborator

@bclement-ocp bclement-ocp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think the caches for bv2nat and int2bv were shared before?

@bclement-ocp
Copy link
Collaborator

Well we do need a Dolmen version that is compatible with 4.08 though, Gbury/dolmen#195

Copy link
Collaborator

@bclement-ocp bclement-ocp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually now that I think about it -- I think it would be better to do this in the PR that will solve #892 so that we can track (using git log / git blame) the actual reason why we bump the dependencies.

@Halbaroth
Copy link
Collaborator Author

I don't think the caches for bv2nat and int2bv were shared before?

I know. I said I checked it was still the case after this commit.

@Halbaroth
Copy link
Collaborator Author

Halbaroth commented Oct 16, 2023

Actually now that I think about it -- I think it would be better to do this in the PR that will solve #892 so that we can track (using git log / git blame) the actual reason why we bump the dependencies.

Actually this commit was the very first commit of my PR for MaxSMT. I prefer separate it and create an remainder issue on this PR to remind we have to revert the lock before releasing.

@bclement-ocp
Copy link
Collaborator

I don't think the caches for bv2nat and int2bv were shared before?

I know. I said I checked it was still the case after this commit.

Ah, sorry — I parsed "bv2nat and int2bv don't share their cache as before." as stating that bv2nat and int2bv shared their cache before but no longer do.

@Halbaroth
Copy link
Collaborator Author

I don't think the caches for bv2nat and int2bv were shared before?

I know. I said I checked it was still the case after this commit.

Ah, sorry — I parsed "bv2nat and int2bv don't share their cache as before." as stating that bv2nat and int2bv shared their cache before but no longer do.

My sentence was very misleading ;)

@Halbaroth
Copy link
Collaborator Author

I prefer waiting the fix for Dolmen as we will need to change the lock again.

This commit locks the Dolmen used by AE to a specific commit
in order to use the unreleased feature for custom statements.

I also notice that the `with_cache` in `d_cnf` was silently shadow by
the same function from the module `Expr` of `Dolmen`. The signature of
this latter changed recently. I fix it by using the `with_cache` from
Dolmen. Notice that the hash table of the cache is hidden in the closure
of `with_cache` and `bv2nat` and `int2bv` don't share their cache as
before.
@Halbaroth Halbaroth merged commit dc172b8 into OCamlPro:next Oct 18, 2023
14 checks passed
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this pull request Oct 19, 2023
After OCamlPro#893 the version of dolmen in the sources.json no longer works.
Also bumps the pinned nixpkgs.
bclement-ocp added a commit that referenced this pull request Oct 19, 2023
After #893 the version of dolmen in the sources.json no longer works.
Also bumps the pinned nixpkgs.
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this pull request Nov 2, 2023
It seems the lock file haven't been updated correctly in the PR OCamlPro#893.
We have to lock `dolmen` to the dev version.
@Halbaroth Halbaroth mentioned this pull request Nov 2, 2023
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this pull request Nov 2, 2023
It seems the lock file haven't been updated correctly in the PR OCamlPro#893.
We have to lock `dolmen` to the dev version.
Halbaroth added a commit that referenced this pull request Nov 6, 2023
It seems the lock file haven't been updated correctly in the PR #893.
We have to lock `dolmen` to the dev version.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants