Commit dea2f404 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

sudoku, some adjustments

parent c17b9b2a
......@@ -20,7 +20,7 @@ ifeq ($(BENCH),yes)
endif
MAIN=main
GEN=map__Map mp__N
GEN=map__Map mach__int__UInt32 mp__N
OBJ=$(GEN) parse
GENML = $(addsuffix .ml, $(GEN))
......@@ -46,7 +46,7 @@ $(MAIN).opt: $(CMX) $(MAIN).cmx
$(MAIN).cmx: $(CMX)
$(GENML): ../mp.mlw
$(WHY3) -E ocaml32 $< -o .
$(WHY3) extract -D ocaml32 $< -o .
%.cmx: %.ml
$(OCAMLOPT) $(INCLUDE) -annot -c $<
......@@ -71,11 +71,11 @@ JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o
$(JSMAIN).js: $(JSMAIN).byte
js_of_ocaml -pretty -noinline $(JSMAIN).byte
js_of_ocaml +nat.js $(JSMAIN).byte
$(JSMAIN).byte: $(CMO) jsmain.ml
$(JSOCAMLC) $(INCLUDE) -o $@ -linkpkg $^
$(JSOCAMLC) $(INCLUDE) -o $@ -linkpkg nums.cma why3extract.cma $^
%.cmo: %.ml
......
......@@ -58,7 +58,7 @@ JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o
$(JSMAIN).js: $(JSMAIN).byte
js_of_ocaml -pretty -noinline +nat.js $(JSMAIN).byte
js_of_ocaml +nat.js $(JSMAIN).byte
$(JSMAIN).byte: $(CMO) $(JSMAIN).cmo
$(JSOCAMLC) $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ -linkpkg $^
......
......@@ -7,14 +7,11 @@
</head>
<body id="body" style="background-color:#e0e0a0">
<h1>Sudoku Solver</h1>
<p>The solver was developed and formally proved correct using
<a href="http://why3.lri.fr/">Why3</a>, extracted to OCaml and then compiled to JavaScript
<p>This solver was developed and formally proved correct using
<a href="http://why3.lri.fr/">Why3</a>, extracted to OCaml and
then compiled to JavaScript
using <a href="http://ocsigen.org/js_of_ocaml/">Js_of_ocaml</a></p>
<p>See also
<ul><li> A <a href="http://www-sop.inria.fr/marelle/Laurent.Thery/Sudoku/Sudoku.html">Sudoku Solver formally proved using Coq</a>
</ul>
</p>
<div id="board"></div>
<p>
<button id="solve">Solve</button>
......@@ -26,5 +23,11 @@
<button id="sample3">Example 3 (hard)</button>
</p>
<script type="text/javascript" src="jsmain.js"></script>
<p>See also
<ul>
<li> The <a href="http://toccata.lri.fr/gallery/sudoku.en.html">Why3 source of this solver</a>
<li> A <a href="http://www-sop.inria.fr/marelle/Laurent.Thery/Sudoku/Sudoku.html">Sudoku Solver formally proved using Coq</a>
</ul>
</p>
</body>
</html>
Supports Markdown
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