Skip to content

Refactor JS worker for Try Why3 #1351

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.

Sign up for GitHub

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

Draft
Halbaroth wants to merge 7 commits into
base: next
Choose a base branch
from
Draft

Refactor JS worker for Try Why3 #1351

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
936386a
Refactor JS worker for Try Why3
Halbaroth Apr 30, 2026
22b9d64
Provide `caml_unix_setitimer`, `caml_unix_kill` and `caml_unix_getpid…
Halbaroth May 11, 2026
28fa57f
Add a steps bound field in the worker example
Halbaroth May 12, 2026
5c39e64
Initialize Steps.steps_bound in the JavaScript worker
Halbaroth May 13, 2026
db01840
Hotfix for the issue 1348
Halbaroth Apr 30, 2026
cf3b2d1
Linter
Halbaroth May 13, 2026
88fdc71
Reinitialize steps bound of Steps module before treating requests
Halbaroth May 20, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 12 additions & 1 deletion rsc/extra/worker_example.html
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,22 @@
<!doctype html>

<html>
<head>
<meta charset="utf-8">
<title>Alt-Ergo JS</title>
<meta name="description" content="Alt-Ergo Js">
<meta name="author" content="Alt-Ergo dev team">
<style>
textarea {
width: 30%;
min-height: 300px;
}

.regular, .diagnostic {
width: 30%;
min-height: 100px;
border: 1px black solid;
}
</style>
<!-- ENTRY POINT -->
<script type="text/javascript" src="alt-ergo-example.js"></script>
</head>
Expand Down
1 change: 1 addition & 0 deletions src/bin/js/options_interface.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,7 @@ let set_options r =
set_options_opt Options.set_age_bound r.age_bound;
set_options_opt Options.set_fm_cross_limit (get_numbers r.fm_cross_limit);
set_options_opt Options.set_steps_bound r.steps_bound;
set_options_opt Steps.set_steps_bound r.steps_bound;

set_options_opt Options.set_output_format
(get_output_format r.output_format);
Expand Down
142 changes: 48 additions & 94 deletions src/bin/js/worker_example.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,14 +33,14 @@ module Html = Dom_html
let document = Html.window##.document

(* Example of the file to prove *)
let file = ref "goal g : true"
let file = ref "(set-logic ALL)\n(check-sat)"

(* This is the extension needed for the parser and corresponding to the input
file format*)
let extension = ref ".ae"
let extension = ref ".psmt2"

(* Timeout *)
let timeout = ref 100.
let steps_bound = ref 10000

(* Function that run the worker. *)
let exec worker file options =
Expand All @@ -61,15 +61,16 @@ let exec worker file options =
(* Create the web worker and launch 2 threads.
The first one for the timeout,
the second on for the call to Alt-Ergo through his web worker *)
let solve () =
let solve ?steps_bound () =
let options =
{(Worker_interface.init_options ()) with
input_format = None;
debug = Some true;
verbose = Some true;
debug = Some false;
verbose = Some false;
steps_bound;
answers_with_loc = Some false;
sat_solver = Some Worker_interface.Tableaux;
unsat_core = Some true;
sat_solver = Some Worker_interface.CDCL_Tableaux;
unsat_core = Some false;
} in

let worker = Worker.create "./alt-ergo-worker.js" in
Expand Down Expand Up @@ -111,22 +112,30 @@ let string_input f area_name area =
Dom.appendChild res (Html.createBr document);
res

let float_input name value =
type 'a parser = { of_string : string -> 'a; to_string : 'a -> string }

let generic_input { of_string; to_string } name value =
let res = document##createDocumentFragment in
Dom.appendChild res (document##createTextNode (Js.string name));
Dom.appendChild res (Html.createBr document);
let input = Html.createInput document in
input##.value := Js.string (string_of_float !value);
input##.value := Js.string (to_string !value);
input##.onchange :=
Html.handler (fun _ ->
(try value := float_of_string (Js.to_string input##.value)
(try value := of_string (Js.to_string input##.value)
with Invalid_argument _ -> ());
input##.value := Js.string (string_of_float !value);
input##.value := Js.string (to_string !value);
Js._false);
Dom.appendChild res input;
Dom.appendChild res (Html.createBr document);
res

let float_input =
generic_input { of_string = float_of_string; to_string = string_of_float }

let int_input =
generic_input { of_string = int_of_string; to_string = string_of_int }

let button name callback =
let res = document##createDocumentFragment in
let input = Html.createInput ~_type:(Js.string "submit") document in
Expand All @@ -140,49 +149,23 @@ let process_results = function
Some (String.concat "" r)
| None -> None

let result = document##createTextNode (Js.string "")
(* update result text area *)
let print_res = function
| Some res ->
result##.data := Js.string res
| None -> ()

let error = document##createTextNode (Js.string "")
(* update error text area *)
let print_error = function
| Some err ->
error##.data := Js.string err
| None -> ()
let regular =
let div = Html.createDiv document in
div##.className := Js.string "regular";
div

let warning = document##createTextNode (Js.string "")
(* update warning text area *)
let print_warning = function
| Some wrn ->
warning##.data := Js.string wrn
let print_regular v =
match v with
| Some s ->
regular##.innerText := Js.string s
| None -> ()

let debug = document##createTextNode (Js.string "")
(* update error text area *)
let print_debug = function
| Some dbg ->
debug##.data := Js.string dbg
| None -> ()

let model = document##createTextNode (Js.string "")
(* update model text area *)
let print_model = function
| Some mdl ->
model##.data := Js.string mdl
| None -> ()

let unsat_core = document##createTextNode (Js.string "")
(* update unsat core text area *)
let print_unsat_core = function
| Some usc -> unsat_core##.data := Js.string usc
| None -> ()
let diagnostic =
let div = Html.createDiv document in
div##.className := Js.string "diagnostic";
div

let statistics = document##createTextNode (Js.string "")
(* update statistics text area *)
let print_statistics = function
| None -> ()
| Some l ->
Expand All @@ -197,75 +180,46 @@ let print_statistics = function
) "" l in
statistics##.data := Js.string stats

let print_diagnostic v =
match v with
| Some s ->
diagnostic##.innerText := Js.string s
| None -> ()

let onload _ =
let main = Js.Opt.get (document##getElementById (Js.string "main"))
(fun () -> assert false) in
(* Create a text area for the input file *)
Dom.appendChild main
(string_input Html.createTextarea "Input file to solve" file);
Dom.appendChild main (Html.createBr document);
(* Create a text area for the extension format *)
Dom.appendChild main (string_input Html.createInput "Extension" extension);
Dom.appendChild main (Html.createBr document);
(* Create a text area for the timeout value *)
Dom.appendChild main (float_input "Timeout" timeout);
Dom.appendChild main (Html.createBr document);
(* Create a button to start the solving *)
Dom.appendChild main (int_input "Steps bound" steps_bound);
Dom.appendChild main (Html.createBr document);
Dom.appendChild
main
(button "Ask Alt-Ergo" (fun _ ->
let div = Html.createDiv document in
Dom.appendChild main div;
Lwt_js_events.async (fun () ->
(* Print "solving" until the end of the solving
or until the timeout *)
print_res (Some "Solving");
print_error (Some "");
let%lwt res = solve () in
(* Update results area *)
print_res (process_results res.regular);
(* Update errors area if errors occurs at solving *)
print_error (process_results res.diagnostic);
(* Update warning area if warning occurs at solving *)
print_warning (process_results res.diagnostic);
(* Update debug area *)
print_debug (process_results res.diagnostic);
(* Update model *)
print_model (process_results res.regular);
(* Update unsat core *)
print_unsat_core (process_results res.regular);
(* Update statistics *)
print_regular (Some "Solving");
print_diagnostic (Some "");
let%lwt res = solve ~steps_bound:!steps_bound () in
print_regular (process_results res.regular);
print_diagnostic (process_results res.diagnostic);
print_statistics res.statistics;
Lwt.return_unit);
Js._false));
Dom.appendChild main (Html.createBr document);
Dom.appendChild main (Html.createBr document);
(* Create a text area for the results *)
Dom.appendChild main result;
Dom.appendChild main (Html.createBr document);
Dom.appendChild main (Html.createBr document);
(* Create a text area for the errors *)
Dom.appendChild main error;
Dom.appendChild main (Html.createBr document);
Dom.appendChild main (Html.createBr document);
(* Create a text area for the warning *)
Dom.appendChild main warning;
Dom.appendChild main (Html.createBr document);
Dom.appendChild main (Html.createBr document);
(* Create a text area for the debug *)
Dom.appendChild main debug;
Dom.appendChild main (Html.createBr document);
Dom.appendChild main (Html.createBr document);
(* Create a text area for the model *)
Dom.appendChild main model;
Dom.appendChild main regular;
Dom.appendChild main (Html.createBr document);
Dom.appendChild main (Html.createBr document);
(* Create a text area for the unsat_core *)
Dom.appendChild main unsat_core;
Dom.appendChild main diagnostic;
Dom.appendChild main (Html.createBr document);
Dom.appendChild main (Html.createBr document);
(* Create a text area for the statistics *)
Dom.appendChild main statistics;
Js._false

let _ = Html.window##.onload := Html.handler onload
Loading
Loading