Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for comparing results with a specific status #75

Merged
merged 2 commits into from
Apr 3, 2024
Merged

Add support for comparing results with a specific status #75

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f7fb210
Add support for comparing results with a specific status
bclement-ocp Apr 3, 2024
c8ff073
Review comments
bclement-ocp Apr 3, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
43 changes: 29 additions & 14 deletions src/core/Test_compare.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ open Common

type filename = string
type prover = filename * Prover.name
type status = [ `Sat | `Unsat ]

let pb_v_record = Test.pb_v_record
let pb_int_color = Test.pb_int_color
Expand Down Expand Up @@ -35,6 +36,16 @@ let cmp2sql = function

let pp_cmp = Fmt.of_to_string cmp2sql

let status_to_string = function
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

status_to_sql maybe?

| `Sat -> {|
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why the newlines? :)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To be honest, because I copied from cmp2sql above (:

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ha! 😂 foisted on my own petard

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually now that I think about it I believe I am also the one who wrote cmp2sql 😬

(r1.res = 'sat' or r2.res = 'sat')
|}
| `Unsat -> {|
(r1.res = 'unsat' or r2.res = 'unsat')
|}

let pp_status = Fmt.of_to_string status_to_string

let pp_opt ?(none = Fmt.const_string "") pp ppf = function
| None -> none ppf ()
| Some v -> pp ppf v
Expand All @@ -43,12 +54,13 @@ let pp_prefix prefix pp ppf v =
Fmt.fprintf ppf "%s" prefix;
pp ppf v

let unsafe_sql ?order ?limit ?offset ?filter select =
let unsafe_sql ?order ?limit ?offset ?filter ?status select =
let pp_filter ppf filter =
match filter with
| None -> ()
| Some filter -> Format.fprintf ppf "and (%a)" pp_cmp filter
in
let pp_status = pp_opt (pp_prefix " and " pp_status) in
let pp_select =
Fmt.list
~sep:(fun ppf () -> Fmt.fprintf ppf ",@,")
Expand All @@ -58,9 +70,9 @@ let unsafe_sql ?order ?limit ?offset ?filter select =
{| select %a
from db1.prover_res r1
inner join db2.prover_res r2 on r2.file = r1.file
where r1.prover = ? and r2.prover = ? %a %a %a %a
where r1.prover = ? and r2.prover = ? %a %a %a %a %a
|}
pp_select select pp_filter filter
pp_select select pp_filter filter pp_status status
(pp_opt (pp_prefix " order by " Fmt.string))
order
(pp_opt (pp_prefix " limit " Fmt.int))
Expand Down Expand Up @@ -90,7 +102,7 @@ module Short = struct
"regressed", pb_int_color Style.(fg_color Cyan) self.regressed;
]

let make1 db p1 p2 : t =
let make1 ?status db p1 p2 : t =
(* Note: first ? is p1, second ? is p2 *)
let get_n q =
Db.exec db q p1 p2
Expand All @@ -115,20 +127,22 @@ module Short = struct
and not exists (select file from db2.prover_res where
db2.prover_res.prover=?
and file = r1.file); |}
and same = get_n (unsafe_sql ~filter:`Same [ "count(r1.file)" ])
and mismatch = get_n (unsafe_sql ~filter:`Mismatch [ "count(r1.file)" ])
and improved = get_n (unsafe_sql ~filter:`Improved [ "count(r1.file)" ])
and same = get_n (unsafe_sql ?status ~filter:`Same [ "count(r1.file)" ])
and mismatch =
get_n (unsafe_sql ?status ~filter:`Mismatch [ "count(r1.file)" ])
and improved =
get_n (unsafe_sql ?status ~filter:`Improved [ "count(r1.file)" ])
and regressed =
get_n (unsafe_sql ~filter:`Regressed [ "count(r1.file)" ])
get_n (unsafe_sql ?status ~filter:`Regressed [ "count(r1.file)" ])
in
{ appeared; disappeared; same; mismatch; improved; regressed }

let make_provers (f1, p1) (f2, p2) : t =
let make_provers ?status (f1, p1) (f2, p2) : t =
Error.guard
(Error.wrapf "short comparison of '%s/%s' and '%s/%s'" f1 p1 f2 p2)
@@ fun () -> make1 (make_db f1 f2) p1 p2
@@ fun () -> make1 ?status (make_db f1 f2) p1 p2

let make f1 f2 : (_ * t) list =
let make ?status f1 f2 : (_ * t) list =
Error.guard (Error.wrapf "short comparison of '%s' and '%s'" f1 f2)
@@ fun () ->
let db = Sqlite3.db_open ":memory:" in
Expand All @@ -145,19 +159,20 @@ module Short = struct
|> Misc.unwrap_db (fun () -> "listing all provers")
in
Logs.debug (fun k -> k "provers: [%s]" (String.concat ";" provers));
CCList.map (fun prover -> prover, make1 db prover prover) provers
CCList.map (fun prover -> prover, make1 ?status db prover prover) provers
end

module Full = struct
type filter = [ `Improved | `Regressed | `Mismatch | `Same ]
type entry = string * Res.t * float * Res.t * float

