From 470d68b17bdf046a4acd3809f372a9e25829753c Mon Sep 17 00:00:00 2001 From: Kate Date: Fri, 14 Apr 2023 18:54:53 +0100 Subject: [PATCH] Add the OPAMSOLVERTOLERANCE environment variable to allow users to fix solver timeouts for good --- doc/pages/Tricks.md | 1 + src/client/opamArg.ml | 10 ++++++++++ src/client/opamClientConfig.mli | 1 + src/solver/opamBuiltin0install.ml | 2 +- src/solver/opamBuiltinMccs.dummy.ml | 2 +- src/solver/opamBuiltinMccs.real.ml | 5 +++-- src/solver/opamBuiltinZ3.dummy.ml | 2 +- src/solver/opamBuiltinZ3.real.ml | 3 ++- src/solver/opamCudf.ml | 7 +++++-- src/solver/opamCudfSolver.ml | 2 +- src/solver/opamCudfSolverSig.ml | 2 +- src/solver/opamSolverConfig.ml | 13 ++++++++++++- src/solver/opamSolverConfig.mli | 3 +++ 13 files changed, 42 insertions(+), 11 deletions(-) diff --git a/doc/pages/Tricks.md b/doc/pages/Tricks.md index 9610babc6e8..54f4d19d6a0 100644 --- a/doc/pages/Tricks.md +++ b/doc/pages/Tricks.md @@ -150,6 +150,7 @@ The following sequence of commands tries to install as much packages as possible opam update opam switch create . ocaml-base-compiler.$(VERSION) export OPAMSOLVERTIMEOUT=3600 +export OPAMSOLVERTOLERANCE=1.0 opam list --available -s | xargs opam install --best-effort --yes # Be patient ``` diff --git a/src/client/opamArg.ml b/src/client/opamArg.ml index 14c25057846..9289fdea990 100644 --- a/src/client/opamArg.ml +++ b/src/client/opamArg.ml @@ -186,6 +186,16 @@ let environment_variables = "change the time allowance of the solver. Default is %.1f, set to 0 \ for unlimited. Note that all solvers may not support this option." (OpamStd.Option.default 0. OpamSolverConfig.(default.solver_timeout))); + "SOLVERTOLERANCE", cli_from cli2_4, (fun v -> SOLVERTOLERANCE (env_float v)), + (Printf.sprintf + "changes the tolerance towards the solver choosing an unoptimized \ + solution (i.e. might pull outdated packages). Typical values range \ + from 0.0 (best solution known to the solver) to 1.0 (unoptimized \ + solution). Default is %.1f. This option is useful in case the solver \ + can't find a solution in a reasonable time \ + (see $(b,\\$OPAMSOLVERTIMEOUT)). Note that all solvers may not \ + support this option." + (OpamStd.Option.default 0. OpamSolverConfig.default.solver_tolerance)); "UPGRADECRITERIA", cli_original, (fun v -> UPGRADECRITERIA (env_string v)), "specifies user $(i,preferences) for dependency solving when performing \ diff --git a/src/client/opamClientConfig.mli b/src/client/opamClientConfig.mli index 6adeeafb1d0..7d3db41ba22 100644 --- a/src/client/opamClientConfig.mli +++ b/src/client/opamClientConfig.mli @@ -146,6 +146,7 @@ val opam_init: ?solver_preferences_fixup:string option Lazy.t -> ?solver_preferences_best_effort_prefix: string option Lazy.t -> ?solver_timeout:float option -> + ?solver_tolerance:float option -> ?solver_allow_suboptimal:bool -> ?cudf_trim:string option -> ?dig_depth:int -> diff --git a/src/solver/opamBuiltin0install.ml b/src/solver/opamBuiltin0install.ml index 3c672a760a0..09c247d9f66 100644 --- a/src/solver/opamBuiltin0install.ml +++ b/src/solver/opamBuiltin0install.ml @@ -123,7 +123,7 @@ let parse_criteria criteria = in parse default (OpamCudfCriteria.of_string criteria) -let call ~criteria ?timeout:_ (preamble, universe, request) = +let call ~criteria ?timeout:_ ?tolerance:_ (preamble, universe, request) = let { drop_installed_packages; prefer_oldest; diff --git a/src/solver/opamBuiltinMccs.dummy.ml b/src/solver/opamBuiltinMccs.dummy.ml index af005c9fb51..5b498336b24 100644 --- a/src/solver/opamBuiltinMccs.dummy.ml +++ b/src/solver/opamBuiltinMccs.dummy.ml @@ -28,7 +28,7 @@ module S = struct crit_best_effort_prefix = None; } - let call ~criteria:_ ?timeout:_ _cudf = + let call ~criteria:_ ?timeout:_ ?tolerance:_ _cudf = failwith "This opam was compiled without a solver built in" end diff --git a/src/solver/opamBuiltinMccs.real.ml b/src/solver/opamBuiltinMccs.real.ml index c3e90619167..2eea665135d 100644 --- a/src/solver/opamBuiltinMccs.real.ml +++ b/src/solver/opamBuiltinMccs.real.ml @@ -31,7 +31,7 @@ let default_criteria = { crit_best_effort_prefix = Some "+count[opam-query:,false],"; } -let call solver_backend ext ~criteria ?timeout cudf = +let call solver_backend ext ~criteria ?timeout ?tolerance cudf = let solver = match solver_backend, ext with | `LP _, Some ext -> `LP ext | _ -> solver_backend @@ -39,7 +39,8 @@ let call solver_backend ext ~criteria ?timeout cudf = match Mccs.resolve_cudf ~solver - ~verbose:OpamCoreConfig.(abs !r.debug_level >= 2) + ?mip_gap:tolerance + ~verbosity:(!OpamCoreConfig.r.debug_level - 1) (* *) ?timeout criteria cudf with | None -> raise Dose_common.CudfSolver.Unsat diff --git a/src/solver/opamBuiltinZ3.dummy.ml b/src/solver/opamBuiltinZ3.dummy.ml index 954087e2400..9859a8bfd33 100644 --- a/src/solver/opamBuiltinZ3.dummy.ml +++ b/src/solver/opamBuiltinZ3.dummy.ml @@ -27,5 +27,5 @@ let default_criteria = { crit_best_effort_prefix = None; } -let call ~criteria:_ ?timeout:_ _cudf = +let call ~criteria:_ ?timeout:_ ?tolerance:_ _cudf = failwith "This opam was compiled without the Z3 solver built in" diff --git a/src/solver/opamBuiltinZ3.real.ml b/src/solver/opamBuiltinZ3.real.ml index 3ffa167d6d1..08ece2707fa 100644 --- a/src/solver/opamBuiltinZ3.real.ml +++ b/src/solver/opamBuiltinZ3.real.ml @@ -382,13 +382,14 @@ let extract_solution_packages universe opt = [] | None -> failwith "no model ??" -let call ~criteria ?timeout (preamble, universe, _ as cudf) = +let call ~criteria ?timeout ?tolerance:_ (preamble, universe, _ as cudf) = (* try *) log "Generating problem..."; let cfg = match timeout with | None -> [] | Some secs -> ["timeout", string_of_int (int_of_float (1000. *. secs))] in + (* TODO: use tolerance. Maybe the rlimit cfg option + intermediate solution could be used *) let ctx = { z3 = Z3.mk_context cfg; pkgs = Hashtbl.create 2731; diff --git a/src/solver/opamCudf.ml b/src/solver/opamCudf.ml index eff960ec9c1..51814abce7b 100644 --- a/src/solver/opamCudf.ml +++ b/src/solver/opamCudf.ml @@ -1595,9 +1595,12 @@ let call_external_solver ~version_map univ req = let msg = Printf.sprintf "Sorry, resolution of the request timed out.\n\ - Try to specify a more precise request, use a different solver, or \ - increase the allowed time by setting OPAMSOLVERTIMEOUT to a bigger \ + Try to specify a more precise request, use a different solver, \ + increase the tolerance for unoptimized solutions by setting \ + OPAMSOLVERTOLERANCE to a bigger value (currently, it is set to %.1f) \ + or increase the allowed time by setting OPAMSOLVERTIMEOUT to a bigger \ value (currently, it is set to %.1f seconds)." + OpamSolverConfig.(OpamStd.Option.default 0. !r.solver_tolerance) OpamSolverConfig.(OpamStd.Option.default 0. !r.solver_timeout) in raise (Solver_failure msg) diff --git a/src/solver/opamCudfSolver.ml b/src/solver/opamCudfSolver.ml index c60a0d012fe..78afff14cac 100644 --- a/src/solver/opamCudfSolver.ml +++ b/src/solver/opamCudfSolver.ml @@ -27,7 +27,7 @@ module type ExternalArg = sig val default_criteria: criteria_def end -let call_external_solver command ~criteria ?timeout (_, universe,_ as cudf) = +let call_external_solver command ~criteria ?timeout ?tolerance:_ (_, universe,_ as cudf) = let solver_in = OpamFilename.of_string (OpamSystem.temp_file "solver-in") in let solver_out = diff --git a/src/solver/opamCudfSolverSig.ml b/src/solver/opamCudfSolverSig.ml index 66a1a7f801e..877ab8d3e68 100644 --- a/src/solver/opamCudfSolverSig.ml +++ b/src/solver/opamCudfSolverSig.ml @@ -38,7 +38,7 @@ module type S = sig it's only run if the solver returns unsat, to extract the explanations. *) val call: - criteria:string -> ?timeout:float -> Cudf.cudf -> + criteria:string -> ?timeout:float -> ?tolerance:float -> Cudf.cudf -> Cudf.preamble option * Cudf.universe end diff --git a/src/solver/opamSolverConfig.ml b/src/solver/opamSolverConfig.ml index 1df6755e121..1d9b06cba82 100644 --- a/src/solver/opamSolverConfig.ml +++ b/src/solver/opamSolverConfig.ml @@ -23,6 +23,7 @@ module E = struct | PREPRO of bool option | SOLVERALLOWSUBOPTIMAL of bool option | SOLVERTIMEOUT of float option + | SOLVERTOLERANCE of float option | UPGRADECRITERIA of string option | USEINTERNALSOLVER of bool option | VERSIONLAGPOWER of int option @@ -42,6 +43,7 @@ module E = struct let solverallowsuboptimal = value (function SOLVERALLOWSUBOPTIMAL b -> b | _ -> None) let solvertimeout = value (function SOLVERTIMEOUT f -> f | _ -> None) + let solvertolerance = value (function SOLVERTOLERANCE f -> f | _ -> None) let useinternalsolver = value (function USEINTERNALSOLVER b -> b | _ -> None) let upgradecriteria = value (function UPGRADECRITERIA s -> s | _ -> None) let versionlagpower = value (function VERSIONLAGPOWER i -> i | _ -> None) @@ -59,6 +61,7 @@ type t = { solver_preferences_fixup: string option Lazy.t; solver_preferences_best_effort_prefix: string option Lazy.t; solver_timeout: float option; + solver_tolerance: float option; solver_allow_suboptimal: bool; cudf_trim: string option; dig_depth: int; @@ -75,6 +78,7 @@ type 'a options_fun = ?solver_preferences_fixup:string option Lazy.t -> ?solver_preferences_best_effort_prefix:string option Lazy.t -> ?solver_timeout:float option -> + ?solver_tolerance:float option -> ?solver_allow_suboptimal:bool -> ?cudf_trim:string option -> ?dig_depth:int -> @@ -95,6 +99,7 @@ let default = solver_preferences_fixup = lazy None; solver_preferences_best_effort_prefix = lazy None; solver_timeout = Some 60.; + solver_tolerance = Some 0.0; solver_allow_suboptimal = true; cudf_trim = None; dig_depth = 2; @@ -111,6 +116,7 @@ let setk k t ?solver_preferences_fixup ?solver_preferences_best_effort_prefix ?solver_timeout + ?solver_tolerance ?solver_allow_suboptimal ?cudf_trim ?dig_depth @@ -133,6 +139,8 @@ let setk k t solver_preferences_best_effort_prefix; solver_timeout = t.solver_timeout + solver_timeout; + solver_tolerance = + t.solver_tolerance + solver_tolerance; solver_allow_suboptimal = t.solver_allow_suboptimal + solver_allow_suboptimal; cudf_trim = t.cudf_trim + cudf_trim; @@ -193,6 +201,8 @@ let initk k = E.besteffortprefixcriteria () >>| fun c -> (lazy (Some c)) in let solver_timeout = E.solvertimeout () >>| fun f -> if f <= 0. then None else Some f in + let solver_tolerance = + E.solvertolerance () >>| fun f -> if f <= 0. then None else Some f in setk (setk (fun c -> r := with_auto_criteria c; k)) !r ~cudf_file:(E.cudffile ()) ~solver @@ -202,6 +212,7 @@ let initk k = ?solver_preferences_fixup:fixup_criteria ?solver_preferences_best_effort_prefix:best_effort_prefix_criteria ?solver_timeout + ?solver_tolerance ?solver_allow_suboptimal:(E.solverallowsuboptimal ()) ~cudf_trim:(E.cudftrim ()) ?dig_depth:(E.digdepth ()) @@ -253,6 +264,6 @@ let call_solver ~criteria cudf = OpamConsole.log "SOLVER" "Calling solver %s with criteria %s" (OpamCudfSolver.get_name (module S)) criteria; let chrono = OpamConsole.timer () in - let r = S.call ~criteria ?timeout:(!r.solver_timeout) cudf in + let r = S.call ~criteria ?timeout:(!r.solver_timeout) ?tolerance:(!r.solver_tolerance) cudf in OpamConsole.log "SOLVER" "External solver took %.3fs" (chrono ()); r diff --git a/src/solver/opamSolverConfig.mli b/src/solver/opamSolverConfig.mli index 46e1da21fd8..2a9b0c2d174 100644 --- a/src/solver/opamSolverConfig.mli +++ b/src/solver/opamSolverConfig.mli @@ -25,6 +25,7 @@ module E : sig | PREPRO of bool option | SOLVERALLOWSUBOPTIMAL of bool option | SOLVERTIMEOUT of float option + | SOLVERTOLERANCE of float option | UPGRADECRITERIA of string option | USEINTERNALSOLVER of bool option | VERSIONLAGPOWER of int option @@ -40,6 +41,7 @@ type t = private { solver_preferences_fixup: string option Lazy.t; solver_preferences_best_effort_prefix: string option Lazy.t; solver_timeout: float option; + solver_tolerance: float option; solver_allow_suboptimal: bool; cudf_trim: string option; dig_depth: int; @@ -56,6 +58,7 @@ type 'a options_fun = ?solver_preferences_fixup:string option Lazy.t -> ?solver_preferences_best_effort_prefix:string option Lazy.t -> ?solver_timeout:float option -> + ?solver_tolerance:float option -> ?solver_allow_suboptimal:bool -> ?cudf_trim:string option -> ?dig_depth:int ->