simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 19:25:36 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

pick proof format with env variable

Browse source
This commit is contained in:
Simon Cruanes 2021-06-11 10:25:40 -04:00
parent 2eee760e29
commit 6a9dbb8440
1 changed files with 13 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/base-term/Proof.ml
View file

@ -464,13 +464,21 @@ module Quip = struct
output_char out ')' output_char out ')'
end end
type out_format = Sexp | CSexp
let default_out_format = Sexp
let out_format_ = match Sys.getenv_opt "PROOF_FMT" with
| Some "csexp" -> CSexp
| Some "sexp" -> Sexp
| Some s -> failwith (Printf.sprintf "unknown proof format %S" s)
| None -> default_out_format
let output oc (self:t) : unit = let output oc (self:t) : unit =
(* canonical sexp *) match out_format_ with
if true then ( | Sexp -> let module M = Make(Out_sexp) in M.pp self oc
let module M = Make(Out_sexp) in M.pp self oc | CSexp ->
) else ( (* canonical sexp *)
let module M = Make(Out_csexp) in M.pp self oc let module M = Make(Out_csexp) in M.pp self oc
)
end end
let pp_debug ~sharing out p = let pp_debug ~sharing out p =