Use Dolmen in the JS worker #1249

Halbaroth · 2024-10-07T10:22:07Z

This PR removes the dependency of the Javascript worker to the legacy
frontend in order to remove it completely. In order to avoid code
duplication as it was done with the legacy frontend, we reuse the
Solving_loop module in the worker. This requires some modifications:

Add a new argument to the main function of Solving_loop to give
different kind of sources instead of reading the file at the path
Options.get_file (). The worker used a raw string as input. I reused
the type Dolmen_loop.State.source.
Add a new argument to the main function of Solving_loop to pass the
selector hook to the constructor of the environment of the SAT solver.
This hook is not used by the worker to select instantiations but just to
record them. I have no strong opinion to preserve this feature but I
try to keep all the feature of the Javascript worker.
Remove the unused sat_env argument of the constructor init_env in
Frontend. This removal is mostly motivated by the fact the semantic
of init_env = Some env + selector_inst = Some f is not clear at
all.
Monomophize the status type in Frontend. This status is only used
for printting purposes but we kept the SAT environment in some of its
constructors. Unfortunately, the type of the SAT can change at the
very beginning of the main function of Solving_loop, which means it
is not easy to add a new argument for the hook_status. This hook is
required to print the result of AE in the worker.

This PR removes the dependency of the Javascript worker to the legacy frontend in order to remove it completely. In order to avoid code duplication as it was done with the legacy frontend, we reuse the `Solving_loop` module in the worker. This requires some modifications: - Add a new argument to the main function of `Solving_loop` to give different kind of sources instead of reading the file at the path `Options.get_file ()`. The worker used a raw string as input. I reused the type `Dolmen_loop.State.source`. - Add a new argument to the main function of `Solving_loop` to pass the selector hook to the constructor of the environment of the SAT solver. This hook is not used by the worker to select instantiations but just to record them. I have no strong opinion to preserve this feature but I try to keep all the feature of the Javascript worker. - Remove the unused `sat_env` argument of the constructor `init_env` in `Frontend`. This removal is mostly motivated by the fact the semantic of `init_env = Some env` + `selector_inst = Some f` is not clear at all. - Monomophize the `status` type in `Frontend`. This status is only used for printting purposes but we kept the SAT environment in some of its constructors. Unfortunately, the type of the SAT can change at the very beginning of the main function of `Solving_loop`, which means it is not easy to add a new argument for the `hook_status`. This hook is required to print the result of AE in the worker.

bclement-ocp

Overall looks good to me --- I think we can simplify handling of input files with Gbury/dolmen#201 and maybe get rid of Compat.In_channel.input_all entirely. If you have time to look into it it'd be great, but it's not important and I'm OK merging as is as well.

bclement-ocp · 2024-10-07T10:39:17Z

src/bin/common/solving_loop.ml

+      | `Stdin when is_incremental ->
+        set_output_format ".smt2";
+        `Stdin
+      | `Stdin ->
+        `Raw (filename, Compat.In_channel.input_all stdin)


I believe this is no longer necessary since Gbury/dolmen#201 and can be replaced with:

Suggested change

| `Stdin when is_incremental ->

set_output_format ".smt2";

`Stdin

| `Stdin ->

`Raw (filename, Compat.In_channel.input_all stdin)

| `Stdin -> `Stdin

(And the definition for is_incremental removed)

bclement-ocp · 2024-10-07T10:42:31Z

src/bin/common/solving_loop.ml

+        let cin = open_in path in
+        let content = Compat.In_channel.input_all cin in
+        close_in cin;
+        `Raw (filename, content)


Note to self: not sure why we had this, I think this can just be `File path (provided that we call set_output_format first)?

bclement-ocp · 2024-10-07T10:46:31Z

src/bin/js/worker_js.ml

    let res = Worker_interface.init_results () in
+    let msg = Fmt.str "Unknown error: %s" (Printexc.to_string exn) in


Actually, this is not sufficient to catch some errors because the worker is running into Lwt monad and the backtrace is sometimes lost.

