Dependencies and build updates for OCaml 4.14.1

hopv / rethfl

ReTHFL: νHFL(Z) (aka higher-order CHC) solver based on refinement types

0 stars 0 forks source link

Dependencies and build updates for OCaml 4.14.1 #2

Closed KenSakayori closed 5 months ago

KenSakayori commented 6 months ago

Now ReTHFL can be built with OCaml 4.14.1. Moreover, the repository has a proper package description and ReTHFL can easily be installed using opam.

TODOs:

[x] Update README
[x] Update the name. Probably rethfl is a better choice than hflmc3. At least we should completely remove the name hflmc2. (This can be done in another PR)
[ ] Check if there is a better way to write idMap.ml and idSet.ml
[ ] Run some test cases to see if there's any regression

(Update: I did a force push on Feb 11, just to modify my email address)

ryosu-sato commented 6 months ago

(I know it might not be appropriate to comment here...) Why is Id.remove_ty used in idMap.ml and idSet.ml in the first place? Is it not enough to implement Key.compare to use only name and id? Is there a situation where we want to use types for comparison? (If that is the case, I think it is enough to implement another version of Key module with a different compare function.)

KenSakayori commented 6 months ago

I don't know why it is implemented like this and @moratorium08 doesn't either. It should be enough to implement a custom Key.compare in id.ml. Then we can simply use normal accessors such as Set.add and Set.remove, which I consider a better practice.
(But I don't have a strong opinion on this.)

KenSakayori commented 6 months ago

I'll rebase this (and locally solve the conflicts) as the master branch has been updated

KenSakayori commented 6 months ago

Actually there wasn't any conflict, but, anyway, I rebased the branch on top of master

KenSakayori commented 5 months ago

Updates:

Renamed everything from hflmc2/3 to rethfl.
Created an opam.lock file, which we can update for every new release.

IMO this is ready for merge as long as @moratorium08 thinks this PR is okay. I myself cannot do a regression test.

moratorium08 commented 5 months ago

Confirmed there is no degradation, so this PR will be merged.