let make_filtered ?(page = 0) ?(page_size = 500) ?filter (f1, p1) (f2, p2) =
let make_filtered ?(page = 0) ?(page_size = 500) ?filter ?status (f1, p1)
(f2, p2) =
let tags = [] (* TODO? *) in
let offset = page * page_size in
let limit = page_size + 1 in
Db.exec (make_db f1 f2)
(unsafe_sql ~order:"r1.file desc" ~limit ~offset ?filter
(unsafe_sql ~order:"r1.file desc" ~limit ~offset ?filter ?status
[ "r1.file"; "r1.res"; "r2.res"; "r1.rtime"; "r2.rtime" ])
p1 p2
~ty:
Expand Down
6 changes: 4 additions & 2 deletions src/core/Test_compare.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

type filename = string
type prover = filename * Prover.name
type status = [ `Sat | `Unsat ]

module Short : sig
type t = {
Expand All @@ -14,9 +15,9 @@ module Short : sig
}

val to_printbox : t -> PrintBox.t
val make : filename -> filename -> (Prover.name * t) list
val make : ?status:status -> filename -> filename -> (Prover.name * t) list

val make_provers : prover -> prover -> t
val make_provers : ?status:status -> prover -> prover -> t
(** Make a single comparison between two provers in (possibly) different files *)
end

Expand All @@ -28,6 +29,7 @@ module Full : sig
?page:int ->
?page_size:int ->
?filter:filter ->
?status:status ->
prover ->
prover ->
entry list
Expand Down
70 changes: 63 additions & 7 deletions src/server/benchpress_server.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1154,6 +1154,14 @@ let handle_compare2 self : unit =
None)
@@ H.Request.query req
in
let status =
match
String.lowercase_ascii @@ List.assoc "status" (H.Request.query req)
with
| "sat" -> Some `Sat
| "unsat" -> Some `Unsat
| _ | (exception Not_found) -> None
in
(* H.Request.query reverses the query order, so we have to reverse it again *)
let provers = List.rev provers in
let prover1, prover2 =
Expand Down Expand Up @@ -1183,6 +1191,30 @@ let handle_compare2 self : unit =
in
let options1 = CCList.mapi (mk_entry ?selected:prover1) entries in
let options2 = CCList.mapi (mk_entry ?selected:prover2) entries in
let status_opt_to_string = function
| Some `Sat -> "sat"
| Some `Unsat -> "unsat"
| None -> ""
in
let status_option ?current status =
let open Html in
let attrs =
A.value (status_opt_to_string status)
::
(if current = Some status then
[ A.selected "selected" ]
else
[])
in
option attrs [ txt (status_opt_to_string status) ]
in
let ostatus =
[
status_option None;
status_option ~current:status (Some `Unsat);
status_option ~current:status (Some `Sat);
]
in
let prover_info =
let file_link fname text =
PrintBox.link ~uri:(uri_get_file fname) (PrintBox.text text)
Expand All @@ -1203,7 +1235,7 @@ let handle_compare2 self : unit =
| `Mismatch -> "Mismatch"
| `Same -> "Same"
in
let short = Test_compare.Short.make_provers (ff1, p1) (ff2, p2) in
let short = Test_compare.Short.make_provers ?status (ff1, p1) (ff2, p2) in
let make filter =
let total = get short filter in
let page_size = min total 500 in
Expand All @@ -1220,8 +1252,8 @@ let handle_compare2 self : unit =
[
summary []
[ txtf "%s (%s)" (filter_to_string filter) limit_info ];
Test_compare.Full.make_filtered ~page_size ~filter (ff1, p1)
(ff2, p2)
Test_compare.Full.make_filtered ?status ~page_size ~filter
(ff1, p1) (ff2, p2)
|> Test_compare.Full.to_printbox ~file_link
|> Html.pb_html;
]);
Expand All @@ -1242,17 +1274,41 @@ let handle_compare2 self : unit =
|> String.concat "," |> gnuplot_img;
]
in
let plot_html =
if Option.is_none status then
plot_html
else
Html.(
strong []
[ txt "Warning: this plot includes BOTH sat and unsat results." ])
:: plot_html
in
let html =
let open Html in
mk_page ~title:"compare2"
([
mk_navigation [ "/compare2/", "compare", true ];
h3 [] [ txt "compare" ];
form []
form
[ A.class_ "container" ]
[
select [ A.name "prover[]" ] options1;
select [ A.name "prover[]" ] options2;
mk_button ~cls:"btn-primary btn-sm" [] [ txt "Compare" ];
div
[ A.class_ "row" ]
[
div
[ A.class_ "col-6" ]
[
select [ A.name "prover[]" ] options1;
select [ A.name "prover[]" ] options2;
mk_button ~cls:"btn-primary btn-sm" [] [ txt "Compare" ];
];
div
[ A.class_ "col-3" ]
[
Html.label [] [ Html.txt "Limit to:" ];
select [ A.name "status" ] ostatus;
];
];
];
]
@ prover_info
Expand Down
Loading