Get rid of stdcompat
#1191
Merged
Get rid of stdcompat
#1191
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Halbaroth
force-pushed
the
get-rid-of-stdcompat
branch
from
30f1171 to
ead131b
Compare
We do not need to use `stdcompat` because we only need to support few new functions from `stdlib`. This PR removes the `stdcompat` dependency and create a new module `compat` which contains all the functions we need to compile on OCaml 4.08. I also rename `Lists` to `my_list` and `myUnix` to `my_unix` and now `my_list` only contains extra functions (which are not part of any stdlib versions).
bclement-ocp
requested changes
Jul 31, 2024
src/bin/common/parse_command.ml
Outdated
| @@ -462,13 +462,13 @@ let mk_theory_opt () no_contracongru | |||
| no_fm no_nla no_tcp no_theory restricted tighten_vars | |||
| _use_fpa (theories) | |||
| = | |||
| set_no_ac (not (Lists.mem Theories.equal Theories.AC theories)); | |||
| set_no_ac (not (My_list.mem Theories.equal Theories.AC theories)); | |||
There was a problem hiding this comment.
Nit: I think we could get rid of My_list.mem everywhere with List.exists (Theories.equal Theories.AC) theories. Not sure we want to.
src/lib/reasoners/records.ml
Outdated
| @@ -322,7 +322,7 @@ module Shostak (X : ALIEN) = struct | |||
| | Record (lbs, ty) -> | |||
| Record (List.map (fun (n,e') -> n, subst_access x s e') lbs, ty) | |||
| | Access (lb, e', _) when compare_mine x e' = 0 -> | |||
| Lists.assoc Uid.equal lb s | |||
| Compat.List.assoc Uid.equal lb s | |||
There was a problem hiding this comment.
Suggested change
| Compat.List.assoc Uid.equal lb s | |
| My_list.assoc Uid.equal lb s |
src/lib/util/my_list.ml
Outdated
Comment on lines
15
to
23
| (* The Alt-Ergo theorem prover *) | ||
| (* *) | ||
| (* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) | ||
| (* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) | ||
| (* *) | ||
| (* CNRS - INRIA - Universite Paris Sud *) | ||
| (* *) | ||
| (* --------------------------------------------------------------- *) | ||
| (* *) |
There was a problem hiding this comment.
This needs to stay since we simply rename the file while keeping the existing code.
src/lib/util/my_list.mli
Outdated
| (* CNRS - INRIA - Universite Paris Sud *) | ||
| (* *) | ||
| (* --------------------------------------------------------------- *) | ||
| (* *) | ||
| (* More details can be found in the directory licenses/ *) |
There was a problem hiding this comment.
Same, needs to stay.
src/lib/util/my_list.mli
Outdated
Comment on lines
28
to
33
| (** Lists utilies | ||
|
|
||
| This modules defines some helper functions on lists | ||
| *) | ||
|
|
||
| (** {3 Misc functions} *) |
src/lib/util/compat.ml
Outdated
| end | ||
|
|
||
| module Bytes = struct | ||
| include Bytes |
There was a problem hiding this comment.
I would argue it would be better to do open Bytes at the beginning of the module, and include Bytes at the end (with [@@@ocaml.warning "-32-33"] at the top of the file). This way, we would use the stdlib version when it is available and only fall back to our version if its not.
(Same for the List, Array, etc. in this module)
There was a problem hiding this comment.
I was looking for such trick in fact, thanks :)
bclement-ocp
approved these changes
Jul 31, 2024
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Aug 1, 2024
The syntax used for silencing warning in OCamlPro#1191 is incorrect.
Halbaroth
pushed a commit
that referenced
this pull request
Aug 1, 2024
The syntax used for silencing warning in #1191 is incorrect.
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Aug 2, 2024
The syntax used for silencing warning in OCamlPro#1191 is incorrect.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We do not need to use
stdcompatbecause we only need to support few new functions fromstdlib. This PR removes thestdcompatdependency and create a new modulecompatwhich contains all the functions we need to compile on OCaml 4.08.I also rename
Liststomy_listandmyUnixtomy_unixand nowmy_listonly contains extra functions (which are not part of any stdlib versions).