Organisationsocaml-gospelcameleerdee290 ()(lint-fmt)

(lint-fmt)

Link Copied
Code Copied

Logs

2024-04-23 18:03.49: New job: test ocaml-gospel/cameleer https://github.com/ocaml-gospel/cameleer.git#refs/heads/master (dee290857643f861e5fe53cb327dbffe772c3f41) (linux-x86_64:(lint-fmt))
Base: ocaml/opam@sha256:e30e92a245a5f284471a3437bd6b19ebfb9ae067e380416fd178b1f6c2290480
ocamlformat version: version 0.24.1 (from opam)


To reproduce locally:


git clone --recursive "https://github.com/ocaml-gospel/cameleer.git" -b "master" && cd "cameleer" && git reset --hard dee29085
cat > Dockerfile <<'END-OF-DOCKERFILE'
FROM ocaml/opam@sha256:e30e92a245a5f284471a3437bd6b19ebfb9ae067e380416fd178b1f6c2290480
USER 1000:1000
RUN cd ~/opam-repository && (git cat-file -e 950c52962d34ab7507ecebe8cc7ef16fed0f292a || git fetch origin master) && git reset -q --hard 950c52962d34ab7507ecebe8cc7ef16fed0f292a && git log --no-decorate -n1 --oneline && opam update -u
RUN opam depext -i dune
WORKDIR /src
RUN opam depext -i ocamlformat=0.24.1
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


2024-04-23 18:03.49: Using cache hint "ocaml-gospel/cameleer-ocaml/opam@sha256:e30e92a245a5f284471a3437bd6b19ebfb9ae067e380416fd178b1f6c2290480-debian-12-4.08_opam-2.1-ocamlformat-950c52962d34ab7507ecebe8cc7ef16fed0f292a"
2024-04-23 18:03.49: Using OBuilder spec:
((from ocaml/opam@sha256:e30e92a245a5f284471a3437bd6b19ebfb9ae067e380416fd178b1f6c2290480)
 (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 950c52962d34ab7507ecebe8cc7ef16fed0f292a || git fetch origin master) && git reset -q --hard 950c52962d34ab7507ecebe8cc7ef16fed0f292a && 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.24.1"))
 (copy (src .) (dst /src/))
 (run (shell "opam exec -- dune build @fmt --ignore-promoted-rules || (echo \"dune build @fmt failed\"; exit 2)"))
)


2024-04-23 18:03.49: Waiting for resource in pool OCluster
2024-04-23 18:03.49: Waiting for worker…
2024-04-23 18:04.42: Got resource from pool OCluster
Building on x86-bm-c15.sw.ocaml.org
HEAD is now at 94f92ba Session updates
HEAD is now at dee2908 Session updates and cosmetic changes in several examples.


(from ocaml/opam@sha256:e30e92a245a5f284471a3437bd6b19ebfb9ae067e380416fd178b1f6c2290480)
2024-04-23 18:05.07 ---> saved as "ca7a47bb337547622343e1e691b0c92596d0990b9ed28342fd47c7204c2b0a74"


/: (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 950c52962d34ab7507ecebe8cc7ef16fed0f292a || git fetch origin master) && git reset -q --hard 950c52962d34ab7507ecebe8cc7ef16fed0f292a && git log --no-decorate -n1 --oneline && opam update -u"))
From https://github.com/ocaml/opam-repository
 * branch                  master     -> FETCH_HEAD
   4bb8cb8b65..4399f486aa  master     -> origin/master
950c52962d [new release] dune (15 packages) (3.15.0)


