Commit 9085bdcf authored by Kim Nguyễn's avatar Kim Nguyễn

Make the number of steps and threads of alt-ergo configurable in trywhy3.

parent a55c1d04
......@@ -48,6 +48,8 @@ let run_alt_ergo_on_task text =
let () =
Options.set_steps_bound 100;
Worker.set_onmessage (fun msg ->
let (id, text) = unmarshal msg in
let result = run_alt_ergo_on_task text in
Worker.post_message (marshal (id,result)))
match unmarshal msg with
Task (id, text) ->
let result = run_alt_ergo_on_task text in
Worker.post_message (marshal (id,result))
| OptionSteps i -> Options.set_steps_bound i)
......@@ -147,24 +147,12 @@ function widescreenView()
{
var e = document.getElementById("editor");
var c = document.getElementById("console");
e.style.width = "50%";
e.style.width = "60%";
e.style.height = "100%";
c.style.width = "40%";
c.style.height = "100%";
editor.focus();
}
function prove()
{
document.getElementById("console").innerHTML = "<p>Execution feature is not yet implemented</p>";
console.focus();
editor.focus();
}
function prove()
{
document.getElementById("console").innerHTML = "<p>Call to Why3 is not yet implemented</p>";
editor.focus();
}
editor.focus();
@import url(fontawesome/fontawesome.css);
/* fontawesome */
[class*="fontawesome-"]:before {
font-family: 'FontAwesome', sans-serif;
}
/* ACE Editor */
.error {
position:absolute;
background:rgba(200,100,100,0.5);
z-index:40;
}
/* Interface */
body {
padding:0;
margin:0;
font-family: sans-serif;
}
#editor-panel {
height: 97vh;
box-sizing:border-box;
padding: 0;
margin: 0;
}
#editor {
position:relative;
font-size: large;
box-sizing: border-box;
display:inline-block;
height:100%;
margin:0 0 0 0;
padding:0 0 0 0;
z-index:0;
vertical-align:top;
border-right: 1pt #ddd solid;
border-bottom: 1pt #ddd solid;
width:59%;
}
#console {
box-sizing: border-box;
overflow: auto;
position:relative;
display:inline-block;
width:40%;
height:100%;
margin:0 0 0 0;
padding:0 0 0 0;
vertical-align:top;
}
/* CSS MENU BAR */
.menu-bar {
margin:0;
z-index:10;
font-size:2vh;
height:3vh;
padding:0;
}
.menu-bar:after {
content:"";
display:table;
clear:both;
}
.menu-bar ul {
padding:0;
margin:0;
list-style: none;
position: relative;
background-image: linear-gradient(to bottom, #eee, #ccc);
height:3vh;
z-index:10;
box-sizing:border-box;
}
/* Positioning the navigation items inline */
.menu-bar ul li {
margin: 0;
padding: 0;
display: inline-block;
float: left;
height: 100%;
box-sizing:border-box;
}
/* Styling the links */
.menu-bar > ul > li > span {
display:block;
padding:0pt 1em;
color:#444;
text-decoration:none;
border-radius: 5pt 5pt 0pt 0pt;
border-style:solid;
border-width:1pt;
border-color:transparent;
height:100%;
box-sizing:border-box;
margin:0;
}
/* Background color change on Hover */
.menu-bar > ul > li > span:hover {
background-image: linear-gradient(to bottom, #eee, #bbb);
border-color: #aaa;
box-sizing:border-box;
}
.menu-bar > ul > li > ul {
/* display:none;*/
height:0;
overflow:hidden;
box-sizing:border-box;
opacity: 0;
transition: opacity .3s ease-in-out;
-webkit-transition: opacity .3s ease-in-out;
-moz-transition: opacity .3s ease-in-out;
-o-transition: opacity .3s ease-in-out;
-ms-transition: opacity .3s ease-in-out;
}
.menu-bar > ul > li:hover > ul {
height:auto;
background-color:#ddd;
box-shadow:0pt 0pt 5pt #444;
opacity:1;
}
.menu-bar > ul > li > ul > li {
float:left;
display: inline-block;
clear:left;
width: 100%;
position: relative;
}
.menu-bar > ul > li > ul > li {
display:block;
padding:1pt 2pt 1pt 2pt;
color:#444;
text-decoration:none;
border-radius: 1pt;
border-style:solid;
border-width:1pt;
border-color:transparent;
box-sizing:border-box;
height: 100%;
}
.menu-bar > ul > li > ul > li:before {
display:inline-block;
content:"";
width:0pt;
height: 100%;
vertical-align:middle;
}
.menu-bar > ul > li > ul > li:hover {
border-color:#cce;
background-image: linear-gradient(to bottom, #abe, #68b);
}
/* Hidden file selector */
#file-selector {
position:absolute;
left:0;
top:0;
width:0;
height:0;
z-index:-1;
}
#editor-panel {
position:relative;
display:block;
box-sizing: border-box;
padding:0;
margin:0;
height:97vh;
}
#console ul#theory-list {
list-style-type: none;
list-style-position: inside;
padding: 0.5em;
/*margin: 0.5em; */
}
#console ul#theory-list li {
font-weight:bold;
}
#console ul#theory-list li * {
font-weight:normal;
}
#console ul ul {
list-style-type: square;
list-style-position: inside;
padding: 0.5em;
/*margin: 0.5em;*/
}
#console ul ul ul {
list-style-type: none;
list-style-position: inside;
padding: 0.5em;
/*margin: 0.5em; */
}
/* Confirmation dialog */
.btn {
width:100%;
z-index:1;
margin:0 0 4pt 0;
box-sizing:border-box;
}
#confirm-dialog {
z-index:20;
display:none;
position:absolute;
margin: 0 auto;
padding: 2pt 0;
width:50%;
left:25%;
right:25%;
top:20%;
border-radius:5pt;
background: #eee;
text-align:center;
}
#background-shadow {
display:none;
background-color: rgba(0,0,0,0.8);
position:absolute;
width:100%;
height:100%;
top: 0;
left:0;
z-index:15;
}
#confirm-dialog .btn {
width:40%;
}
<!-- This document was automatically generated with yamlpp
(see http://www.lri.fr/~filliatr/yamlpp.en.html),
with the following command:
yamlpp -l en src/trywhy3/index.prehtml -o src/trywhy3/index.en.html -->
<html xmlns="http://www.w3.org/1999/xhtml"
style="font-family:Verdana,Arial,Sans-Serif">
<head>
<title>
Try Why3
</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link rel="stylesheet" type="text/css" href="trywhy3.css" />
<!-- color customisation -->
<style>
</style>
</head>
<body>
<!--invisible elements for the open file dialog -->
<input type="file" id="file-selector" />
<div id="background-shadow">
<div id="confirm-dialog" >
The content of the current buffer will be lost
<br/>
<div style="width:70%; display:inline-block;">
<button class="btn"
onclick="confirmReplace();">
Confirm
</button>
<button class="btn"
onclick="cancelReplace();">
Cancel
</button>
</div>
</div>
</div>
<div class="menu-bar">
<ul>
<li><span>File</span>
<ul>
<li onclick="openFile();">
Open</li>
<li onclick="saveFile();">
Save as
</li>
</ul>
</li>
<li><span>Edit</span>
<ul>
<li onclick="editor.undo();">Undo</li>
<li onclick="editor.redo();">Redo</li>
<li onclick="clearBuffer();">Clear buffer</li>
</ul>
</li>
<li><span>Examples</span>
<ul>
<li id="drinkers">Drinker's paradox</li>
<li id="bin_mult">Binary Multiplication</li>
<li id="fact">Factorial</li>
<li id="isqrt">Integral square root</li>
</ul>
</li>
<li><span>Why3</span>
<ul>
<li id="run">Execute Buffer</li>
<li id="prove">Prove with Alt-Ergo</li>
<li id="stop">Stop Alt-ergo</li>
</ul>
</li>
<li><span>Preferences</span>
<ul>
<li onclick="document.getElementById('radio-wide').click();">
<input id="radio-wide" type="radio" name="view"
value="wide" checked="checked" onchange="widescreenView();"
/>
Split Vertically
</li>
<li onclick="document.getElementById('radio-std').click();">
<input id="radio-std" type="radio" name="view" value="std"
onchange="standardView();"
/>
Split Horizontally
</li>
<li>
<input id="input-num-threads" type="number" style="width:3em;" min="1" max="8"
value="4"></input></input> Number of threads for Alt-Ergo
</li>
<li>
<input id="input-num-steps" type="number" style="width:3em;" min="1" max="1000"
value="100"></input></input> Number of steps for Alt-Ergo
</li>
</ul>
</li>
<li style="float:right;"><span>Help</span></li>
</ul>
</div>
<div id="editor-panel">
<div id="editor" title="Editor" tabindex="-1" ></div>
<div title="Console" id="console">
</div>
</div>
<script defer="true" src="ace-builds/src-noconflict/ace.js"
type="text/javascript" charset="utf-8"></script>
<script defer="true" type="text/javascript"
src="editor_helper.js"></script>
<script defer="true" type="text/javascript"
src="trywhy3.js"></script>
</body>
</html>
......@@ -167,8 +167,8 @@ let task_queue = Queue.create ()
let first_task = ref true
type 'a status = Free of 'a | Busy of 'a | Absent
let num_workers = 4
let alt_ergo_workers = Array.make num_workers Absent
let alt_ergo_steps = ref 100
let alt_ergo_workers = ref (Array.make num_workers Absent)
let rec init_alt_ergo_worker i =
let worker = Worker.create "alt_ergo_worker.js" in
......@@ -176,7 +176,7 @@ let rec init_alt_ergo_worker i =
(Dom.handler (fun ev ->
let (id, result) = unmarshal (ev ## data) in
Console.print_alt_ergo_output id result;
alt_ergo_workers.(i) <- Free(worker);
!alt_ergo_workers.(i) <- Free(worker);
process_task ();
Js._false));
Free (worker)
......@@ -184,7 +184,7 @@ let rec init_alt_ergo_worker i =
and process_task () =
let rec find_free_worker_slot i =
if i < num_workers then
match alt_ergo_workers.(i) with
match !alt_ergo_workers.(i) with
Free _ as w -> i, w
| _ -> find_free_worker_slot (i+1)
else -1, Absent
......@@ -193,7 +193,8 @@ and process_task () =
match w with
Free w when not (Queue.is_empty task_queue) ->
let task = Queue.take task_queue in
alt_ergo_workers.(idx) <- Busy (w);
!alt_ergo_workers.(idx) <- Busy (w);
w ## postMessage (marshal (OptionSteps !alt_ergo_steps));
w ## postMessage (marshal task)
| _ -> ()
......@@ -203,10 +204,10 @@ let reset_workers () =
match w with
Busy (w) ->
w ## terminate ();
alt_ergo_workers.(i) <- init_alt_ergo_worker i
| Absent -> alt_ergo_workers.(i) <- init_alt_ergo_worker i
!alt_ergo_workers.(i) <- init_alt_ergo_worker i
| Absent -> !alt_ergo_workers.(i) <- init_alt_ergo_worker i
| Free _ -> ()
) alt_ergo_workers
) !alt_ergo_workers
let push_task task =
Queue.add task task_queue;
......@@ -224,19 +225,16 @@ let init_why3_worker () =
Console.print_why3_output msg;
let () =
match msg with
Tasks (_,_,(id,_,code)) -> push_task (id,code)
Tasks (_,_,(id,_,code)) -> push_task (Task (id,code))
| _ -> ()
in Js._false));
(* seems necessary to warm-up the worker and start loading
the script premptively *)
worker ## postMessage(marshal Init);
worker
let why3_worker = ref (init_why3_worker ())
let why3_parse () =
Console.clear ();
Console.print_msg "Sending buffer to Alt-ergo … ";
Console.print_msg "Sending buffer to Alt-Ergo … ";
log_time "Before marshalling in main thread";
reset_workers ();
first_task := true;
......@@ -261,7 +259,34 @@ let () =
!why3_worker ## terminate ();
why3_worker := init_why3_worker ();
reset_workers ();
Console.set_abort_icon())
Console.set_abort_icon());
let input_threads = get_opt Dom_html.(CoerceTo.input
(getElementById "input-num-threads"))
in
input_threads ## oninput <-
Dom.handler
(fun ev ->
let len = int_of_string (Js.to_string (input_threads ## value)) in
Array.iter (function Busy (w) | Free (w) -> w ## terminate () | _ -> ())
!alt_ergo_workers;
log (string_of_int len);
alt_ergo_workers := Array.make len Absent;
Console.set_abort_icon();
Js._false
);
let input_steps = get_opt Dom_html.(CoerceTo.input
(getElementById "input-num-steps"))
in
input_steps ## oninput <-
Dom.handler
(fun ev ->
let steps = int_of_string (Js.to_string (input_steps ## value)) in
log(string_of_int steps);
alt_ergo_steps := steps;
reset_workers ();
Console.set_abort_icon();
Js._false
)
(* Predefined examples *)
......
......@@ -217,7 +217,6 @@ let () =
let ev = unmarshal ev in
log_time ("After unmarshal ");
match ev with
Init -> ()
| ParseBuffer code ->
why3_run why3_parse_theories Env.base_language code
| ExecuteBuffer code ->
......
type command = ParseBuffer of string
type id = string
type why3_command = ParseBuffer of string
| ExecuteBuffer of string
| Init
type output = Error of string (* msg *)
type why3_output = Error of string (* msg *)
| ErrorLoc of ((int*int*int*int) * string) (* loc * msg *)
| Tasks of ((string * string) (* Theory (id, name) *)
* (string * string) (* Task (id, name *)
* (string * string * string)) (* VC (id, expl, code ) *)
| Tasks of ((id * string) (* Theory (id, name) *)
* (id * string) (* Task (id, name *)
* (id * string * string)) (* VC (id, expl, code ) *)
| Result of string list
type prover_answer = Valid | Unknown of string | Invalid of string
type prover_command = OptionSteps of int | Task of id * string
type prover_output = Valid | Unknown of string | Invalid of string
let marshal a =
Js.string (String.escaped (Marshal.to_string a [Marshal.No_sharing; Marshal.Compat_32]))
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment