···
1
+
(* Implementation of the PubGrub algorithm in OCaml *)
4
+
module type PACKAGE_ID = sig
6
+
val compare : t -> t -> int
7
+
val to_string : t -> string
10
+
module type VERSION = sig
12
+
val compare : t -> t -> int
13
+
val to_string : t -> string
16
+
module type VERSION_SET = sig
21
+
val singleton : version -> t
22
+
val union : t -> t -> t
23
+
val intersection : t -> t -> t
24
+
val complement : t -> t
25
+
val is_empty : t -> bool
26
+
val contains : version -> t -> bool
27
+
val subset_of : t -> t -> bool
28
+
val is_disjoint : t -> t -> bool
29
+
val to_string : t -> string
32
+
(* Terms and Constraints *)
33
+
type ('v, 'vs) term =
34
+
| Positive of 'vs (* The package version must be in this set *)
35
+
| Negative of 'vs (* The package version must not be in this set *)
37
+
module Term = struct
38
+
type ('v, 'vs) t = ('v, 'vs) term
40
+
let any (vs : 'vs) : ('v, 'vs) t = Positive vs
41
+
let empty (vs : 'vs) : ('v, 'vs) t = Negative vs
42
+
let exact (v : 'v) (mk_singleton : 'v -> 'vs) : ('v, 'vs) t =
43
+
Positive (mk_singleton v)
45
+
let negate = function
46
+
| Positive vs -> Negative vs
47
+
| Negative vs -> Positive vs
49
+
let contains (v : 'v) (vs_contains : 'v -> 'vs -> bool) term =
51
+
| Positive vs -> vs_contains v vs
52
+
| Negative vs -> not (vs_contains v vs)
54
+
let intersect_positive_positive vs_intersect vs1 vs2 =
55
+
Positive (vs_intersect vs1 vs2)
57
+
let intersect_negative_negative vs_intersect vs_complement vs1 vs2 =
58
+
Negative (vs_intersect (vs_complement vs1) (vs_complement vs2))
60
+
let intersect_positive_negative vs_intersect vs_complement vs1 vs2 =
61
+
let intersection = vs_intersect vs1 (vs_complement vs2) in
62
+
Positive intersection
64
+
let intersect_negative_positive vs_intersect vs_complement vs1 vs2 =
65
+
let intersection = vs_intersect (vs_complement vs1) vs2 in
66
+
Positive intersection
68
+
let intersection vs_intersect vs_complement t1 t2 =
70
+
| Positive vs1, Positive vs2 ->
71
+
intersect_positive_positive vs_intersect vs1 vs2
72
+
| Negative vs1, Negative vs2 ->
73
+
intersect_negative_negative vs_intersect vs_complement vs1 vs2
74
+
| Positive vs1, Negative vs2 ->
75
+
intersect_positive_negative vs_intersect vs_complement vs1 vs2
76
+
| Negative vs1, Positive vs2 ->
77
+
intersect_negative_positive vs_intersect vs_complement vs1 vs2
79
+
let union_positive_positive vs_union vs1 vs2 =
80
+
Positive (vs_union vs1 vs2)
82
+
let union_negative_negative vs_intersect vs1 vs2 =
83
+
Negative (vs_intersect vs1 vs2)
85
+
let union_positive_negative vs_intersect vs_complement vs_is_empty vs1 vs2 =
86
+
let diff = vs_intersect vs1 (vs_complement vs2) in
87
+
if vs_is_empty diff then Negative vs2 else Positive diff
89
+
let union_negative_positive vs_intersect vs_complement vs_is_empty vs1 vs2 =
90
+
let diff = vs_intersect (vs_complement vs1) vs2 in
91
+
if vs_is_empty diff then Negative vs1 else Positive diff
93
+
let union vs_union vs_intersect vs_complement vs_is_empty t1 t2 =
95
+
| Positive vs1, Positive vs2 ->
96
+
union_positive_positive vs_union vs1 vs2
97
+
| Negative vs1, Negative vs2 ->
98
+
union_negative_negative vs_intersect vs1 vs2
99
+
| Positive vs1, Negative vs2 ->
100
+
union_positive_negative vs_intersect vs_complement vs_is_empty vs1 vs2
101
+
| Negative vs1, Positive vs2 ->
102
+
union_negative_positive vs_intersect vs_complement vs_is_empty vs1 vs2
104
+
let is_positive = function
105
+
| Positive _ -> true
106
+
| Negative _ -> false
108
+
let to_string (_ : 'v -> string) (vs_to_str : 'vs -> string) term =
110
+
| Positive vs -> vs_to_str vs
111
+
| Negative vs -> "not " ^ vs_to_str vs
114
+
(* Incompatibilities *)
115
+
type ('p, 'v, 'vs, 'meta) incompatibility = {
116
+
terms : (('p * ('v, 'vs) term) list);
117
+
cause : ('p, 'v, 'vs, 'meta) incompatibility_cause;
119
+
and ('p, 'v, 'vs, 'meta) incompatibility_cause =
121
+
| NoVersions of 'p * 'vs
122
+
| Dependency of 'p * 'vs * 'p * 'vs
123
+
| Derived of int * int
124
+
| External of 'p * 'vs * 'meta
126
+
module Incompatibility = struct
127
+
type ('p, 'v, 'vs, 'meta) t = ('p, 'v, 'vs, 'meta) incompatibility
129
+
let not_root pkg ver vs_singleton =
130
+
{ terms = [(pkg, Negative (vs_singleton ver))];
131
+
cause = Root (pkg, ver) }
133
+
let no_versions pkg term =
136
+
{ terms = [(pkg, term)];
137
+
cause = NoVersions (pkg, vs) }
139
+
failwith "Expected positive term"
141
+
let from_dependency pkg_from vs_from pkg_to vs_to =
142
+
{ terms = [(pkg_from, Positive vs_from); (pkg_to, Negative vs_to)];
143
+
cause = Dependency (pkg_from, vs_from, pkg_to, vs_to) }
145
+
let from_derivation incomp1 incomp2 =
146
+
{ terms = []; (* This will be populated during conflict resolution *)
147
+
cause = Derived (incomp1, incomp2) }
150
+
(* Partial Solutions *)
151
+
type ('p, 'v, 'vs) partial_solution = {
152
+
decision_level : int;
153
+
decisions : ('p * 'v) list;
154
+
assignments : ('p * ('v, 'vs) term * int * bool) list;
157
+
module PartialSolution = struct
158
+
type ('p, 'v, 'vs) t = ('p, 'v, 'vs) partial_solution
161
+
decision_level = 0;
166
+
let current_decision_level solution = solution.decision_level
168
+
let add_decision solution package version vs_singleton =
169
+
let decision_level = solution.decision_level + 1 in
170
+
let new_assignment = (package, Positive (vs_singleton version), decision_level, true) in
173
+
decisions = (package, version) :: solution.decisions;
174
+
assignments = new_assignment :: solution.assignments;
177
+
let add_derivation solution package term cause_incompat decision_level =
178
+
let new_assignment = (package, term, decision_level, false) in
180
+
assignments = new_assignment :: solution.assignments;
183
+
let check_assignment p_compare pkg term (assign_pkg, assign_term, _, _) =
184
+
if p_compare assign_pkg pkg = 0 then
185
+
match assign_term, term with
186
+
| Positive _, Positive _ -> true
187
+
| Negative _, Negative _ -> true
192
+
let relation solution p_compare incompatibility =
193
+
let rec check_terms satisfied unsatisfied_term = function
195
+
if satisfied then `Satisfied else `AlmostSatisfied unsatisfied_term
196
+
| (pkg, term) :: rest ->
197
+
let pkg_satisfies =
198
+
List.exists (fun a -> check_assignment p_compare pkg term a) solution.assignments in
199
+
if pkg_satisfies then
200
+
check_terms satisfied unsatisfied_term rest
202
+
check_terms false (pkg, term) rest
204
+
check_terms true (List.hd incompatibility.terms) incompatibility.terms
206
+
let extract_solution solution =
207
+
solution.decisions |> List.rev
209
+
let backtrack solution level =
210
+
let new_assignments =
211
+
List.filter (fun (_, _, assignment_level, _) -> assignment_level <= level) solution.assignments in
212
+
let new_decisions =
213
+
List.filter (fun (_, _) -> level <= solution.decision_level) solution.decisions in
214
+
{ decision_level = level; assignments = new_assignments; decisions = new_decisions }
217
+
(* Dependency Provider *)
218
+
module type DEPENDENCY_PROVIDER = sig
224
+
val get_root_package : unit -> package_id
225
+
val get_root_version : unit -> version
226
+
val available_versions : package_id -> version list
227
+
val get_dependencies : package_id -> version -> ((package_id * version_set) list, error) result
228
+
val choose_version : package_id -> version_set -> version option
231
+
(* Solver Configuration *)
233
+
max_iterations : int option;
236
+
let default_config = {
237
+
max_iterations = None;
240
+
(* Main Solver Interface *)
241
+
module type SOLVER = sig
248
+
| Unsatisfiable of {
249
+
explanation : string;
251
+
| DependencyProviderError of {
252
+
package : package_id;
256
+
| MaxIterationsExceeded
258
+
type solution = (package_id * version) list
261
+
(module DEPENDENCY_PROVIDER with
262
+
type package_id = package_id and
263
+
type version = version and
264
+
type version_set = version_set and
265
+
type error = string) ->
267
+
(solution, error) result
269
+
val explain_error : error -> string
272
+
(* Functor Implementation *)
276
+
(VS : VERSION_SET with type version = V.t) = struct
278
+
type package_id = P.t
280
+
type version_set = VS.t
281
+
type metadata = string
284
+
| Unsatisfiable of {
285
+
explanation : string;
287
+
| DependencyProviderError of {
288
+
package : package_id;
292
+
| MaxIterationsExceeded
294
+
type solution = (package_id * version) list
296
+
(* Helper functions for the PubGrub algorithm *)
298
+
let add_incompatibility_from_dependencies package version deps =
299
+
List.map (fun (dep_pkg, dep_vs) ->
300
+
Incompatibility.from_dependency package (VS.singleton version) dep_pkg dep_vs
303
+
let check_max_iterations config iterations =
304
+
match config.max_iterations with
305
+
| Some max when iterations >= max -> Error MaxIterationsExceeded
308
+
let process_unit_propagation solution incompatibility =
309
+
match PartialSolution.relation solution P.compare incompatibility with
311
+
Error (`Conflict incompatibility)
312
+
| `AlmostSatisfied (pkg, term) ->
313
+
(* Add derived assignment *)
315
+
PartialSolution.add_derivation
316
+
solution pkg (Term.negate term) incompatibility solution.decision_level in
321
+
let unit_propagation solution incompatibilities package =
322
+
let relevant_incompats =
323
+
List.filter (fun incomp ->
324
+
List.exists (fun (pkg, _) -> P.compare pkg package = 0) incomp.terms
325
+
) incompatibilities in
327
+
let rec process_incompats solution = function
328
+
| [] -> Ok solution
329
+
| incomp :: rest ->
330
+
match process_unit_propagation solution incomp with
331
+
| Ok new_solution -> process_incompats new_solution rest
332
+
| Error e -> Error e
334
+
process_incompats solution relevant_incompats
336
+
let propagate_all solution incompatibilities pending_packages =
337
+
let rec propagate solution = function
338
+
| [] -> Ok solution
340
+
match unit_propagation solution incompatibilities pkg with
341
+
| Ok new_solution -> propagate new_solution rest
342
+
| Error (`Conflict incomp) ->
343
+
(* Simple conflict handling for now - just fails with explanation *)
345
+
Printf.sprintf "Conflict found for package %s" (P.to_string pkg) in
346
+
Error (Unsatisfiable { explanation })
348
+
propagate solution pending_packages
350
+
let get_packages_with_constraints solution =
351
+
List.fold_left (fun acc (package, _, _, _) ->
352
+
if List.exists (fun (p, _) -> P.compare p package = 0) solution.decisions then
356
+
) [] solution.assignments
357
+
|> List.sort_uniq P.compare
359
+
let get_package_constraints solution package =
360
+
List.fold_left (fun acc (pkg, term, _, _) ->
361
+
if P.compare pkg package = 0 then
365
+
) [] solution.assignments
367
+
let compute_effective_range constraints =
368
+
let process_constraint range term =
369
+
match term, range with
370
+
| Positive vs1, Positive vs2 ->
371
+
Positive (VS.intersection vs1 vs2)
372
+
| Negative vs1, Positive vs2 ->
373
+
let complement = VS.complement vs1 in
374
+
Positive (VS.intersection vs2 complement)
375
+
| Positive vs1, Negative vs2 ->
376
+
let complement = VS.complement vs2 in
377
+
Positive (VS.intersection vs1 complement)
378
+
| Negative vs1, Negative vs2 ->
379
+
Negative (VS.union vs1 vs2)
382
+
match constraints with
383
+
| [] -> Positive VS.any
385
+
List.fold_left process_constraint first rest
387
+
let extract_version_set = function
388
+
| Positive vs -> vs
389
+
| Negative vs -> VS.complement vs
391
+
(* Main solver implementation *)
393
+
(module Provider : DEPENDENCY_PROVIDER with
394
+
type package_id = package_id and
395
+
type version = version and
396
+
type version_set = version_set and
397
+
type error = string)
398
+
(config : 'a config) =
400
+
let root_pkg = Provider.get_root_package () in
401
+
let root_version = Provider.get_root_version () in
403
+
let initial_solution = PartialSolution.empty in
404
+
let initial_incompats = [
405
+
Incompatibility.not_root root_pkg root_version VS.singleton
408
+
let rec solve_loop solution incompatibilities iterations =
409
+
match check_max_iterations config iterations with
410
+
| Error e -> Error e
412
+
(* Get all packages that need propagation *)
413
+
let pending_packages =
414
+
List.map (fun (package, _, _, _) -> package) solution.assignments in
416
+
(* Run unit propagation on all packages *)
417
+
match propagate_all solution incompatibilities pending_packages with
418
+
| Error e -> Error e
419
+
| Ok propagated_solution ->
420
+
(* Check if we're done *)
421
+
if List.length propagated_solution.decisions = 0 then
423
+
else if List.exists (fun (pkg, _) -> P.compare pkg root_pkg = 0) propagated_solution.decisions then
424
+
(* We have a solution *)
425
+
Ok (PartialSolution.extract_solution propagated_solution)
427
+
(* Decision making - pick next package to decide on *)
428
+
let packages_with_constraints =
429
+
get_packages_with_constraints propagated_solution in
431
+
match packages_with_constraints with
433
+
(* No more packages to decide on, we're done *)
434
+
Ok (PartialSolution.extract_solution propagated_solution)
436
+
(* Find constraints for this package *)
438
+
get_package_constraints propagated_solution next_pkg in
440
+
(* Compute effective range *)
441
+
let effective_range =
442
+
compute_effective_range constraints in
444
+
(* Choose version *)
445
+
let effective_vs = extract_version_set effective_range in
447
+
match Provider.choose_version next_pkg effective_vs with
449
+
(* No valid version - add incompatibility and backtrack *)
450
+
let incomp = Incompatibility.no_versions next_pkg effective_range in
451
+
solve_loop propagated_solution (incomp :: incompatibilities) (iterations + 1)
453
+
(* Get dependencies for this version *)
454
+
match Provider.get_dependencies next_pkg version with
456
+
Error (DependencyProviderError {
457
+
package = next_pkg;
462
+
(* Add decision and dependencies as incompatibilities *)
464
+
PartialSolution.add_decision
465
+
propagated_solution next_pkg version VS.singleton in
467
+
let new_incompats =
468
+
add_incompatibility_from_dependencies next_pkg version deps in
472
+
(new_incompats @ incompatibilities)
476
+
match solve_loop initial_solution initial_incompats 0 with
478
+
(* Empty solution - just return the root package *)
479
+
Ok [(root_pkg, root_version)]
480
+
| Ok solution -> Ok solution
481
+
| Error e -> Error e
483
+
(* Format error messages *)
484
+
let explain_error = function
485
+
| Unsatisfiable { explanation } ->
486
+
"Dependency resolution failed: " ^ explanation
487
+
| DependencyProviderError { package; version; message } ->
488
+
Printf.sprintf "Error retrieving dependencies for %s %s: %s"
489
+
(P.to_string package) (V.to_string version) message
490
+
| MaxIterationsExceeded ->
491
+
"Dependency resolution exceeded maximum iterations"
anil.recoil.org