<><> Updating package repositories ><><><><><><><><><><><><><><><><><><><><><><>
[default] synchronised from file:///home/opam/opam-repository
default (at file:///home/opam/opam-repository): 
    [INFO] opam 2.1 includes many performance 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
2024-04-23 18:06.31 ---> saved as "d503da00125902acd1f20be2925fe11278adbad3e0b35a554096da2f3ec05919"


/: (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.15.0


<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[dune.3.15.0] found in cache


<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> installed dune.3.15.0
Done.
# Run eval $(opam env) to update the current shell environment
2024-04-23 18:07.40 ---> saved as "053f2f263babb78e1364986dbbdff3b12925587c6fccaee354efcf5dac5b5e8d"


/: (workdir /src)


/src: (run (cache (opam-archives (target /home/opam/.opam/download-cache)))
           (network host)
           (shell "opam depext -i ocamlformat=0.24.1"))
# 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 ocamlbuild        0.14.3   [required by fpath, uuseg]
  - install menhirCST         20231231 [required by menhir]
  - install dune-build-info   3.15.0   [required by ocamlformat]
  - install either            1.0.0    [required by ocamlformat]
  - install cmdliner          1.2.0    [required by ocamlformat]
  - install menhirSdk         20231231 [required by ocamlformat]
  - install ocaml-version     3.5.0    [required by ocamlformat]
  - install ocamlfind         1.9.6    [required by ocp-indent, fpath, uuseg]
  - install menhirLib         20231231 [required by ocamlformat]
  - install result            1.5      [required by odoc-parser]
  - install seq               base     [required by re]
  - install csexp             1.5.2    [required by ocamlformat]
  - install camlp-streams     5.0.1    [required by odoc-parser]
  - install fix               20230505 [required by ocamlformat]
  - install topkg             1.0.7    [required by fpath, uuseg]
  - install base-bytes        base     [required by ocp-indent]
  - install menhir            20231231 [required by ocamlformat]
  - install re                1.11.0   [required by ocamlformat]
  - install dune-configurator 3.15.0   [required by base]
  - install uutf              1.0.3    [required by ocamlformat]
  - install astring           0.8.5    [required by fpath, odoc-parser]
  - install ocp-indent        1.8.1    [required by ocamlformat]
  - install base              v0.14.3  [required by ocamlformat]
  - install uucp              15.0.0   [required by uuseg]
  - install odoc-parser       2.0.0    [required by ocamlformat]
  - install fpath             0.7.3    [required by ocamlformat]
  - install stdio             v0.14.0  [required by ocamlformat]
  - install uuseg             15.0.0   [required by ocamlformat]
  - install ocamlformat       0.24.1
===== 30 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.2.0] found in cache
[csexp.1.5.2] found in cache
[dune-build-info.3.15.0] found in cache
[dune-configurator.3.15.0] found in cache
[either.1.0.0] found in cache
[fix.20230505] found in cache
[fpath.0.7.3] found in cache
[menhir.20231231] found in cache
[menhirCST.20231231] found in cache
[menhirLib.20231231] found in cache
[menhirSdk.20231231] found in cache
[ocaml-version.3.5.0] found in cache
[ocamlbuild.0.14.3] found in cache
[ocamlfind.1.9.6] found in cache
[ocamlformat.0.24.1] found in cache
[ocp-indent.1.8.1] found in cache
[odoc-parser.2.0.0] found in cache
[re.1.11.0] found in cache
[result.1.5] found in cache
[sexplib0.v0.14.0] found in cache
[stdio.v0.14.0] found in cache
[topkg.1.0.7] found in cache
[uucp.15.0.0] found in cache
[uuseg.15.0.0] found in cache
[uutf.1.0.3] 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.20230505
-> installed cmdliner.1.2.0
-> installed menhirCST.20231231
-> installed menhirLib.20231231
-> installed menhirSdk.20231231
-> installed ocaml-version.3.5.0
-> installed re.1.11.0
-> installed result.1.5
-> installed sexplib0.v0.14.0
-> installed dune-build-info.3.15.0
-> installed dune-configurator.3.15.0
-> installed ocamlfind.1.9.6
-> installed base-bytes.base
-> installed ocp-indent.1.8.1
-> installed ocamlbuild.0.14.3
-> installed base.v0.14.3
-> installed topkg.1.0.7
-> installed stdio.v0.14.0
-> installed uutf.1.0.3
-> installed astring.0.8.5
-> installed odoc-parser.2.0.0
-> installed fpath.0.7.3
-> installed menhir.20231231
-> installed uucp.15.0.0
-> installed uuseg.15.0.0
-> installed ocamlformat.0.24.1
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
2024-04-23 18:09.18 ---> saved as "e67f7159bfd13f525cd13a6005802695e21eb0c94824c08f5e1d88e84b52789c"


/src: (copy (src .) (dst /src/))
2024-04-23 18:09.18 ---> saved as "d98e70082aaac80e10bfad3db19daf4e5c4ba32c297c50df5eecc06da571546f"


/src: (run (shell "opam exec -- dune build @fmt --ignore-promoted-rules || (echo \"dune build @fmt failed\"; exit 2)"))
File "examples/mjrty.ml", line 1, characters 0-0:
diff --git a/_build/default/examples/mjrty.ml b/_build/default/examples/.formatted/mjrty.ml
index 03382eb..9f0df0c 100644
--- a/_build/default/examples/mjrty.ml
+++ b/_build/default/examples/.formatted/mjrty.ml
@@ -1,4 +1,3 @@
-
 (*@ function rec numof (p: integer -> bool) (a b: integer) : integer =
       if b <= a then 0 else
       if p (b - 1) then 1 + numof p a (b - 1)
@@ -45,9 +44,9 @@ module Mjrty (Eq : EQUAL) = struct
         (*@ invariant 0 <= !k <= numof_eq a !cand 0 i
             invariant 2 * (numof_eq a !cand 0 i - !k) <= i - !k
             invariant forall c. c <> !cand -> 2 * numof_eq a c 0 i <= i - !k *)
-        if !k = 0 then begin
+        if !k = 0 then (
           cand := a.(i);
-          k := 1 end
+          k := 1)
         else if Eq.eq !cand a.(i) then incr k
         else decr k
       done;
File "examples/mergesort.ml", line 1, characters 0-0:
diff --git a/_build/default/examples/mergesort.ml b/_build/default/examples/.formatted/mergesort.ml
index dd961b1..abff9aa 100644
--- a/_build/default/examples/mergesort.ml
+++ b/_build/default/examples/.formatted/mergesort.ml
@@ -63,9 +63,9 @@ module Make (E : PRE_ORD) = struct
   let rec split l =
     match l with
     | [] -> ([], [])
-    | [x] -> ([x], [])
+    | [ x ] -> ([ x ], [])
     | x :: y :: xs ->
-        let (l1, l2) = split xs in
+        let l1, l2 = split xs in
         (x :: l1, y :: l2)
   (*@ (l1, l2) = split l
         variant List.length l
File "examples/find.ml", line 1, characters 0-0:
diff --git a/_build/default/examples/find.ml b/_build/default/examples/.formatted/find.ml
index 038889c..25540c8 100644
--- a/_build/default/examples/find.ml
+++ b/_build/default/examples/.formatted/find.ml
@@ -24,13 +24,8 @@ module Make (E : EQUAL) = struct
                 | Some i -> a.(i) = x *)
 end
 
-module MakeList (E: EQUAL) = struct
+module MakeList (E : EQUAL) = struct
   type elt = E.t
 
-  let rec mem x l =
-    match l with
-    | [] -> false
-    | y :: r ->
-        E.eq x y || mem x r
-
+  let rec mem x l = match l with [] -> false | y :: r -> E.eq x y || mem x r
 end
Warning: Invalid documentation comment:
File "stdlib/setCameleer.mli", line 115, characters 7-28:
'{ x | x in s /\ p x }': bad markup.
Suggestion: did you mean '{! x | x in s /\ p x }' or '[ x | x in s /\ p x ]'?
Warning: Invalid documentation comment:
File "stdlib/setCameleer.mli", line 124, characters 7-23:
'{ f x | x in U }': bad markup.
Suggestion: did you mean '{! f x | x in U }' or '[ f x | x in U ]'?
File "examples/union_find.ml", line 1, characters 0-0:
diff --git a/_build/default/examples/union_find.ml b/_build/default/examples/.formatted/union_find.ml
index 186124c..2b39111 100644
--- a/_build/default/examples/union_find.ml
+++ b/_build/default/examples/.formatted/union_find.ml
@@ -1,4 +1,3 @@
-
 (** The following is used to prove validity of the [uf] type invariant. *)
 let[@ghost] [@logic] init () = Array.init 0 (fun x -> x)
 (*@ a = init ()
@@ -42,7 +41,7 @@ let rec find i uf =
       mem i uf.link -> mem j uf.link -> uf.rep i = uf.rep j *)
 
 let[@ghost] set (f : 'a -> 'b) (x : 'a) (v : 'b) : 'a -> 'b =
-  fun y -> if (y = x) [@pure] then v else f y
+ fun y -> if (y = x) [@pure] then v else f y
 
 let union i j uf =
   let rep_i = find i uf in
File "examples/leftist_heap.ml", line 1, characters 0-0:
diff --git a/_build/default/examples/leftist_heap.ml b/_build/default/examples/.formatted/leftist_heap.ml
index 265d1dc..22056ca 100644
--- a/_build/default/examples/leftist_heap.ml
+++ b/_build/default/examples/.formatted/leftist_heap.ml
@@ -22,7 +22,7 @@ module type S = sig
 
   type t
 
-  val[@logic] size : t -> int
+  val size : t -> int [@@logic]
   (*@ r = size t
         ensures 0 <= r *)
 
@@ -45,12 +45,12 @@ module type S = sig
 
   (*@ predicate leftist_heap (h: t) *)
 
-  val[@logic] empty : t
+  val empty : t [@@logic]
   (*@ r = empty
         ensures size r = 0
         ensures forall x. occ x r = 0 *)
 
-  val[@logic] is_empty : t -> bool
+  val is_empty : t -> bool [@@logic]
   (*@ b = is_empty t
         requires leftist_heap t
         ensures  b <-> size t = 0 *)
File "src/odecl.mli", line 1, characters 0-0:
diff --git a/_build/default/src/odecl.mli b/_build/default/src/.formatted/odecl.mli
index 22a4851..a7798b6 100644
--- a/_build/default/src/odecl.mli
+++ b/_build/default/src/.formatted/odecl.mli
@@ -52,9 +52,7 @@ val add_info : info -> string -> int -> unit
 val add_info_refinement : info -> string -> info_refinement -> unit
 val mk_function : let_function -> odecl
 val mk_dtype : Loc.position -> Ptree.type_decl list -> odecl
-
-val mk_dlogic :
-  Loc.position -> Ptree.logic_decl list -> odecl
+val mk_dlogic : Loc.position -> Ptree.logic_decl list -> odecl
 
 val mk_dprop :
   Loc.position -> Decl.prop_kind -> Ptree.ident -> Ptree.term -> odecl
File "src/declaration.ml", line 1, characters 0-0:
diff --git a/_build/default/src/declaration.ml b/_build/default/src/.formatted/declaration.ml
index f8e27fa..3f1e95b 100644
--- a/_build/default/src/declaration.ml
+++ b/_build/default/src/.formatted/declaration.ml
@@ -302,12 +302,12 @@ let function_ f =
           (ld_loc, ld_ident, f.fun_rec, binders, ld_type, dlet_spec, dlet_expr)
       in
       (fun_desc, coerc)
-  (* let coercion = *)
-  (*   match fun_spec with *)
-  (*   | None -> None *)
-  (*   | Some f -> if f.fun_coer then Some (Qident ld_ident) else None *)
-  (* in *)
-  (* ({ ld_loc; ld_ident; ld_params; ld_type; ld_def }, coercion) *)
+(* let coercion = *)
+(*   match fun_spec with *)
+(*   | None -> None *)
+(*   | Some f -> if f.fun_coer then Some (Qident ld_ident) else None *)
+(* in *)
+(* ({ ld_loc; ld_ident; ld_params; ld_type; ld_def }, coercion) *)
 
 let prop p =
   let kind =
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
2024-04-23 18:09.19: Job failed: Failed: Build failed