Build:
- 1
- 0
2026-09-03 17:20.00: New job: build theo.0.1.0 (12587ba2e6d8)
2026-09-03 17:20.00: Waiting for resource in pool day11-builds
2026-09-03 17:43.30: Got resource from pool day11-builds
2026-09-03 17:43.30: [profile full] build theo.0.1.0
2026-09-03 17:43.30: build theo.0.1.0 (12587ba2e6d8)
=== DEPENDENCIES (7 transitive) ===
base-threads.base 3d2f2cbc6db2
base-unix.base 3a38ddca6b5e
compiler-cloning.enabled 966a2e6839f0
dune.3.24.2 ec704e062ad3
ocaml.5.5.0 22ebd7932512
ocaml-base-compiler.5.5.0 db1659234e8a
ocaml-compiler.5.5.0 7f52fb26d939
=== STDOUT ===
Processing: [default: loading data]
[theo.0.1.0: dl]
[theo.0.1.0: extract]
-> retrieved theo.0.1.0 (https://opam.ocaml.org/cache)
[theo: dune build]
+ /home/opam/.opam/default/bin/dune "build" "-p" "theo" "-j" "39" "@install" (CWD=/home/opam/.opam/default/.opam-switch/build/theo.0.1.0)
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I src/lib-theo/.theo.objs/byte -cmi-file src/lib-theo/.theo.objs/byte/theo.cmi -no-alias-deps -o src/lib-theo/.theo.objs/byte/theo.cmo -c -impl src/lib-theo/theo.ml)
- File "src/lib-theo/theo.ml", lines 243-256, characters 4-25:
- 243 | ....match u with
- 244 | | False -> Zero (* False *)
- 245 | | Not False -> One (* True *)
- 246 | | If { atom; high; negate_high; low; _ } ->
- 247 | (* if v then (high ^ neg) else low *)
- ...
- 253 | (* = if v then not (high ^ neg) else not low *)
- 254 | let h = with_polarity (Stdlib.not negate_high) high in
- 255 | let l = with_polarity true low in
- 256 | Node (atom, l, h)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not (Not _)
-
- File "src/lib-theo/theo.ml", line 358, characters 30-74:
- 358 | let id (u : positive u) = match u with False -> 0 | If { id; _ } -> id
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 364-377, characters 8-36:
- 364 | ........match (t, t') with
- 365 | | ( If { atom; high; negate_high; low; _ },
- 366 | If
- 367 | {
- 368 | atom = atom';
- ...
- 374 | Atom.equal atom atom' && high == high' && negate_high = negate_high'
- 375 | && low == low'
- 376 | | False, False -> true
- 377 | | If _, _ | _, If _ -> false
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (False, Not _)
-
- File "src/lib-theo/theo.ml", lines 380-389, characters 8-29:
- 380 | ........match t with
- 381 | | False -> 0
- 382 | | If { atom = Atom atom; high; negate_high; low; _ } ->
- 383 | let h =
- 384 | atom.id
- 385 | |> combine (id high)
- 386 | |> combine (if negate_high then 1 else 0)
- 387 | |> combine (id low)
- 388 | in
- 389 | h lxor (h lsr 17)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 404-408, characters 6-28:
- 404 | ......match node with
- 405 | | If { id = id'; _ } when Int.equal id id' ->
- 406 | next_id := !next_id + 1;
- 407 | node
- 408 | | If _ | False -> node
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 469-506, characters 6-77:
- 469 | ......match low with
- 470 | | Bdd
- 471 | (If
- 472 | {
- 473 | atom = l_atom;
- ...
- 503 | then low
- 504 | else
- 505 | let negate_high, h_node = split high in
- 506 | Bdd (Not (Node.ite atom h_node (Stdlib.not negate_high) l_inner))
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Bdd (Not (Not _))
-
- File "src/lib-theo/theo.ml", line 511, characters 4-64:
- 511 | match u with If { atom; _ } -> atom | False -> Atom.sentinel
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 516-528, characters 4-21:
- 516 | ....match u with
- 517 | | If { atom; high; negate_high; low; _ } ->
- 518 | if atom == v then
- 519 | let eff_neg_high =
- 520 | if negate_t then Stdlib.not negate_high else negate_high
- ...
- 525 | else
- 526 | let simplified = prune v u atom high negate_high low negate_t in
- 527 | (simplified, t)
- 528 | | False -> (t, t)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 912-926, characters 12-17:
- 912 | ............match u with
- 913 | | False -> false_
- 914 | | If { atom = Atom atom; high; negate_high; low; _ } -> (
- 915 | if atom.var > max_var then Bdd u
- 916 | else
- ...
- 923 | let h = visit high in
- 924 | let l = visit low in
- 925 | make_node (Atom atom) (if negate_high then not h else h) l
- 926 | )
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 1085-1103, characters 12-53:
- 1085 | ............match u with
- 1086 | | False -> if negate then true_ else false_
- 1087 | | If { atom = Atom atom; high; negate_high; low; _ } -> (
- 1088 | if atom.var > target_var then with_polarity negate u
- 1089 | else
- ...
- 1100 | | Bdd (Not l_inner) ->
- 1101 | let res = make_node (Atom atom) (not h) (Bdd l_inner) in
- 1102 | not res
- 1103 | | _ -> make_node (Atom atom) h l)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 1154-1165, characters 6-58:
- 1154 | ......match u with
- 1155 | | False -> [] (* Only reached if valid, so return empty constraints *)
- 1156 | | If { atom; high; negate_high; low; _ } ->
- 1157 | (* Prefer high branch. Check if high is capable of satisfying
- 1158 | eff_target. *)
- ...
- 1162 | in
- 1163 | if high_satisfiable then
- 1164 | { atom; value = true } :: solve high eff_target
- 1165 | else { atom; value = false } :: solve low target
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 1181-1196, characters 12-23:
- 1181 | ............match (u, target) with
- 1182 | | False, true -> max_int (* Impossible *)
- 1183 | | False, false -> 0 (* Reached! *)
- 1184 | | If { high; negate_high; low; _ }, _ ->
- 1185 | let eff_target_high =
- ...
- 1193 | if d_high = max_int && d_low = max_int then max_int
- 1194 | else 1 + min d_high d_low
- 1195 | in
- 1196 | min_d
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (Not _, _)
-
- File "src/lib-theo/theo.ml", lines 1203-1218, characters 6-58:
- 1203 | ......match (u, target) with
- 1204 | | False, false -> []
- 1205 | | False, true -> assert false
- 1206 | | If { atom; high; negate_high; low; _ }, _ ->
- 1207 | let eff_target_high =
- ...
- 1215 | let d_low = get_dist low target in
- 1216 | d_high <= d_low
- 1217 | then { atom; value = true } :: trace high eff_target_high
- 1218 | else { atom; value = false } :: trace low target
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (Not _, _)
-
- File "src/lib-theo/theo.ml", lines 1308-1319, characters 8-18:
- 1308 | ........match u with
- 1309 | | False -> ()
- 1310 | | If { atom = Atom { var; category; id = aid; _ }; high; low; _ } ->
- 1311 | (match category with
- 1312 | | Bool -> ()
- ...
- 1316 | | Some _ -> ()
- 1317 | | None -> Hashtbl.add seen var aid));
- 1318 | go high;
- 1319 | go low.
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -I src/lib-theo/.theo.objs/byte -I src/lib-theo/.theo.objs/native -cmi-file src/lib-theo/.theo.objs/byte/theo.cmi -no-alias-deps -o src/lib-theo/.theo.objs/native/theo.cmx -c -impl src/lib-theo/theo.ml)
- File "src/lib-theo/theo.ml", lines 243-256, characters 4-25:
- 243 | ....match u with
- 244 | | False -> Zero (* False *)
- 245 | | Not False -> One (* True *)
- 246 | | If { atom; high; negate_high; low; _ } ->
- 247 | (* if v then (high ^ neg) else low *)
- ...
- 253 | (* = if v then not (high ^ neg) else not low *)
- 254 | let h = with_polarity (Stdlib.not negate_high) high in
- 255 | let l = with_polarity true low in
- 256 | Node (atom, l, h)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not (Not _)
-
- File "src/lib-theo/theo.ml", line 358, characters 30-74:
- 358 | let id (u : positive u) = match u with False -> 0 | If { id; _ } -> id
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 364-377, characters 8-36:
- 364 | ........match (t, t') with
- 365 | | ( If { atom; high; negate_high; low; _ },
- 366 | If
- 367 | {
- 368 | atom = atom';
- ...
- 374 | Atom.equal atom atom' && high == high' && negate_high = negate_high'
- 375 | && low == low'
- 376 | | False, False -> true
- 377 | | If _, _ | _, If _ -> false
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (False, Not _)
-
- File "src/lib-theo/theo.ml", lines 380-389, characters 8-29:
- 380 | ........match t with
- 381 | | False -> 0
- 382 | | If { atom = Atom atom; high; negate_high; low; _ } ->
- 383 | let h =
- 384 | atom.id
- 385 | |> combine (id high)
- 386 | |> combine (if negate_high then 1 else 0)
- 387 | |> combine (id low)
- 388 | in
- 389 | h lxor (h lsr 17)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 404-408, characters 6-28:
- 404 | ......match node with
- 405 | | If { id = id'; _ } when Int.equal id id' ->
- 406 | next_id := !next_id + 1;
- 407 | node
- 408 | | If _ | False -> node
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 469-506, characters 6-77:
- 469 | ......match low with
- 470 | | Bdd
- 471 | (If
- 472 | {
- 473 | atom = l_atom;
- ...
- 503 | then low
- 504 | else
- 505 | let negate_high, h_node = split high in
- 506 | Bdd (Not (Node.ite atom h_node (Stdlib.not negate_high) l_inner))
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Bdd (Not (Not _))
-
- File "src/lib-theo/theo.ml", line 511, characters 4-64:
- 511 | match u with If { atom; _ } -> atom | False -> Atom.sentinel
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 516-528, characters 4-21:
- 516 | ....match u with
- 517 | | If { atom; high; negate_high; low; _ } ->
- 518 | if atom == v then
- 519 | let eff_neg_high =
- 520 | if negate_t then Stdlib.not negate_high else negate_high
- ...
- 525 | else
- 526 | let simplified = prune v u atom high negate_high low negate_t in
- 527 | (simplified, t)
- 528 | | False -> (t, t)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 912-926, characters 12-17:
- 912 | ............match u with
- 913 | | False -> false_
- 914 | | If { atom = Atom atom; high; negate_high; low; _ } -> (
- 915 | if atom.var > max_var then Bdd u
- 916 | else
- ...
- 923 | let h = visit high in
- 924 | let l = visit low in
- 925 | make_node (Atom atom) (if negate_high then not h else h) l
- 926 | )
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 1085-1103, characters 12-53:
- 1085 | ............match u with
- 1086 | | False -> if negate then true_ else false_
- 1087 | | If { atom = Atom atom; high; negate_high; low; _ } -> (
- 1088 | if atom.var > target_var then with_polarity negate u
- 1089 | else
- ...
- 1100 | | Bdd (Not l_inner) ->
- 1101 | let res = make_node (Atom atom) (not h) (Bdd l_inner) in
- 1102 | not res
- 1103 | | _ -> make_node (Atom atom) h l)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 1154-1165, characters 6-58:
- 1154 | ......match u with
- 1155 | | False -> [] (* Only reached if valid, so return empty constraints *)
- 1156 | | If { atom; high; negate_high; low; _ } ->
- 1157 | (* Prefer high branch. Check if high is capable of satisfying
- 1158 | eff_target. *)
- ...
- 1162 | in
- 1163 | if high_satisfiable then
- 1164 | { atom; value = true } :: solve high eff_target
- 1165 | else { atom; value = false } :: solve low target
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-
- File "src/lib-theo/theo.ml", lines 1181-1196, characters 12-23:
- 1181 | ............match (u, target) with
- 1182 | | False, true -> max_int (* Impossible *)
- 1183 | | False, false -> 0 (* Reached! *)
- 1184 | | If { high; negate_high; low; _ }, _ ->
- 1185 | let eff_target_high =
- ...
- 1193 | if d_high = max_int && d_low = max_int then max_int
- 1194 | else 1 + min d_high d_low
- 1195 | in
- 1196 | min_d
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (Not _, _)
-
- File "src/lib-theo/theo.ml", lines 1203-1218, characters 6-58:
- 1203 | ......match (u, target) with
- 1204 | | False, false -> []
- 1205 | | False, true -> assert false
- 1206 | | If { atom; high; negate_high; low; _ }, _ ->
- 1207 | let eff_target_high =
- ...
- 1215 | let d_low = get_dist low target in
- 1216 | d_high <= d_low
- 1217 | then { atom; value = true } :: trace high eff_target_high
- 1218 | else { atom; value = false } :: trace low target
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (Not _, _)
-
- File "src/lib-theo/theo.ml", lines 1308-1319, characters 8-18:
- 1308 | ........match u with
- 1309 | | False -> ()
- 1310 | | If { atom = Atom { var; category; id = aid; _ }; high; low; _ } ->
- 1311 | (match category with
- 1312 | | Bool -> ()
- ...
- 1316 | | Some _ -> ()
- 1317 | | None -> Hashtbl.add seen var aid));
- 1318 | go high;
- 1319 | go low.
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Not _
-> compiled theo.0.1.0
-> installed theo.0.1.0
=== STDERR ===
2026-09-03 17:43.36: OK: build theo.0.1.0 (runc: 2.1s, disk: 22KB)
2026-09-03 17:43.36: Job succeeded