Commit 305c620c authored by MARCHE Claude's avatar MARCHE Claude

Coq tests

parent af13cc38
...@@ -177,22 +177,17 @@ test: bin/why.byte $(TOOLS) ...@@ -177,22 +177,17 @@ test: bin/why.byte $(TOOLS)
--output-file tmp.v --goal Test.G src/test.why --output-file tmp.v --goal Test.G src/test.why
echo bin/why.byte --call --timeout 1 --driver drivers/alt_ergo.drv -I theories/ \ echo bin/why.byte --call --timeout 1 --driver drivers/alt_ergo.drv -I theories/ \
--all-goals theories/real.why --all-goals theories/real.why
mkdir -p theories/coq @mkdir -p theories/coq
bin/why.byte --driver drivers/coq.drv -I theories/ \ @printf "*** Checking Coq file generation ***\\n"
--output-dir theories/coq --goals-of int.Abs @for i in int.Abs int.EuclideanDivision int.ComputerDivision \
bin/why.byte --driver drivers/coq.drv -I theories/ \ real.Abs real.FromInt real.ExpLog real.Trigonometric \
--output-dir theories/coq --goals-of int.EuclideanDivision --goals-of int.ComputerDivision floating_point.Test \
bin/why.byte --driver drivers/coq.drv -I theories/ \ ; do \
--output-dir theories/coq --goals-of real.Abs printf "Generate Coq file for $$i" && bin/why.byte \
bin/why.byte --driver drivers/coq.drv -I theories/ \ --driver drivers/coq.drv -I theories/ \
--output-dir theories/coq --goals-of real.FromInt --output-dir theories/coq --goals-of $$i ; done
bin/why.byte --driver drivers/coq.drv -I theories/ \ @printf "*** Checking Coq compilation ***\\n"
--output-dir theories/coq --goals-of real.ExpLog @for i in theories/coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done
bin/why.byte --driver drivers/coq.drv -I theories/ \
--output-dir theories/coq --goals-of real.Trigonometric
bin/why.byte --driver drivers/coq.drv -I theories/ \
--output-dir theories/coq --goals-of floating_point.Test
for i in theories/coq/*.v; do echo coq $$i; (coqc $$i || true) done
testl: bin/whyl.byte testl: bin/whyl.byte
ocamlrun -bt bin/whyl.byte -I theories/ src/programs/test.mlw ocamlrun -bt bin/whyl.byte -I theories/ src/programs/test.mlw
......
...@@ -68,8 +68,8 @@ let print_ts fmt ts = ...@@ -68,8 +68,8 @@ let print_ts fmt ts =
let print_ls fmt ls = let print_ls fmt ls =
let n = id_unique lprinter ls.ls_name in let n = id_unique lprinter ls.ls_name in
(* if ls.ls_name = "mod" then *) (* temporary workaround *)
eprintf "Coq.print_ls: %s -> %s@." ls.ls_name.id_long n; let n = if n = "mod" then "bmod" else n in
fprintf fmt "%s" n fprintf fmt "%s" n
let print_pr fmt pr = let print_pr fmt pr =
......
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