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

Support dolmen frontend in JS worker #1232

Closed
bclement-ocp opened this issue Sep 5, 2024 · 4 comments
Closed

Support dolmen frontend in JS worker #1232

bclement-ocp opened this issue Sep 5, 2024 · 4 comments

Comments

@bclement-ocp
Copy link
Collaborator

          > I think Try Alt-Ergo is currently broken but I don't think that should block the release.

More precisely worker_js.ml does not seem to be compatible with dolmen.

Originally posted by @bclement-ocp in #1218 (comment)

@Halbaroth
Copy link
Collaborator

When I try to run the worker example as follows:
dune exec -- src/bin/js/worker_example.exe
I got:

Fatal error: Unimplemented Javascript primitive caml_js_expr!
fish: Job 1, 'dune exec -- src/bin/js/worker_…' terminated by signal SIGABRT (Abort)

Is it the issue you ran into?

@bclement-ocp
Copy link
Collaborator Author

I don't think calling src/bin/js/worker_example.exe is supposed to work. The way to run the js example is to build with make js-example and then run from the www directory.

The issue is that the worker always uses the legacy frontend, but tries to find a "dolmen" type. The easy fix is to force the use of the "legacy" frontend in the JS worker; the long-term fix is to modify the JS worker to use the dolmen frontend instead of the legacy frontend.

@bclement-ocp
Copy link
Collaborator Author

bclement-ocp commented Sep 6, 2024

The way I run the worker is as follows (you can't simply open the www/index.html file; you run into restrictions in the browser that refuses to execute javascript from the file:// protocol):

$ make js-example
$ python -m http.server -d www

Sending a file with "Ask Alt-Ergo" returns an error in the dev console:

{ "worker_id": 42, "status": { "Error": "Unknown error" } }

and if I print the exception in src/bin/js/worker_js.ml:

diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml
index 4d79920d..484d7812 100644
--- a/src/bin/js/worker_js.ml
+++ b/src/bin/js/worker_js.ml
@@ -259,11 +259,11 @@ let main worker_id content =
       Worker_interface.diagnostic =
         Some [Format.asprintf "%a" Errors.report e]
     }
-  | _ ->
+  | exn ->
     let res = Worker_interface.init_results () in
     { res with
       Worker_interface.worker_id = worker_id;
-      Worker_interface.status = Error "Unknown error";
+      Worker_interface.status = Error ("Unknown error: " ^ Printexc.to_string exn);
     }
 
 (** Worker initialisation

we get a more detailed error:

{ "worker_id": 42,
  "status":
    { "Error":
        "Unknown error: AltErgoLib.Input.Method_not_registered(\"dolmen\")" } }

@Halbaroth
Copy link
Collaborator

Done in #556

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants