Commit d6328f8f authored by Kim Nguyễn's avatar Kim Nguyễn

[trywhy3]: prepare for merge.

	   * clean-up the code and files
	   * add license headers in .ml files
	   * add a Makefile rule to generate a tarball
	   * update the README
parent 96886731
......@@ -1505,7 +1505,18 @@ ALTERGOMODS=util/numsNumbers util/numbers \
sat/sat_solvers \
main/frontend
ALTERGOCMO=$(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
TRYWHY3CMO=lib/why3/why3.cma
TRYWHY3CMO=lib/why3/why3.cma
TRYWHY3FILES=trywhy3.js why3_worker.js alt_ergo_worker.js trywhy3.html trywhy3.css \
README examples/ \
trywhy3_custom.css gen_index.sh fontawesome/css/font-awesome.min.css \
fontawesome/fonts/FontAwesome.otf fontawesome/fonts/fontawesome-webfont.svg \
fontawesome/fonts/fontawesome-webfont.woff fontawesome/fonts/fontawesome-webfont.eot \
fontawesome/fonts/fontawesome-webfont.ttf fontawesome/fonts/fontawesome-webfont.woff2 \
ace-builds/src-min-noconflict/ace.js ace-builds/src-min-noconflict/mode-why3.js \
ace-builds/src-min-noconflict/theme-chrome.js
trywhy3_package: trywhy3
tar czf trywhy3.tar.gz -C src $(addprefix trywhy3/, $(TRYWHY3FILES))
trywhy3: src/trywhy3/trywhy3.js src/trywhy3/why3_worker.js src/trywhy3/alt_ergo_worker.js
......@@ -1546,7 +1557,7 @@ clean::
rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte src/trywhy3/trywhy3.cm* \
src/trywhy3/why3_worker.js src/trywhy3/why3_worker.byte src/trywhy3/why3_worker.cm* \
src/trywhy3/alt_ergo_worker.js src/trywhy3/alt_ergo_worker.byte src/trywhy3/alt_ergo_worker.cm* \
src/trywhy3/worker_proto.cm*
src/trywhy3/worker_proto.cm* trywhy3.tar.gz
CLEANDIRS += src/trywhy3
......
......@@ -15,7 +15,7 @@ Instructions to build TryWhy3
mkdir fontawesome
copy in that directory the directory fonts and css of the Font-Awesome distribution.
** install Alt-Ergo
......@@ -46,4 +46,28 @@ Instructions to build TryWhy3
make trywhy3
* install : TODO
* install
you can build a package with
make trywhy3_package
this creates a tarball containing a directory trywhy3/ which you can put on a webserver.
* customization
** To change the theme used by the ace editor widget, add the
relevant theme-*.js file to the ace-builds/src-min-noconflict/
directory and update the variable definition at the top of the
trywhy3.html file
** To change the look and feel of the rest of the application, edit
the file trywhy3_custom.css.
** To add some predefined examples, put some .mlw or .why files in the
examples/ subdirectory and generate an index as follows (assuming you
are in your trywhy3 directory) :
cp some_file.mlw examples/
cd examples/
../gen_index.sh *.mlw > index.txt
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open Format
open Worker_proto
......
......@@ -143,10 +143,11 @@
<p>© 2010-2016, INRIA - CNRS - Paris-Sud University<br/>
This software is distributed under the terms of the GNU Lesser
General Public License version 2.1, with the special exception
on linking described in file LICENSE.
on linking described in the
file <a href="https://scm.gforge.inria.fr/anonscm/gitweb?p=why3/why3.git;a=blob_plain;f=LICENSE">LICENSE</a>.
</p>
<p>TryWhy3 relies on the following excellent open source
software and resources :
softwares and resources :
</p>
<ul>
<li>A Javascript version of
......
......@@ -556,7 +556,7 @@ module Dialogs =
let radio_wide = getElement AsHtml.input "why3-radio-wide"
let radio_column = getElement AsHtml.input "why3-radio-column"
let all_dialogs = [ setting_dialog ]
let all_dialogs = [ setting_dialog; about_dialog ]
let show diag () =
log ("HERE");
dialog_panel ## style ## display <- Js.string "flex";
......@@ -753,42 +753,6 @@ let () =
Dialogs.(set_onchange radio_wide (fun _ -> Panel.set_wide true));
Dialogs.(set_onchange radio_column (fun _ -> Panel.set_wide false))
(* add_button "button-prove" (why3_transform `Prove (fun _ -> ()));
add_button "button-split" (why3_transform `Split (fun _ -> ()));
add_button "button-clean" (why3_transform `Clean TaskList.clean_task);
*)
(*
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;
TaskList.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 ();
TaskList.set_abort_icon();
Js._false
)
*)
let () =
let xhr = XHR.create () in
xhr ## onreadystatechange <-
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
type id = string
type loc = int * int * int * int
type why3_loc = string * (int * int * int) (* kind, line, column, length *)
......
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