https://github.com/EasyCrypt/easycrypt
Revision 98608e4339a7b96cbc0e13c449f6985fc97aaf89 authored by Benjamin Gregoire on 24 March 2021, 03:41:53 UTC, committed by Benjamin Gregoire on 24 March 2021, 03:41:53 UTC
1 parent f5ea5b3
Tip revision: 98608e4339a7b96cbc0e13c449f6985fc97aaf89 authored by Benjamin Gregoire on 24 March 2021, 03:41:53 UTC
fix translation to why3 for operator, where some of its type parameters do not appear in the its type.
fix translation to why3 for operator, where some of its type parameters do not appear in the its type.
Tip revision: 98608e4
myocamlbuild.ml
open Ocamlbuild_plugin
let _ = dispatch begin function
| After_options ->
Options.ocamlc := S[!Options.ocamlc ; A"-rectypes"];
Options.ocamlopt := S[!Options.ocamlopt; A"-rectypes"];
| After_rules ->
(* Numerical warnings *)
begin
let wflag error mode wid =
let mode = match mode with
| `Enable -> "+"
| `Disable -> "-"
| `Mark -> "@"
in
match error with
| false -> S[A"-w"; A(Printf.sprintf "%s%d" mode wid)]
| true -> S[A"-warn-error"; A(Printf.sprintf "%s%d" mode wid)]
in
for i = 1 to 59 do
flag ["ocaml"; "compile"; Printf.sprintf "warn_+%d" i] & (wflag false `Enable i);
flag ["ocaml"; "compile"; Printf.sprintf "warn_-%d" i] & (wflag false `Disable i);
flag ["ocaml"; "compile"; Printf.sprintf "warn_@%d" i] & (wflag false `Mark i);
flag ["ocaml"; "compile"; Printf.sprintf "werr_+%d" i] & (wflag true `Enable i);
flag ["ocaml"; "compile"; Printf.sprintf "werr_-%d" i] & (wflag true `Disable i);
flag ["ocaml"; "compile"; Printf.sprintf "werr_@%d" i] & (wflag true `Mark i)
done
end;
(* menhir & --explain/--trace/--table *)
flag ["ocaml"; "parser"; "menhir"; "menhir_explain"] & A"--explain";
flag ["ocaml"; "parser"; "menhir"; "menhir_trace" ] & A"--trace";
flag ["ocaml"; "parser"; "menhir"; "menhir_table" ] & A"--table";
(* Threads switches *)
flag ["ocaml"; "pkg_threads"; "compile"] (S[A "-thread"]);
flag ["ocaml"; "pkg_threads"; "link"] (S[A "-thread"]);
(* Bisect *)
flag ["ocaml"; "compile" ; "bisect"] & S[A"-package"; A"bisect"];
flag ["ocaml"; "compile" ; "bisect"] & S[A"-syntax" ; A"camlp4o"];
flag ["ocaml"; "compile" ; "bisect"] & S[A"-syntax" ; A"bisect_pp"];
flag ["ocaml"; "ocamldep"; "bisect"] & S[A"-package"; A"bisect"];
flag ["ocaml"; "ocamldep"; "bisect"] & S[A"-syntax" ; A"camlp4o"];
flag ["ocaml"; "ocamldep"; "bisect"] & S[A"-syntax" ; A"bisect_pp"];
flag ["ocaml"; "link" ; "bisect"] & S[A"-package"; A"bisect"];
(* Lint switches *)
flag ["ocaml"; "lint"; "compile"] (S[A "-ppx"; A "../lint/ppx_lint.native"])
| _ -> ()
end
Computing file changes ...