2025-05-23 09:36.25: New job: test ocaml-gospel/ortac https://github.com/ocaml-gospel/ortac.git#refs/pull/310/head (11c574517a2b3f3296e7f015389109683a2f9e69) (linux-x86_64:(lint-fmt)) Base: ocaml/opam:debian-12-ocaml-4.08@sha256:48fa4a7216c3973bb95572cf5dca98cbbcefe90f288f552e7ac70a8ccd438aa7 ocamlformat version: version 0.27.0 (from opam) To reproduce locally: git clone --recursive "https://github.com/ocaml-gospel/ortac.git" && cd "ortac" && git fetch origin "refs/pull/310/head" && git reset --hard 11c57451 cat > Dockerfile <<'END-OF-DOCKERFILE' FROM ocaml/opam:debian-12-ocaml-4.08@sha256:48fa4a7216c3973bb95572cf5dca98cbbcefe90f288f552e7ac70a8ccd438aa7 USER 1000:1000 RUN cd ~/opam-repository && (git cat-file -e 35eb2f107a989a2d623b0bbe170696398fcb9b1e || git fetch origin master) && git reset -q --hard 35eb2f107a989a2d623b0bbe170696398fcb9b1e && git log --no-decorate -n1 --oneline && opam update -u RUN opam depext -i dune WORKDIR /src RUN opam depext -i ocamlformat=0.27.0 COPY --chown=1000:1000 . /src/ RUN opam exec -- dune build @fmt --ignore-promoted-rules || (echo "dune build @fmt failed"; exit 2) END-OF-DOCKERFILE docker build . END-REPRO-BLOCK 2025-05-23 09:36.25: Using cache hint "ocaml-gospel/ortac-ocaml/opam:debian-12-ocaml-4.08@sha256:48fa4a7216c3973bb95572cf5dca98cbbcefe90f288f552e7ac70a8ccd438aa7-debian-12-4.08_opam-2.3-ocamlformat-35eb2f107a989a2d623b0bbe170696398fcb9b1e" 2025-05-23 09:36.25: Using OBuilder spec: ((from ocaml/opam:debian-12-ocaml-4.08@sha256:48fa4a7216c3973bb95572cf5dca98cbbcefe90f288f552e7ac70a8ccd438aa7) (user (uid 1000) (gid 1000)) (run (cache (opam-archives (target /home/opam/.opam/download-cache))) (network host) (shell "cd ~/opam-repository && (git cat-file -e 35eb2f107a989a2d623b0bbe170696398fcb9b1e || git fetch origin master) && git reset -q --hard 35eb2f107a989a2d623b0bbe170696398fcb9b1e && git log --no-decorate -n1 --oneline && opam update -u")) (run (cache (opam-archives (target /home/opam/.opam/download-cache))) (network host) (shell "opam depext -i dune")) (workdir /src) (run (cache (opam-archives (target /home/opam/.opam/download-cache))) (network host) (shell "opam depext -i ocamlformat=0.27.0")) (copy (src .) (dst /src/)) (run (shell "opam exec -- dune build @fmt --ignore-promoted-rules || (echo \"dune build @fmt failed\"; exit 2)")) ) 2025-05-23 09:36.25: Waiting for resource in pool OCluster 2025-05-23 09:36.25: Waiting for worker… 2025-05-23 09:38.23: Got resource from pool OCluster Building on phoebe.caelum.ci.dev All commits already cached HEAD is now at 11c5745 updt test (from ocaml/opam:debian-12-ocaml-4.08@sha256:48fa4a7216c3973bb95572cf5dca98cbbcefe90f288f552e7ac70a8ccd438aa7) 2025-05-23 09:40.38 ---> saved as "d1b97f3f32fc7cff4791d73e3fff398d19cc5b0541c709028ff05a921e22d2c8" /: (user (uid 1000) (gid 1000)) /: (run (cache (opam-archives (target /home/opam/.opam/download-cache))) (network host) (shell "cd ~/opam-repository && (git cat-file -e 35eb2f107a989a2d623b0bbe170696398fcb9b1e || git fetch origin master) && git reset -q --hard 35eb2f107a989a2d623b0bbe170696398fcb9b1e && git log --no-decorate -n1 --oneline && opam update -u")) 35eb2f107a Merge pull request #27838 from maiste/release-dune-3.18.2 <><> Updating package repositories ><><><><><><><><><><><><><><><><><><><><><><> [default] Initialised default (at git+file:///home/opam/opam-repository): [INFO] opam 2.1 and 2.2 include many performance and security improvements over 2.0; please consider upgrading (https://opam.ocaml.org/doc/Install.html) Everything as up-to-date as possible (run with --verbose to show unavailable upgrades). However, you may "opam upgrade" these packages explicitly, which will ask permission to downgrade or uninstall the conflicting packages. Nothing to do. # Run eval $(opam env) to update the current shell environment 2025-05-23 09:43.18 ---> saved as "0ed37ff9180ea5331ab17e3106ce3fc10bf21b69021c66107f159798cee036fc" /: (run (cache (opam-archives (target /home/opam/.opam/download-cache))) (network host) (shell "opam depext -i dune")) # Detecting depexts using vars: arch=x86_64, os=linux, os-distribution=debian, os-family=debian # No extra OS packages requirements found. # All required OS packages found. # Now letting opam install the packages The following actions will be performed: - install dune 3.18.2 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [dune.3.18.2] found in cache <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> installed dune.3.18.2 Done. # Run eval $(opam env) to update the current shell environment 2025-05-23 09:45.56 ---> saved as "dc3dc92082cbd6b1d2902dc06db6b555f449a0b1c6f054b5888f3ddab10a5d9e" /: (workdir /src) /src: (run (cache (opam-archives (target /home/opam/.opam/download-cache))) (network host) (shell "opam depext -i ocamlformat=0.27.0")) # Detecting depexts using vars: arch=x86_64, os=linux, os-distribution=debian, os-family=debian # No extra OS packages requirements found. # All required OS packages found. # Now letting opam install the packages The following actions will be performed: - install sexplib0 v0.14.0 [required by base] - install dune-build-info 3.18.2 [required by ocamlformat-lib] - install cmdliner 1.3.0 [required by ocamlformat] - install menhirLib 20240715 [required by ocamlformat-lib] - install menhirCST 20240715 [required by menhir] - install ocamlbuild 0.16.1 [required by fpath, astring, uuseg] - install menhirSdk 20240715 [required by ocamlformat-lib] - install either 1.0.0 [required by ocamlformat-lib] - install ocaml-version 4.0.0 [required by ocamlformat-lib] - install camlp-streams 5.0.1 [required by ocamlformat-lib] - install csexp 1.5.2 [required by ocamlformat] - install seq base [required by re] - install fix 20250428 [required by ocamlformat-lib] - install ocamlfind 1.9.8 [required by ocp-indent, astring, fpath, uuseg] - install menhir 20240715 [required by ocamlformat-lib] - install dune-configurator 3.18.2 [required by base] - install re 1.11.0 [required by ocamlformat] - install topkg 1.0.8 [required by fpath, astring, uuseg] - install base-bytes base [required by ocp-indent] - install base v0.14.3 [required by ocamlformat-lib] - install uutf 1.0.4 [required by ocamlformat-lib] - install astring 0.8.5 [required by ocamlformat-lib] - install ocp-indent 1.8.1 [required by ocamlformat-lib] - install stdio v0.14.0 [required by ocamlformat-lib] - install uucp 15.0.0 [required by uuseg] - install fpath 0.7.3 [required by ocamlformat-lib] - install uuseg 15.0.0 [required by ocamlformat-lib] - install ocamlformat-lib 0.27.0 [required by ocamlformat] - install ocamlformat 0.27.0 ===== 29 to install ===== <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [astring.0.8.5] found in cache [base.v0.14.3] found in cache [camlp-streams.5.0.1] found in cache [cmdliner.1.3.0] found in cache [csexp.1.5.2] found in cache [dune-build-info.3.18.2] found in cache [dune-configurator.3.18.2] found in cache [either.1.0.0] found in cache [fix.20250428] found in cache [fpath.0.7.3] found in cache [menhir.20240715] found in cache [menhirCST.20240715] found in cache [menhirLib.20240715] found in cache [menhirSdk.20240715] found in cache [ocaml-version.4.0.0] found in cache [ocamlbuild.0.16.1] found in cache [ocamlfind.1.9.8] found in cache [ocamlformat.0.27.0] found in cache [ocamlformat-lib.0.27.0] found in cache [ocp-indent.1.8.1] found in cache [re.1.11.0] found in cache [sexplib0.v0.14.0] found in cache [stdio.v0.14.0] found in cache [topkg.1.0.8] found in cache [uucp.15.0.0] found in cache [uuseg.15.0.0] found in cache [uutf.1.0.4] found in cache <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> installed seq.base -> installed camlp-streams.5.0.1 -> installed csexp.1.5.2 -> installed either.1.0.0 -> installed fix.20250428 -> installed menhirCST.20240715 -> installed menhirLib.20240715 -> installed menhirSdk.20240715 -> installed cmdliner.1.3.0 -> installed ocaml-version.4.0.0 -> installed re.1.11.0 -> installed sexplib0.v0.14.0 -> installed dune-build-info.3.18.2 -> installed dune-configurator.3.18.2 -> installed ocamlfind.1.9.8 -> installed base-bytes.base -> installed ocp-indent.1.8.1 -> installed ocamlbuild.0.16.1 -> installed base.v0.14.3 -> installed topkg.1.0.8 -> installed stdio.v0.14.0 -> installed uutf.1.0.4 -> installed astring.0.8.5 -> installed menhir.20240715 -> installed fpath.0.7.3 -> installed uucp.15.0.0 -> installed uuseg.15.0.0 -> installed ocamlformat-lib.0.27.0 -> installed ocamlformat.0.27.0 Done. <><> ocp-indent.1.8.1 installed successfully ><><><><><><><><><><><><><><><><><> => This package requires additional configuration for use in editors. Install package 'user-setup', or manually: * for Emacs, add these lines to ~/.emacs: (add-to-list 'load-path "/home/opam/.opam/4.08/share/emacs/site-lisp") (require 'ocp-indent) * for Vim, add this line to ~/.vimrc: set rtp^="/home/opam/.opam/4.08/share/ocp-indent/vim" # Run eval $(opam env) to update the current shell environment 2025-05-23 09:48.59 ---> saved as "5e3a5282f655843df8e02a2497598f2918acc59345107286c51ff04d386b492b" /src: (copy (src .) (dst /src/)) 2025-05-23 09:49.00 ---> saved as "4a7d922b51d2dfe3f5bb72ac02521cb903faf14d143631a57721f6c36bfa17a6" /src: (run (shell "opam exec -- dune build @fmt --ignore-promoted-rules || (echo \"dune build @fmt failed\"; exit 2)")) File "plugins/wrapper/test/generated/braun_tree.ml", line 1, characters 0-0: diff --git a/_build/default/plugins/wrapper/test/generated/braun_tree.ml b/_build/default/plugins/wrapper/test/generated/.formatted/braun_tree.ml index 69173f5..c96db74 100644 --- a/_build/default/plugins/wrapper/test/generated/braun_tree.ml +++ b/_build/default/plugins/wrapper/test/generated/.formatted/braun_tree.ml @@ -1,37 +1,34 @@ type 'a t = Empty | Tree of 'a t * 'a * 'a t -let rec get t i = match t with +let rec get t i = + match t with | Empty -> assert false - | Tree (l, x, r) -> if i = 0 then x else - if i mod 2 = 1 then get l (i/2) else get r (i/2 - 1) - -let head = function - | Empty -> failwith "No head" - | Tree (_, x, _) -> x - -let left_t = function - | Empty -> failwith "No left tree" - | Tree (l, _, _) -> l -let right_t = function - | Empty -> assert false - | Tree (_, _, r) -> r + | Tree (l, x, r) -> + if i = 0 then x + else if i mod 2 = 1 then get l (i / 2) + else get r ((i / 2) - 1) +let head = function Empty -> failwith "No head" | Tree (_, x, _) -> x +let left_t = function Empty -> failwith "No left tree" | Tree (l, _, _) -> l +let right_t = function Empty -> assert false | Tree (_, _, r) -> r let empty () = Empty -let rec diff t n = match t, n with +let rec diff t n = + match (t, n) with | Empty, 0 -> 0 | Tree _, 0 -> 1 - | Tree (l, _, _), n when n mod 2 = 1 -> diff l ((n-1)/2) - | Tree (_, _, r), n when n mod 2 = 0 -> diff r ((n-2)/2) - | _ , _ -> failwith "No more cases" + | Tree (l, _, _), n when n mod 2 = 1 -> diff l ((n - 1) / 2) + | Tree (_, _, r), n when n mod 2 = 0 -> diff r ((n - 2) / 2) + | _, _ -> failwith "No more cases" let rec size = function | Empty -> 0 | Tree (l, _, r) -> - let m = size r in - 1 + 2 * m + diff l m + let m = size r in + 1 + (2 * m) + diff l m -let rec cons v t = match t with +let rec cons v t = + match t with | Empty -> Tree (Empty, v, Empty) | Tree (l, x, r) -> Tree (cons x r, v, l) @@ -40,38 +37,34 @@ let rec tail = function | Tree (Empty, _, Empty) -> Empty | Tree (l, _, r) -> Tree (r, get l 0, tail l) -let rec snoc x t = match t with +let rec snoc x t = + match t with | Empty -> Tree (Empty, x, Empty) | Tree (l, e, r) -> - if size t mod 2 = 0 - then Tree(l, e, snoc x r) - else Tree (snoc x l, e, r) + if size t mod 2 = 0 then Tree (l, e, snoc x r) else Tree (snoc x l, e, r) -let rec liat t = match t with +let rec liat t = + match t with | Empty -> failwith "Already empty" | Tree (Empty, _, Empty) -> Empty | Tree (l, x, r) -> - if size t mod 2 = 0 - then Tree (liat l, x, r) - else Tree (l, x, liat r) + if size t mod 2 = 0 then Tree (liat l, x, r) else Tree (l, x, liat r) let to_list t = - let rec aux acc t = match t with - | Empty -> acc - | Tree (Empty, x, _) -> x :: acc - | Tree (l, x, Empty) -> aux (x :: acc) l - | Tree (_, x, _) -> - let nt = tail t in - aux (x :: acc) nt + let rec aux acc t = + match t with + | Empty -> acc + | Tree (Empty, x, _) -> x :: acc + | Tree (l, x, Empty) -> aux (x :: acc) l + | Tree (_, x, _) -> + let nt = tail t in + aux (x :: acc) nt in List.rev (aux [] t) let of_list l = - let rec aux acc = function - | [] -> acc - | hd :: tl -> - aux (snoc hd acc) tl - in aux Empty l + let rec aux acc = function [] -> acc | hd :: tl -> aux (snoc hd acc) tl in + aux Empty l let cont = to_list @@ -80,4 +73,3 @@ let cont = to_list if i mod 2 <> 0 then find ((i - 1) / 2) (left_t t) else find ((i / 2) - 1) (right_t t) *) - File "plugins/wrapper/test/generated/braun_tree.mli", line 1, characters 0-0: diff --git a/_build/default/plugins/wrapper/test/generated/braun_tree.mli b/_build/default/plugins/wrapper/test/generated/.formatted/braun_tree.mli index 064eb5a..4a454f5 100644 --- a/_build/default/plugins/wrapper/test/generated/braun_tree.mli +++ b/_build/default/plugins/wrapper/test/generated/.formatted/braun_tree.mli @@ -2,66 +2,67 @@ type 'a t (*@ model size: int model cont: 'a list *) -val size: 'a t -> int [@@model] -val cont: 'a t -> 'a list [@@model] - -val get: 'a t -> int -> 'a +val size : 'a t -> int [@@model] +val cont : 'a t -> 'a list [@@model] +val get : 'a t -> int -> 'a (*@ x = get t i (* requires t.cont <> [] *) ensures x = List.nth t.cont i *) -val head: 'a t -> 'a +val head : 'a t -> 'a (*@ x = head t (* requires t.cont <> [] *) ensures x = List.hd t.cont *) -val left_t: 'a t -> 'a t +val left_t : 'a t -> 'a t (*@ t' = left_t t pure (* requires t.cont <> [] *) *) -val right_t: 'a t -> 'a t +val right_t : 'a t -> 'a t (*@ t' = right_t t pure (* requires t.cont <> [] *) *) -val empty: unit -> 'a t +val empty : unit -> 'a t (** Create an empty Braun tree *) (*@ t = empty () ensures t.size = 0 ensures t.cont = [] *) -val cons: 'a -> 'a t -> 'a t +val cons : 'a -> 'a t -> 'a t (** [cons x t] returns [t] with [x] as new root. *) (*@ t' = cons x t ensures t'.size = t.size + 1 ensures List.hd t'.cont = x ensures t'.cont = x :: t.cont *) -val tail: 'a t -> 'a t -(** [tail t] removes the first element of [t] and returns the popped element and the updated Braun tree. *) +val tail : 'a t -> 'a t +(** [tail t] removes the first element of [t] and returns the popped element and + the updated Braun tree. *) (*@ t' = tail t (* requires t.cont <> [] *) ensures t.size = t'.size + 1 *) -val snoc: 'a -> 'a t -> 'a t +val snoc : 'a -> 'a t -> 'a t (** [snoc x t] returns [t] with [x] appended at the end. *) (*@ t' = snoc x t ensures t'.size = t.size + 1 ensures List.hd t'.cont = List.hd t.cont ensures List.rev t'.cont = x :: List.rev t.cont *) -val liat: 'a t -> 'a t -(** [tail t] removes the last element of [t] and returns the popped element and the updated Braun tree. *) +val liat : 'a t -> 'a t +(** [tail t] removes the last element of [t] and returns the popped element and + the updated Braun tree. *) (*@ t' = liat t (* requires t.cont <> [] *) ensures t.size = t'.size + 1 *) -val to_list: 'a t -> 'a list -val of_list: 'a list -> 'a t +val to_list : 'a t -> 'a list +val of_list : 'a list -> 'a t (* val find: int -> 'a t -> 'a (** [find n t] returns the value at index [n]. *) File "plugins/wrapper/test/generated/test.ml", line 1, characters 0-0: diff --git a/_build/default/plugins/wrapper/test/generated/test.ml b/_build/default/plugins/wrapper/test/generated/.formatted/test.ml index 72de7a8..a3f5160 100644 --- a/_build/default/plugins/wrapper/test/generated/test.ml +++ b/_build/default/plugins/wrapper/test/generated/.formatted/test.ml @@ -102,13 +102,12 @@ let add_model () = To_test3.add s 2; To_test3.add s 3 - let pp t = List.iter (fun e -> Format.printf "[%d]" e) (Braun.cont t); Format.printf "@." let braun_tree () = - let b = Braun.of_list [1;2;3;4] in + let b = Braun.of_list [ 1; 2; 3; 4 ] in let b = Braun.cons 0 b in let b = Braun.snoc 5 b in let b = Braun.tail b in File "examples/braun_tree.mli", line 1, characters 0-0: diff --git a/_build/default/examples/braun_tree.mli b/_build/default/examples/.formatted/braun_tree.mli index a91c789..c0b0559 100644 --- a/_build/default/examples/braun_tree.mli +++ b/_build/default/examples/.formatted/braun_tree.mli @@ -2,42 +2,44 @@ type 'a t (*@ model size: int model cont: 'a list *) -val size: 'a t -> int [@@model] -val cont: 'a t -> 'a list [@@model] +val size : 'a t -> int [@@model] +val cont : 'a t -> 'a list [@@model] -val empty: unit -> 'a t +val empty : unit -> 'a t (** Create an empty Braun tree *) (*@ t = empty () ensures t.size = 0 ensures t.cont = [] *) -val add_front: 'a -> 'a t -> 'a t +val add_front : 'a -> 'a t -> 'a t (** [add_front x t] returns [t] with [x] as new root. *) (*@ t' = add_front x t ensures t'.size = t.size + 1 ensures t'.cont = x :: t.cont *) -val remove_first: 'a t -> 'a * 'a t -(** [remove_first t] removes the first element of [t] and returns the popped element and the updated Braun tree. *) +val remove_first : 'a t -> 'a * 'a t +(** [remove_first t] removes the first element of [t] and returns the popped + element and the updated Braun tree. *) (*@ x, t' = remove_first t requires t.cont <> [] ensures t.size = t'.size + 1 ensures t.cont = x :: t'.cont *) -val append: 'a -> 'a t -> 'a t +val append : 'a -> 'a t -> 'a t (** [append x t] returns [t] with [x] appended at the end. *) (*@ t' = append x t ensures t'.size = t.size + 1 ensures List.rev t'.cont = x :: List.rev t.cont *) -val remove_last: 'a t -> 'a * 'a t -(** [remove_first t] removes the last element of [t] and returns the popped element and the updated Braun tree. *) +val remove_last : 'a t -> 'a * 'a t +(** [remove_first t] removes the last element of [t] and returns the popped + element and the updated Braun tree. *) (*@ x, t' = remove_last t requires t.cont <> [] ensures t.size = t'.size + 1 ensures List.rev t.cont = x :: List.rev t'.cont *) -val find: int -> 'a t -> 'a +val find : int -> 'a t -> 'a (** [find n t] returns the value at index [n]. *) (*@ x = find i t pure File "examples/braun_tree.ml", line 1, characters 0-0: diff --git a/_build/default/examples/braun_tree.ml b/_build/default/examples/.formatted/braun_tree.ml index a2b3892..5b98526 100644 --- a/_build/default/examples/braun_tree.ml +++ b/_build/default/examples/.formatted/braun_tree.ml @@ -2,29 +2,23 @@ type 'a t = Empty | Tree of 'a t * 'a * 'a t let empty = Empty -let rec diff t n = match t, n with +let rec diff t n = + match (t, n) with | Empty, 0 -> 0 | Tree _, 0 -> 1 - | Tree (l, x, r), n when n mod 2 = 1 -> diff l ((n-1)/2) - | Tree (l, x, r), n when n mod 2 = 0 -> diff r ((n-2)/2) - | _ , _ -> failwith "No more cases" + | Tree (l, x, r), n when n mod 2 = 1 -> diff l ((n - 1) / 2) + | Tree (l, x, r), n when n mod 2 = 0 -> diff r ((n - 2) / 2) + | _, _ -> failwith "No more cases" let rec size = function | Empty -> 0 | Tree (l, x, r) -> - let m = size r in - 1 + 2 * m + diff l m + let m = size r in + 1 + (2 * m) + diff l m -let head = function - | Empty -> failwith "No head" - | Tree (_, x, _) -> x - -let left_t = function - | Empty -> failwith "No left tree" - | Tree (l, _, _) -> l -let right_t = function - | Empty -> failwith "No right tree" - | Tree (_, _, r) -> r +let head = function Empty -> failwith "No head" | Tree (_, x, _) -> x +let left_t = function Empty -> failwith "No left tree" | Tree (l, _, _) -> l +let right_t = function Empty -> failwith "No right tree" | Tree (_, _, r) -> r let rec add_front x = function | Empty -> Tree (Empty, x, Empty) @@ -32,39 +26,36 @@ let rec add_front x = function let rec remove_first = function | Empty -> failwith "Already empty" - | Tree (l, n, r) when l = Empty -> n, Empty + | Tree (l, n, r) when l = Empty -> (n, Empty) | Tree (l, n, r) -> - let x, l = remove_first l in - n, Tree (r, x, l) + let x, l = remove_first l in + (n, Tree (r, x, l)) -let rec append x t = match t with +let rec append x t = + match t with | Empty -> Tree (Empty, x, Empty) - | Tree (l, _, r) -> - if size t mod 2 = 0 - then append x r - else append x l + | Tree (l, _, r) -> if size t mod 2 = 0 then append x r else append x l -let rec remove_last t = match t with +let rec remove_last t = + match t with | Empty -> failwith "Already empty" - | Tree (l, n, r) when l = Empty -> n, Empty - | Tree (l, n, r) -> - if size t mod 2 = 0 - then remove_last l - else remove_last r + | Tree (l, n, r) when l = Empty -> (n, Empty) + | Tree (l, n, r) -> if size t mod 2 = 0 then remove_last l else remove_last r -let rec find i t = if t = Empty then failwith "Empty"; +let rec find i t = + if t = Empty then failwith "Empty"; if i = 0 then head t; - if i mod 2 <> 0 - then find ((i - 1) / 2) (left_t t) + if i mod 2 <> 0 then find ((i - 1) / 2) (left_t t) else find ((i / 2) - 1) (right_t t) let cont x t = - let rec aux acc t = match t with - | Empty -> acc - | Tree (Empty, x, _) -> x :: acc - | Tree (l, x, Empty) -> aux (x :: acc) l - | Tree (l, x, r) -> - let _, nt = remove_first t in - aux (x :: acc) nt + let rec aux acc t = + match t with + | Empty -> acc + | Tree (Empty, x, _) -> x :: acc + | Tree (l, x, Empty) -> aux (x :: acc) l + | Tree (l, x, r) -> + let _, nt = remove_first t in + aux (x :: acc) nt in aux [] t File "examples/braun_rac.ml", line 1, characters 0-0: diff --git a/_build/default/examples/braun_rac.ml b/_build/default/examples/.formatted/braun_rac.ml index 7d47872..bb40dcb 100644 --- a/_build/default/examples/braun_rac.ml +++ b/_build/default/examples/.formatted/braun_rac.ml @@ -1,5 +1,6 @@ include Braun_tree module Ortac_runtime = Ortac_runtime + let size __arg0 = let __error__001_ = Ortac_runtime.Errors.create @@ -9,28 +10,33 @@ let size __arg0 = pos_fname = "braun_tree.mli"; pos_lnum = 5; pos_bol = 158; - pos_cnum = 158 + pos_cnum = 158; }; Ortac_runtime.stop = { pos_fname = "braun_tree.mli"; pos_lnum = 5; pos_bol = 158; - pos_cnum = 193 - } - } "size" in + pos_cnum = 193; + }; + } + "size" + in + Ortac_runtime.Errors.report __error__001_; + let result = + try size __arg0 with + | (Stack_overflow | Out_of_memory) as e -> + Ortac_runtime.Errors.report __error__001_; + raise e + | e -> + Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e } + |> Ortac_runtime.Errors.register __error__001_; + Ortac_runtime.Errors.report __error__001_; + raise e + in Ortac_runtime.Errors.report __error__001_; - (let result = - try size __arg0 - with - | Stack_overflow | Out_of_memory as e -> - (Ortac_runtime.Errors.report __error__001_; raise e) - | e -> - ((Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e }) - |> (Ortac_runtime.Errors.register __error__001_); - Ortac_runtime.Errors.report __error__001_; - raise e) in - Ortac_runtime.Errors.report __error__001_; result) + result + let cont __arg0_1 = let __error__002_ = Ortac_runtime.Errors.create @@ -40,28 +46,33 @@ let cont __arg0_1 = pos_fname = "braun_tree.mli"; pos_lnum = 6; pos_bol = 194; - pos_cnum = 194 + pos_cnum = 194; }; Ortac_runtime.stop = { pos_fname = "braun_tree.mli"; pos_lnum = 6; pos_bol = 194; - pos_cnum = 229 - } - } "cont" in + pos_cnum = 229; + }; + } + "cont" + in + Ortac_runtime.Errors.report __error__002_; + let result_1 = + try cont __arg0_1 with + | (Stack_overflow | Out_of_memory) as e -> + Ortac_runtime.Errors.report __error__002_; + raise e + | e -> + Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e } + |> Ortac_runtime.Errors.register __error__002_; + Ortac_runtime.Errors.report __error__002_; + raise e + in Ortac_runtime.Errors.report __error__002_; - (let result_1 = - try cont __arg0_1 - with - | Stack_overflow | Out_of_memory as e -> - (Ortac_runtime.Errors.report __error__002_; raise e) - | e -> - ((Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e }) - |> (Ortac_runtime.Errors.register __error__002_); - Ortac_runtime.Errors.report __error__002_; - raise e) in - Ortac_runtime.Errors.report __error__002_; result_1) + result_1 + let empty () = let __error__003_ = Ortac_runtime.Errors.create @@ -71,57 +82,57 @@ let empty () = pos_fname = "braun_tree.mli"; pos_lnum = 8; pos_bol = 231; - pos_cnum = 231 + pos_cnum = 231; }; Ortac_runtime.stop = { pos_fname = "braun_tree.mli"; pos_lnum = 12; pos_bol = 499; - pos_cnum = 525 - } - } "empty" in + pos_cnum = 525; + }; + } + "empty" + in Ortac_runtime.Errors.report __error__003_; - (let t_1 = - try empty () - with - | Stack_overflow | Out_of_memory as e -> - (Ortac_runtime.Errors.report __error__003_; raise e) - | e -> - ((Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e }) - |> (Ortac_runtime.Errors.register __error__003_); - Ortac_runtime.Errors.report __error__003_; - raise e) in - if - not - (try t_1.cont = [] - with - | e -> - ((Ortac_runtime.Specification_failure - { term = "t.cont = []"; term_kind = Post; exn = e }) - |> (Ortac_runtime.Errors.register __error__003_); - true)) - then - (Ortac_runtime.Violated_condition - { term = "t.cont = []"; term_kind = Post }) - |> (Ortac_runtime.Errors.register __error__003_); - if - not - (try - (Ortac_runtime.Gospelstdlib.integer_of_int t_1.size) = - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - with - | e -> - ((Ortac_runtime.Specification_failure - { term = "t.size = 0"; term_kind = Post; exn = e }) - |> (Ortac_runtime.Errors.register __error__003_); - true)) - then - (Ortac_runtime.Violated_condition - { term = "t.size = 0"; term_kind = Post }) - |> (Ortac_runtime.Errors.register __error__003_); - Ortac_runtime.Errors.report __error__003_; - t_1) + let t_1 = + try empty () with + | (Stack_overflow | Out_of_memory) as e -> + Ortac_runtime.Errors.report __error__003_; + raise e + | e -> + Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e } + |> Ortac_runtime.Errors.register __error__003_; + Ortac_runtime.Errors.report __error__003_; + raise e + in + if + not + (try t_1.cont = [] + with e -> + Ortac_runtime.Specification_failure + { term = "t.cont = []"; term_kind = Post; exn = e } + |> Ortac_runtime.Errors.register __error__003_; + true) + then + Ortac_runtime.Violated_condition { term = "t.cont = []"; term_kind = Post } + |> Ortac_runtime.Errors.register __error__003_; + if + not + (try + Ortac_runtime.Gospelstdlib.integer_of_int t_1.size + = Ortac_runtime.Gospelstdlib.integer_of_int 0 + with e -> + Ortac_runtime.Specification_failure + { term = "t.size = 0"; term_kind = Post; exn = e } + |> Ortac_runtime.Errors.register __error__003_; + true) + then + Ortac_runtime.Violated_condition { term = "t.size = 0"; term_kind = Post } + |> Ortac_runtime.Errors.register __error__003_; + Ortac_runtime.Errors.report __error__003_; + t_1 + let add_front x t_2 = let __error__004_ = Ortac_runtime.Errors.create @@ -131,59 +142,61 @@ let add_front x t_2 = pos_fname = "braun_tree.mli"; pos_lnum = 14; pos_bol = 527; - pos_cnum = 527 + pos_cnum = 527; }; Ortac_runtime.stop = { pos_fname = "braun_tree.mli"; pos_lnum = 18; pos_bol = 879; - pos_cnum = 915 - } - } "add_front" in + pos_cnum = 915; + }; + } + "add_front" + in Ortac_runtime.Errors.report __error__004_; - (let t' = - try add_front x t_2 - with - | Stack_overflow | Out_of_memory as e -> - (Ortac_runtime.Errors.report __error__004_; raise e) - | e -> - ((Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e }) - |> (Ortac_runtime.Errors.register __error__004_); - Ortac_runtime.Errors.report __error__004_; - raise e) in - if - not - (try t'.cont = (x :: t_2.cont) - with - | e -> - ((Ortac_runtime.Specification_failure - { term = "t'.cont = x :: t.cont"; term_kind = Post; exn = e }) - |> (Ortac_runtime.Errors.register __error__004_); - true)) - then - (Ortac_runtime.Violated_condition - { term = "t'.cont = x :: t.cont"; term_kind = Post }) - |> (Ortac_runtime.Errors.register __error__004_); - if - not - (try - (Ortac_runtime.Gospelstdlib.integer_of_int t'.size) = - (Ortac_runtime.Gospelstdlib.(+) - (Ortac_runtime.Gospelstdlib.integer_of_int t_2.size) - (Ortac_runtime.Gospelstdlib.integer_of_int 1)) - with - | e -> - ((Ortac_runtime.Specification_failure - { term = "t'.size = t.size + 1"; term_kind = Post; exn = e }) - |> (Ortac_runtime.Errors.register __error__004_); - true)) - then - (Ortac_runtime.Violated_condition - { term = "t'.size = t.size + 1"; term_kind = Post }) - |> (Ortac_runtime.Errors.register __error__004_); - Ortac_runtime.Errors.report __error__004_; - t') + let t' = + try add_front x t_2 with + | (Stack_overflow | Out_of_memory) as e -> + Ortac_runtime.Errors.report __error__004_; + raise e + | e -> + Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e } + |> Ortac_runtime.Errors.register __error__004_; + Ortac_runtime.Errors.report __error__004_; + raise e + in + if + not + (try t'.cont = x :: t_2.cont + with e -> + Ortac_runtime.Specification_failure + { term = "t'.cont = x :: t.cont"; term_kind = Post; exn = e } + |> Ortac_runtime.Errors.register __error__004_; + true) + then + Ortac_runtime.Violated_condition + { term = "t'.cont = x :: t.cont"; term_kind = Post } + |> Ortac_runtime.Errors.register __error__004_; + if + not + (try + Ortac_runtime.Gospelstdlib.integer_of_int t'.size + = Ortac_runtime.Gospelstdlib.( + ) + (Ortac_runtime.Gospelstdlib.integer_of_int t_2.size) + (Ortac_runtime.Gospelstdlib.integer_of_int 1) + with e -> + Ortac_runtime.Specification_failure + { term = "t'.size = t.size + 1"; term_kind = Post; exn = e } + |> Ortac_runtime.Errors.register __error__004_; + true) + then + Ortac_runtime.Violated_condition + { term = "t'.size = t.size + 1"; term_kind = Post } + |> Ortac_runtime.Errors.register __error__004_; + Ortac_runtime.Errors.report __error__004_; + t' + let remove_first t_3 = let __error__005_ = Ortac_runtime.Errors.create @@ -193,72 +206,72 @@ let remove_first t_3 = pos_fname = "braun_tree.mli"; pos_lnum = 20; pos_bol = 917; - pos_cnum = 917 + pos_cnum = 917; }; Ortac_runtime.stop = { pos_fname = "braun_tree.mli"; pos_lnum = 25; pos_bol = 1419; - pos_cnum = 1455 - } - } "remove_first" in + pos_cnum = 1455; + }; + } + "remove_first" + in if not (try not (t_3.cont = []) - with - | e -> - ((Ortac_runtime.Specification_failure - { term = "t.cont <> []"; term_kind = Pre; exn = e }) - |> (Ortac_runtime.Errors.register __error__005_); - true)) + with e -> + Ortac_runtime.Specification_failure + { term = "t.cont <> []"; term_kind = Pre; exn = e } + |> Ortac_runtime.Errors.register __error__005_; + true) then - (Ortac_runtime.Violated_condition - { term = "t.cont <> []"; term_kind = Pre }) - |> (Ortac_runtime.Errors.register __error__005_); + Ortac_runtime.Violated_condition { term = "t.cont <> []"; term_kind = Pre } + |> Ortac_runtime.Errors.register __error__005_; Ortac_runtime.Errors.report __error__005_; - (let (x_1, t'_1) = - try remove_first t_3 - with - | Stack_overflow | Out_of_memory as e -> - (Ortac_runtime.Errors.report __error__005_; raise e) - | e -> - ((Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e }) - |> (Ortac_runtime.Errors.register __error__005_); - Ortac_runtime.Errors.report __error__005_; - raise e) in - if - not - (try t_3.cont = (x_1 :: t'_1.cont) - with - | e -> - ((Ortac_runtime.Specification_failure - { term = "t.cont = x :: t'.cont"; term_kind = Post; exn = e }) - |> (Ortac_runtime.Errors.register __error__005_); - true)) - then - (Ortac_runtime.Violated_condition - { term = "t.cont = x :: t'.cont"; term_kind = Post }) - |> (Ortac_runtime.Errors.register __error__005_); - if - not - (try - (Ortac_runtime.Gospelstdlib.integer_of_int t_3.size) = - (Ortac_runtime.Gospelstdlib.(+) - (Ortac_runtime.Gospelstdlib.integer_of_int t'_1.size) - (Ortac_runtime.Gospelstdlib.integer_of_int 1)) - with - | e -> - ((Ortac_runtime.Specification_failure - { term = "t.size = t'.size + 1"; term_kind = Post; exn = e }) - |> (Ortac_runtime.Errors.register __error__005_); - true)) - then - (Ortac_runtime.Violated_condition - { term = "t.size = t'.size + 1"; term_kind = Post }) - |> (Ortac_runtime.Errors.register __error__005_); - Ortac_runtime.Errors.report __error__005_; - (x_1, t'_1)) + let x_1, t'_1 = + try remove_first t_3 with + | (Stack_overflow | Out_of_memory) as e -> + Ortac_runtime.Errors.report __error__005_; + raise e + | e -> + Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e } + |> Ortac_runtime.Errors.register __error__005_; + Ortac_runtime.Errors.report __error__005_; + raise e + in + if + not + (try t_3.cont = x_1 :: t'_1.cont + with e -> + Ortac_runtime.Specification_failure + { term = "t.cont = x :: t'.cont"; term_kind = Post; exn = e } + |> Ortac_runtime.Errors.register __error__005_; + true) + then + Ortac_runtime.Violated_condition + { term = "t.cont = x :: t'.cont"; term_kind = Post } + |> Ortac_runtime.Errors.register __error__005_; + if + not + (try + Ortac_runtime.Gospelstdlib.integer_of_int t_3.size + = Ortac_runtime.Gospelstdlib.( + ) + (Ortac_runtime.Gospelstdlib.integer_of_int t'_1.size) + (Ortac_runtime.Gospelstdlib.integer_of_int 1) + with e -> + Ortac_runtime.Specification_failure + { term = "t.size = t'.size + 1"; term_kind = Post; exn = e } + |> Ortac_runtime.Errors.register __error__005_; + true) + then + Ortac_runtime.Violated_condition + { term = "t.size = t'.size + 1"; term_kind = Post } + |> Ortac_runtime.Errors.register __error__005_; + Ortac_runtime.Errors.report __error__005_; + (x_1, t'_1) + let append x_2 t_4 = let __error__006_ = Ortac_runtime.Errors.create @@ -268,66 +281,67 @@ let append x_2 t_4 = pos_fname = "braun_tree.mli"; pos_lnum = 27; pos_bol = 1457; - pos_cnum = 1457 + pos_cnum = 1457; }; Ortac_runtime.stop = { pos_fname = "braun_tree.mli"; pos_lnum = 31; pos_bol = 1831; - pos_cnum = 1885 - } - } "append" in + pos_cnum = 1885; + }; + } + "append" + in + Ortac_runtime.Errors.report __error__006_; + let t'_2 = + try append x_2 t_4 with + | (Stack_overflow | Out_of_memory) as e -> + Ortac_runtime.Errors.report __error__006_; + raise e + | e -> + Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e } + |> Ortac_runtime.Errors.register __error__006_; + Ortac_runtime.Errors.report __error__006_; + raise e + in + if + not + (try + Ortac_runtime.Gospelstdlib.List.rev t'_2.cont + = x_2 :: Ortac_runtime.Gospelstdlib.List.rev t_4.cont + with e -> + Ortac_runtime.Specification_failure + { + term = "List.rev t'.cont = x :: List.rev t.cont"; + term_kind = Post; + exn = e; + } + |> Ortac_runtime.Errors.register __error__006_; + true) + then + Ortac_runtime.Violated_condition + { term = "List.rev t'.cont = x :: List.rev t.cont"; term_kind = Post } + |> Ortac_runtime.Errors.register __error__006_; + if + not + (try + Ortac_runtime.Gospelstdlib.integer_of_int t'_2.size + = Ortac_runtime.Gospelstdlib.( + ) + (Ortac_runtime.Gospelstdlib.integer_of_int t_4.size) + (Ortac_runtime.Gospelstdlib.integer_of_int 1) + with e -> + Ortac_runtime.Specification_failure + { term = "t'.size = t.size + 1"; term_kind = Post; exn = e } + |> Ortac_runtime.Errors.register __error__006_; + true) + then + Ortac_runtime.Violated_condition + { term = "t'.size = t.size + 1"; term_kind = Post } + |> Ortac_runtime.Errors.register __error__006_; Ortac_runtime.Errors.report __error__006_; - (let t'_2 = - try append x_2 t_4 - with - | Stack_overflow | Out_of_memory as e -> - (Ortac_runtime.Errors.report __error__006_; raise e) - | e -> - ((Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e }) - |> (Ortac_runtime.Errors.register __error__006_); - Ortac_runtime.Errors.report __error__006_; - raise e) in - if - not - (try - (Ortac_runtime.Gospelstdlib.List.rev t'_2.cont) = - (x_2 :: (Ortac_runtime.Gospelstdlib.List.rev t_4.cont)) - with - | e -> - ((Ortac_runtime.Specification_failure - { - term = "List.rev t'.cont = x :: List.rev t.cont"; - term_kind = Post; - exn = e - }) - |> (Ortac_runtime.Errors.register __error__006_); - true)) - then - (Ortac_runtime.Violated_condition - { term = "List.rev t'.cont = x :: List.rev t.cont"; term_kind = Post - }) - |> (Ortac_runtime.Errors.register __error__006_); - if - not - (try - (Ortac_runtime.Gospelstdlib.integer_of_int t'_2.size) = - (Ortac_runtime.Gospelstdlib.(+) - (Ortac_runtime.Gospelstdlib.integer_of_int t_4.size) - (Ortac_runtime.Gospelstdlib.integer_of_int 1)) - with - | e -> - ((Ortac_runtime.Specification_failure - { term = "t'.size = t.size + 1"; term_kind = Post; exn = e }) - |> (Ortac_runtime.Errors.register __error__006_); - true)) - then - (Ortac_runtime.Violated_condition - { term = "t'.size = t.size + 1"; term_kind = Post }) - |> (Ortac_runtime.Errors.register __error__006_); - Ortac_runtime.Errors.report __error__006_; - t'_2) + t'_2 + let remove_last t_5 = let __error__007_ = Ortac_runtime.Errors.create @@ -337,79 +351,78 @@ let remove_last t_5 = pos_fname = "braun_tree.mli"; pos_lnum = 33; pos_bol = 1887; - pos_cnum = 1887 + pos_cnum = 1887; }; Ortac_runtime.stop = { pos_fname = "braun_tree.mli"; pos_lnum = 38; pos_bol = 2403; - pos_cnum = 2457 - } - } "remove_last" in + pos_cnum = 2457; + }; + } + "remove_last" + in if not (try not (t_5.cont = []) - with - | e -> - ((Ortac_runtime.Specification_failure - { term = "t.cont <> []"; term_kind = Pre; exn = e }) - |> (Ortac_runtime.Errors.register __error__007_); - true)) + with e -> + Ortac_runtime.Specification_failure + { term = "t.cont <> []"; term_kind = Pre; exn = e } + |> Ortac_runtime.Errors.register __error__007_; + true) + then + Ortac_runtime.Violated_condition { term = "t.cont <> []"; term_kind = Pre } + |> Ortac_runtime.Errors.register __error__007_; + Ortac_runtime.Errors.report __error__007_; + let x_3, t'_3 = + try remove_last t_5 with + | (Stack_overflow | Out_of_memory) as e -> + Ortac_runtime.Errors.report __error__007_; + raise e + | e -> + Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e } + |> Ortac_runtime.Errors.register __error__007_; + Ortac_runtime.Errors.report __error__007_; + raise e + in + if + not + (try + Ortac_runtime.Gospelstdlib.List.rev t_5.cont + = x_3 :: Ortac_runtime.Gospelstdlib.List.rev t'_3.cont + with e -> + Ortac_runtime.Specification_failure + { + term = "List.rev t.cont = x :: List.rev t'.cont"; + term_kind = Post; + exn = e; + } + |> Ortac_runtime.Errors.register __error__007_; + true) + then + Ortac_runtime.Violated_condition + { term = "List.rev t.cont = x :: List.rev t'.cont"; term_kind = Post } + |> Ortac_runtime.Errors.register __error__007_; + if + not + (try + Ortac_runtime.Gospelstdlib.integer_of_int t_5.size + = Ortac_runtime.Gospelstdlib.( + ) + (Ortac_runtime.Gospelstdlib.integer_of_int t'_3.size) + (Ortac_runtime.Gospelstdlib.integer_of_int 1) + with e -> + Ortac_runtime.Specification_failure + { term = "t.size = t'.size + 1"; term_kind = Post; exn = e } + |> Ortac_runtime.Errors.register __error__007_; + true) then - (Ortac_runtime.Violated_condition - { term = "t.cont <> []"; term_kind = Pre }) - |> (Ortac_runtime.Errors.register __error__007_); + Ortac_runtime.Violated_condition + { term = "t.size = t'.size + 1"; term_kind = Post } + |> Ortac_runtime.Errors.register __error__007_; Ortac_runtime.Errors.report __error__007_; - (let (x_3, t'_3) = - try remove_last t_5 - with - | Stack_overflow | Out_of_memory as e -> - (Ortac_runtime.Errors.report __error__007_; raise e) - | e -> - ((Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e }) - |> (Ortac_runtime.Errors.register __error__007_); - Ortac_runtime.Errors.report __error__007_; - raise e) in - if - not - (try - (Ortac_runtime.Gospelstdlib.List.rev t_5.cont) = - (x_3 :: (Ortac_runtime.Gospelstdlib.List.rev t'_3.cont)) - with - | e -> - ((Ortac_runtime.Specification_failure - { - term = "List.rev t.cont = x :: List.rev t'.cont"; - term_kind = Post; - exn = e - }) - |> (Ortac_runtime.Errors.register __error__007_); - true)) - then - (Ortac_runtime.Violated_condition - { term = "List.rev t.cont = x :: List.rev t'.cont"; term_kind = Post - }) - |> (Ortac_runtime.Errors.register __error__007_); - if - not - (try - (Ortac_runtime.Gospelstdlib.integer_of_int t_5.size) = - (Ortac_runtime.Gospelstdlib.(+) - (Ortac_runtime.Gospelstdlib.integer_of_int t'_3.size) - (Ortac_runtime.Gospelstdlib.integer_of_int 1)) - with - | e -> - ((Ortac_runtime.Specification_failure - { term = "t.size = t'.size + 1"; term_kind = Post; exn = e }) - |> (Ortac_runtime.Errors.register __error__007_); - true)) - then - (Ortac_runtime.Violated_condition - { term = "t.size = t'.size + 1"; term_kind = Post }) - |> (Ortac_runtime.Errors.register __error__007_); - Ortac_runtime.Errors.report __error__007_; - (x_3, t'_3)) + (x_3, t'_3) + let find i t_6 = let __error__008_ = Ortac_runtime.Errors.create @@ -419,58 +432,58 @@ let find i t_6 = pos_fname = "braun_tree.mli"; pos_lnum = 40; pos_bol = 2459; - pos_cnum = 2459 + pos_cnum = 2459; }; Ortac_runtime.stop = { pos_fname = "braun_tree.mli"; pos_lnum = 45; pos_bol = 2785; - pos_cnum = 2821 - } - } "find" in + pos_cnum = 2821; + }; + } + "find" + in if not (try - Ortac_runtime.Gospelstdlib.(<) + Ortac_runtime.Gospelstdlib.( < ) (Ortac_runtime.Gospelstdlib.integer_of_int i) (Ortac_runtime.Gospelstdlib.integer_of_int t_6.size) - with - | e -> - ((Ortac_runtime.Specification_failure - { term = "i < t.size"; term_kind = Pre; exn = e }) - |> (Ortac_runtime.Errors.register __error__008_); - true)) + with e -> + Ortac_runtime.Specification_failure + { term = "i < t.size"; term_kind = Pre; exn = e } + |> Ortac_runtime.Errors.register __error__008_; + true) + then + Ortac_runtime.Violated_condition { term = "i < t.size"; term_kind = Pre } + |> Ortac_runtime.Errors.register __error__008_; + Ortac_runtime.Errors.report __error__008_; + let x_4 = + try find i t_6 with + | (Stack_overflow | Out_of_memory) as e -> + Ortac_runtime.Errors.report __error__008_; + raise e + | e -> + Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e } + |> Ortac_runtime.Errors.register __error__008_; + Ortac_runtime.Errors.report __error__008_; + raise e + in + if + not + (try + x_4 + = Ortac_runtime.Gospelstdlib.List.nth t_6.cont + (Ortac_runtime.Gospelstdlib.integer_of_int i) + with e -> + Ortac_runtime.Specification_failure + { term = "x = List.nth t.cont i"; term_kind = Post; exn = e } + |> Ortac_runtime.Errors.register __error__008_; + true) then - (Ortac_runtime.Violated_condition - { term = "i < t.size"; term_kind = Pre }) - |> (Ortac_runtime.Errors.register __error__008_); + Ortac_runtime.Violated_condition + { term = "x = List.nth t.cont i"; term_kind = Post } + |> Ortac_runtime.Errors.register __error__008_; Ortac_runtime.Errors.report __error__008_; - (let x_4 = - try find i t_6 - with - | Stack_overflow | Out_of_memory as e -> - (Ortac_runtime.Errors.report __error__008_; raise e) - | e -> - ((Ortac_runtime.Unexpected_exception { allowed_exn = []; exn = e }) - |> (Ortac_runtime.Errors.register __error__008_); - Ortac_runtime.Errors.report __error__008_; - raise e) in - if - not - (try - x_4 = - (Ortac_runtime.Gospelstdlib.List.nth t_6.cont - (Ortac_runtime.Gospelstdlib.integer_of_int i)) - with - | e -> - ((Ortac_runtime.Specification_failure - { term = "x = List.nth t.cont i"; term_kind = Post; exn = e }) - |> (Ortac_runtime.Errors.register __error__008_); - true)) - then - (Ortac_runtime.Violated_condition - { term = "x = List.nth t.cont i"; term_kind = Post }) - |> (Ortac_runtime.Errors.register __error__008_); - Ortac_runtime.Errors.report __error__008_; - x_4) + x_4 dune build @fmt failed "/usr/bin/env" "bash" "-c" "opam exec -- dune build @fmt --ignore-promoted-rules || (echo "dune build @fmt failed"; exit 2)" failed with exit status 2 2025-05-23 09:49.04: Job failed: Failed: Build failed