Merge pull request #5510 from kit-ty-kate/solver-tolerance

Add the OPAMSOLVERTOLERANCE environment variable to allow users to fix solver timeouts for good

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
 ```

master_changes.md

@@ -81,6 +81,7 @@ users)
 ## Clean
 
 ## Env
+  * Add the `OPAMSOLVERTOLERANCE` environment variable to allow users to fix solver timeouts for good [#5510 @kit-ty-kate - fix #3230]
 
 ## Opamfile
 

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 \

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 ->

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;

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
 

src/solver/opamBuiltinMccs.real.ml

@@ -31,15 +31,16 @@ 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
   in
   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

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"

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;

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)

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 =

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

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

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 ->