It is still better for the ones we do catch — I'll take an improvement over what we had before even if it is not perfect!

bclement-ocp · 2024-10-07T10:49:26Z

src/lib/frontend/frontend.ml

+  | Sat of Commands.sat_tdecl
+  | Unknown of Commands.sat_tdecl


I am slightly surprised that we were never using these environments, but if that is the case, there is no point to keep them anyways.

Me too. Our API is such an onion with too many layers, we didn't notice it before.

bclement-ocp · 2024-10-07T10:59:28Z

src/lib/util/compat.ml

@@ -153,3 +153,99 @@ module Type = struct
      match A.Id with B.Id -> Some Equal | _ -> None
  end
 end
+
+module In_channel = struct
+  open In_channel


Ah yes unfortunately that one is not going to work since the module itself was added in 4.14; bummer.

Halbaroth · 2024-10-07T11:00:48Z

Overall looks good to me --- I think we can simplify handling of input files with Gbury/dolmen#201 and maybe get rid of Compat.In_channel.input_all entirely. If you have time to look into it it'd be great, but it's not important and I'm OK merging as is as well.

Unfortunately, we still need input_all for the zip format. We may create a temporary file and read it instead of loading all the file in a string.

bclement-ocp · 2024-10-07T11:05:39Z

Overall looks good to me --- I think we can simplify handling of input files with Gbury/dolmen#201 and maybe get rid of Compat.In_channel.input_all entirely. If you have time to look into it it'd be great, but it's not important and I'm OK merging as is as well.

Unfortunately, we still need input_all for the zip format. We may create a temporary file and read it instead of loading all the file in a string.

I think for the zip format we use My_zip.extract_zip_file which does not use input_all? We are using input_all for the case of non-zip file, but I believe that passing `File path to Dolmen instead of reading the file ourselves should work.

We do not need `In_channel.input_all` too ;)

Halbaroth added 2 commits October 3, 2024 18:39

Add In_channel.input_all in Compat

f193259

Halbaroth changed the title ~~Dolmen worker js bis~~ Use Dolmen in the JS worker Oct 7, 2024

Halbaroth added javascript frontend labels Oct 7, 2024

Halbaroth mentioned this pull request Oct 7, 2024

Supporting exit on error in Javascript mode #1250

Closed

Halbaroth force-pushed the dolmen-worker-js-bis branch from cf1ecbf to 3a3a8b8 Compare October 7, 2024 10:37

Fix input format in the JS example

3a3a8b8

bclement-ocp approved these changes Oct 7, 2024

View reviewed changes

bclement-ocp reviewed Oct 7, 2024

View reviewed changes

Simplify mk_files in Solving_loop

27cf381

We do not need `In_channel.input_all` too ;)

Halbaroth merged commit bc49809 into OCamlPro:next Oct 7, 2024
17 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use Dolmen in the JS worker #1249

Use Dolmen in the JS worker #1249

Halbaroth commented Oct 7, 2024

bclement-ocp left a comment

bclement-ocp Oct 7, 2024

bclement-ocp Oct 7, 2024

bclement-ocp Oct 7, 2024

Halbaroth Oct 7, 2024

bclement-ocp Oct 7, 2024

bclement-ocp Oct 7, 2024

Halbaroth Oct 7, 2024

bclement-ocp Oct 7, 2024

Halbaroth Oct 7, 2024

Halbaroth commented Oct 7, 2024 •

edited

Loading

bclement-ocp commented Oct 7, 2024

		let res = Worker_interface.init_results () in
		let msg = Fmt.str "Unknown error: %s" (Printexc.to_string exn) in

Use Dolmen in the JS worker #1249

Use Dolmen in the JS worker #1249

Conversation

Halbaroth commented Oct 7, 2024

bclement-ocp left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth commented Oct 7, 2024 • edited Loading

bclement-ocp commented Oct 7, 2024

Halbaroth commented Oct 7, 2024 •

edited

Loading