Commit d07a1f53 authored by MARCHE Claude's avatar MARCHE Claude

try why3: attempt to add Alt-ergo parser

Issue: stack overflow when loading the driver, how can it be??
parent 6b90ebf2
......@@ -1426,15 +1426,16 @@ install_local:: bin/why3doc
# trywhy3
#########
ALTERGODIR=src/trywhy3/alt-ergo-0.99.1
ALTERGODIR=src/trywhy3/alt-ergo-1.00-private-2015-01-29
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o -I src/trywhy3 -I $(ALTERGODIR)/src/parsing
ALTERGOMODS=util/numbers util/version util/options parsing/why_parser parsing/why_lexer
ALTERGOMODS=util/numsNumbers util/numbers \
util/version util/myUnix util/config util/options \
parsing/why_parser parsing/why_lexer
TRYWHY3CMO=lib/why3/why3.cma
# $(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
TRYWHY3CMO=lib/why3/why3.cma $(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
trywhy3: src/trywhy3/trywhy3.js src/trywhy3/index.en.html src/trywhy3/index.fr.html
......
......@@ -85,10 +85,7 @@ let run_alt_ergo_on_task t =
let text = flush_str_formatter () in
let lb = Lexing.from_string text in
(* from Alt-Ergo *)
(* does not work yet: it requires zarith
--> investigate how to compile alt-ergo with nums instead
let a = Why_parser.file Why_lexer.token lb in
*)
let _a = Why_parser.file Why_lexer.token lb in
(* TODO ! *)
(*
let ltd, typ_env = Why_typing.file false Why_typing.empty_env a in
......
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