2024-11-05 15:13.53: New job: test ocaml-gospel/gospel https://github.com/ocaml-gospel/gospel.git#refs/pull/423/head (dcac42ee012a89ef19a1aaecdd9e6f2024abc209) (linux-x86_64:(lint-fmt)) Base: ocaml/opam:debian-12-ocaml-4.08@sha256:e4f2cf9099096504addd23b73b0d98c5a1fbb1633a6d52b7627cfa16f89debf8 ocamlformat version: version 0.26.2 (from opam) To reproduce locally: git clone --recursive "https://github.com/ocaml-gospel/gospel.git" && cd "gospel" && git fetch origin "refs/pull/423/head" && git reset --hard dcac42ee cat > Dockerfile <<'END-OF-DOCKERFILE' FROM ocaml/opam:debian-12-ocaml-4.08@sha256:e4f2cf9099096504addd23b73b0d98c5a1fbb1633a6d52b7627cfa16f89debf8 USER 1000:1000 RUN cd ~/opam-repository && (git cat-file -e 654ee104df48ee785861d169cd1ca7eba64b6668 || git fetch origin master) && git reset -q --hard 654ee104df48ee785861d169cd1ca7eba64b6668 && git log --no-decorate -n1 --oneline && opam update -u RUN opam depext -i dune WORKDIR /src RUN opam depext -i ocamlformat=0.26.2 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-11-05 15:13.53: Using cache hint "ocaml-gospel/gospel-ocaml/opam:debian-12-ocaml-4.08@sha256:e4f2cf9099096504addd23b73b0d98c5a1fbb1633a6d52b7627cfa16f89debf8-debian-12-4.08_opam-2.2-ocamlformat-654ee104df48ee785861d169cd1ca7eba64b6668" 2024-11-05 15:13.53: Using OBuilder spec: ((from ocaml/opam:debian-12-ocaml-4.08@sha256:e4f2cf9099096504addd23b73b0d98c5a1fbb1633a6d52b7627cfa16f89debf8) (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 654ee104df48ee785861d169cd1ca7eba64b6668 || git fetch origin master) && git reset -q --hard 654ee104df48ee785861d169cd1ca7eba64b6668 && 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.26.2")) (copy (src .) (dst /src/)) (run (shell "opam exec -- dune build @fmt --ignore-promoted-rules || (echo \"dune build @fmt failed\"; exit 2)")) ) 2024-11-05 15:13.53: Waiting for resource in pool OCluster 2024-11-05 15:13.53: Waiting for worker… 2024-11-05 15:13.53: Got resource from pool OCluster Building on x86-bm-c11.sw.ocaml.org All commits already cached HEAD is now at dcac42e Test tweaks (from ocaml/opam:debian-12-ocaml-4.08@sha256:e4f2cf9099096504addd23b73b0d98c5a1fbb1633a6d52b7627cfa16f89debf8) 2024-11-05 15:13.53 ---> using "45ed51cabfe3de1acd486922e22b24eee2a37ab1a07c3ddaa8a9367527eeade3" from cache /: (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 654ee104df48ee785861d169cd1ca7eba64b6668 || git fetch origin master) && git reset -q --hard 654ee104df48ee785861d169cd1ca7eba64b6668 && git log --no-decorate -n1 --oneline && opam update -u")) From https://github.com/ocaml/opam-repository * branch master -> FETCH_HEAD d872638bdf..8582dee8ae master -> origin/master 654ee104df Merge pull request #26834 from mtelvers/opam-publish-ocaml-version.3.7.0 <><> Updating package repositories ><><><><><><><><><><><><><><><><><><><><><><> [default] synchronised from file:///home/opam/opam-repository default (at 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 2024-11-05 15:13.53 ---> using "18901fe09c8dc82dfc1bd6387f454db3a5837c77a102a9a582c26793a9a85840" from cache /: (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.16.1 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [dune.3.16.1] found in cache <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> installed dune.3.16.1 Done. # Run eval $(opam env) to update the current shell environment 2024-11-05 15:13.53 ---> using "38c457990c07d85296d3b7bed82ffaff5af001eae317464ac0a075812df097e9" from cache /: (workdir /src) /src: (run (cache (opam-archives (target /home/opam/.opam/download-cache))) (network host) (shell "opam depext -i ocamlformat=0.26.2")) # 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 menhirLib 20240715 [required by ocamlformat-lib] - install menhirCST 20240715 [required by menhir] - install menhirSdk 20240715 [required by ocamlformat-lib] - install ocaml-version 3.7.0 [required by ocamlformat-lib] - install ocamlbuild 0.15.0 [required by fpath, astring, uuseg] - install either 1.0.0 [required by ocamlformat-lib] - install ocamlfind 1.9.6 [required by ocp-indent, astring, fpath, uuseg] - install cmdliner 1.3.0 [required by ocamlformat] - install result 1.5 [required by ocamlformat-lib] - install seq base [required by re] - install csexp 1.5.2 [required by ocamlformat-lib] - install camlp-streams 5.0.1 [required by ocamlformat-lib] - install fix 20230505 [required by ocamlformat-lib] - install dune-build-info 3.16.1 [required by ocamlformat-lib] - install menhir 20240715 [required by ocamlformat-lib] - install topkg 1.0.7 [required by fpath, astring, uuseg] - install base-bytes base [required by ocp-indent] - install re 1.11.0 [required by ocamlformat] - install dune-configurator 3.16.1 [required by base] - install uutf 1.0.3 [required by ocamlformat-lib] - install astring 0.8.5 [required by ocamlformat-lib] - install ocp-indent 1.8.1 [required by ocamlformat-lib] - install base v0.14.3 [required by ocamlformat-lib] - install uucp 15.0.0 [required by uuseg] - install fpath 0.7.3 [required by ocamlformat-lib] - install stdio v0.14.0 [required by ocamlformat-lib] - install uuseg 15.0.0 [required by ocamlformat-lib] - install ocamlformat-lib 0.26.2 [required by ocamlformat] - install ocamlformat 0.26.2 ===== 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.3.0] found in cache [csexp.1.5.2] found in cache [dune-build-info.3.16.1] found in cache [dune-configurator.3.16.1] found in cache [either.1.0.0] found in cache [fix.20230505] 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.3.7.0] found in cache [ocamlbuild.0.15.0] found in cache [ocamlfind.1.9.6] found in cache [ocamlformat.0.26.2] found in cache [ocamlformat-lib.0.26.2] found in cache [ocp-indent.1.8.1] 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.3.0 -> installed menhirCST.20240715 -> installed menhirLib.20240715 -> installed menhirSdk.20240715 -> installed ocaml-version.3.7.0 -> installed re.1.11.0 -> installed result.1.5 -> installed sexplib0.v0.14.0 -> installed dune-build-info.3.16.1 -> installed dune-configurator.3.16.1 -> installed ocamlfind.1.9.6 -> installed base-bytes.base -> installed ocamlbuild.0.15.0 -> installed ocp-indent.1.8.1 -> installed base.v0.14.3 -> installed stdio.v0.14.0 -> installed topkg.1.0.7 -> installed uutf.1.0.3 -> installed astring.0.8.5 -> installed fpath.0.7.3 -> installed menhir.20240715 -> installed uucp.15.0.0 -> installed uuseg.15.0.0 -> installed ocamlformat-lib.0.26.2 -> installed ocamlformat.0.26.2 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-11-05 15:15.20 ---> saved as "461fccf8bc43bcf03b770a5f2324a4ebdbf1e3173fbd6e418b4a30a84fb31b26" /src: (copy (src .) (dst /src/)) 2024-11-05 15:15.21 ---> saved as "064e94c532c4fa4e43e4c4deaa1a87a64f7d71df73dc971ccbf36e90005418f7" /src: (run (shell "opam exec -- dune build @fmt --ignore-promoted-rules || (echo \"dune build @fmt failed\"; exit 2)")) File "src/stdlib/gospelstdlib.mli", line 1, characters 0-0: diff --git a/_build/default/src/stdlib/gospelstdlib.mli b/_build/default/src/stdlib/.formatted/gospelstdlib.mli index c82bf5b..d00b545 100644 --- a/_build/default/src/stdlib/gospelstdlib.mli +++ b/_build/default/src/stdlib/.formatted/gospelstdlib.mli @@ -108,42 +108,42 @@ module Sequence : sig (*@ predicate in_range (s : 'a t) (i : integer) = 0 <= i < length s *) (*@ axiom length_nonneg : forall s. 0 <= length s *) - + (*@ axiom append_length : forall s s'. length (s++s') = length s + length s' *) (*@ axiom append_elems_left : forall s s' i. 0 <= i < length s -> (s ++ s')[i] = s[i] *) - + (*@ axiom append_elems_right : forall s s' i. length s <= i < length s + length s' -> (s ++ s')[i] = s'[i - length s] *) - + (*@ axiom subseq_l : forall s i. 0 <= i < length s -> s[i ..] = s[i .. length s] *) - + (*@ axiom subseq : forall s i i1 i2. 0 <= i1 <= i < i2 <= length s -> s[i] = (s[i1 .. i2])[i-i1] *) - + (*@ axiom subseq_len : forall s i1 i2. 0 <= i1 <= i2 < length s -> length (s[i1 .. i2]) = i1-i2 *) - + (*@ function empty : 'a t *) (** [empty] is the empty sequence. *) (*@ axiom empty_length : length empty = 0 *) - + (*@ function init (n: integer) (f: integer -> 'a) : 'a t *) (** [init n f] is the sequence containing [f 0], [f 1], [...] , [f n]. *) (*@ axiom init_length : forall n f. n >= 0 -> length (init n f) = n *) - + (* TODO : replace init with notation *) (*@ axiom init_elems : forall n f. forall i. 0 <= i < n -> (init n f)[i] = f i *) (*@ function singleton (x: 'a) : 'a t = init 1 (fun _ -> x) *) (** [singleton] is the sequence containing [x]. *) - + (*@ function cons (x: 'a) (s: 'a t): 'a t = (singleton x) ++ s *) (** [cons x s] is the sequence containing [x] followed by the elements of [s]. *) @@ -162,8 +162,7 @@ module Sequence : sig (** [append s s'] is [s ++ s']. *) (*@ function multiplicity (x : 'a) (s: 'a t) : integer *) - (** [multiplicity x s] counts the number of occurrences of - [x] in [s] *) + (** [multiplicity x s] counts the number of occurrences of [x] in [s] *) (*@ axiom mult_empty : forall x. multiplicity x empty = 0 *) @@ -178,12 +177,12 @@ module Sequence : sig (** [mem s x] holds iff [x] is in [s]. *) (*@ function map (f: 'a -> 'b) (s: 'a t) : 'b t *) - + (*@ axiom map_elems : forall i f s. 0 <= i < length s -> (map f s)[i] = f (s[i]) *) (** [map f s] is a sequence whose elements are the elements of [s], transformed by [f]. *) - + (*@ function filter (f: 'a -> bool) (s: 'a t) : 'a t *) (** [filter f s] is a sequence whose elements are the elements of [s], that satisfy [f]. *) @@ -195,10 +194,9 @@ module Sequence : sig (** [get s i] is [s[i]]. *) (*@ function set (s: 'a t) (i: integer) (x: 'a): 'a t *) - (** [set s i x] returns a new sequence identical to x - where the only difference is that the element at - index [i] equal [x] *) - + (** [set s i x] returns a new sequence identical to x where the only + difference is that the element at index [i] equal [x] *) + (*@ axiom set_elem : forall s i x. 0 <= i < length s -> (set s i x)[i] = x *) (*@ axiom set_elem_other : @@ -206,13 +204,13 @@ module Sequence : sig 0 <= i1 < length s -> 0 <= i2 < length s -> (set s i1 x)[i2] = s[i2] *) - + (*@ function rev (s: 'a t) : 'a t *) (** [rev s] is the sequence containing the same elements as [s], in reverse order. *) (*@ axiom rev_length : forall s. length s = length (rev s) *) - + (*@ axiom rev_elems : forall i s. 0 <= i < length s -> (rev s)[i] = s[length s - 1 - i] *) @@ -223,7 +221,7 @@ module Sequence : sig *) (*@ function fold (f: 'a -> 'b -> 'a) (acc: 'a) (s: 'b sequence) : 'a *) - (** [fold f acc s] is [f (... (f (f acc s[0]) s[1]) ...) s[n-1]], where [n] is + (** [fold f acc s] is [f (... (f (f acc s[0]) s[1]) ...) s[n-1]], where [n] is the length of [s]. *) (*@ axiom fold_empty : forall f acc. fold f acc empty = acc *) @@ -249,41 +247,41 @@ module Bag : sig (** [multiplicity x b] is the number of occurrences of [x] in [s]. *) (*@ axiom well_formed : forall b x. multiplicity b x >= 0 *) - + (*@ function empty : 'a t *) (** [empty] is the empty bag. *) (*@ axiom empty_mult : forall x. multiplicity x empty = 0 *) (*@ function init (f : 'a -> integer) : 'a t *) - (** [init f] Creates a bag where every element [x] has - multiplicity [max 0 (f x)]. *) - + (** [init f] Creates a bag where every element [x] has multiplicity + [max 0 (f x)]. *) + (*@ axiom init_axiom : forall f x. max 0 (f x) = multiplicity x (init f) *) (*@ predicate mem (x: 'a) (b: 'a t) = multiplicity x b > 0 *) (** [mem x b] holds iff [b] contains [x] at least once. *) - + (*@ function add (x: 'a) (b: 'a t) : 'a t *) (** [add x b] is [b] when an occurence of [x] was added. *) (*@ axiom add_mult_x : forall b x. multiplicity x (add x b) = 1 + multiplicity x b *) - + (*@ axiom add_mult_neg_x : forall x y b. x <> y -> multiplicity y (add x b) = (multiplicity y b) *) - + (*@ function singleton (x: 'a) : 'a t = add x empty *) (** [singleton x] is a bag containing one occurence of [x]. *) (*@ function remove (x: 'a) (b: 'a t) : 'a t *) (** [remove x b] is [b] where an occurence of [x] was removed. *) - + (*@ axiom remove_mult_x : forall b x. multiplicity x (remove x b) = max 0 (multiplicity x b - 1) *) - + (*@ axiom remove_mult_neg_x : forall x y b. x <> y -> multiplicity y (remove x b) = multiplicity y b *) - + (*@ function union (b b': 'a t) : 'a t *) (** [union b b'] is a bag [br] where for all element [x], [occurences x br = max @@ -291,7 +289,7 @@ module Bag : sig (*@ axiom union_all : forall b b' x. max (multiplicity x b) (multiplicity x b') = multiplicity x (union b b') *) - + (*@ function sum (b b': 'a t) : 'a t *) (** [sum b b'] is a bag [br] where for all element [x], [occurences x br = @@ -299,7 +297,7 @@ module Bag : sig (*@ axiom sum_all : forall b b' x. multiplicity x b + multiplicity x b' = multiplicity x (sum b b') *) - + (*@ function inter (b b': 'a t) : 'a t *) (** [inter b b'] is a bag [br] where for all element [x], [occurences x br = @@ -310,7 +308,7 @@ module Bag : sig (** [inter b b'] is a bag [br] where for all element [x], [multiplicity x br = min (multiplicity x b) (multiplicity x b')]. *) - + (*@ predicate disjoint (b b': 'a t) = forall x. mem x b -> not (mem x b') *) @@ -325,22 +323,22 @@ module Bag : sig (*@ function filter (f: 'a -> bool) (b: 'a t) : 'a t *) (** [filter f b] is the bag of all elements in [b] that satisfy [f]. *) - + (*@ predicate subset (b b': 'a t) = forall x. multiplicity x b <= multiplicity x b' *) (** [subset b b'] holds iff for all element [x], [multiplicity x b <= multiplicity x b']. *) - (*@ axiom filter_mem : forall b x f. f x -> - multiplicity x (filter f b) = multiplicity x b *) - - (*@ axiom filter_mem_neg : - forall b x f. not (f x) -> multiplicity x (filter f b) = 0 *) + (*@ axiom filter_mem : forall b x f. f x -> + multiplicity x (filter f b) = multiplicity x b *) + + (*@ axiom filter_mem_neg : + forall b x f. not (f x) -> multiplicity x (filter f b) = 0 *) (*@ axiom filter_mem : forall b x f. f x -> multiplicity x (filter f b) = multiplicity x b *) (*@ axiom filter_mem_neg : forall b x f. not (f x) -> multiplicity x (filter f b) = 0 *) - + (*@ function cardinal (b: 'a t) : integer *) (** [cardinal b] is the total number of elements in [b], all occurrences being counted. *) @@ -374,10 +372,9 @@ module Bag : sig (*@ axiom of_seq_multiplicity : forall s x. Sequence.multiplicity x s = multiplicity x (of_seq s) *) - + (*@ function fold (f : 'a -> 'b -> 'b) (s : 'a t) (acc : 'b) : 'b *) (*<- to be removed*) - end (** {1 Sets} *) @@ -391,12 +388,12 @@ module Set : sig (*@ function empty : 'a t *) (** [empty] is [∅]. *) - + (*@ predicate mem (x: 'a) (s: 'a t) *) (** [mem x s] is [x ∈ s]. *) (*@ axiom empty_mem : forall x. not (mem x empty) *) - + (*@ function add (x: 'a) (s: 'a t) : 'a t *) (** [add x s] is [s ∪ {x}]. *) @@ -405,7 +402,7 @@ module Set : sig (*@ axiom add_mem_neq : forall s x y. x <> y -> (mem x s <-> mem x (add y s)) *) - + (*@ function singleton (x: 'a) : 'a t = add x empty *) (** [singleton x] is [{x}]. *) @@ -418,7 +415,7 @@ module Set : sig (*@ axiom remove_mem_neq : forall s x y. x <> y -> (mem x s <-> mem x (remove y s)) *) - + (*@ function union (s s': 'a t) : 'a t *) (** [union s s'] is [s ∪ s']. *) @@ -427,7 +424,7 @@ module Set : sig (*@ axiom union_mem_neg : forall s s' x. not (mem x s) -> not (mem x s') -> not (mem x (union s s')) *) - + (*@ function inter (s s': 'a t) : 'a t *) (** [inter s s'] is [s ∩ s']. *) @@ -438,7 +435,7 @@ module Set : sig (*@ axiom inter_mem_neq : forall s s' x. not (mem x s || mem x s') -> not mem x (inter s s') *) - + (*@ predicate disjoint (s s': 'a t) = inter s s' = empty *) (** [disjoint s s'] is [s ∩ s' = ∅]. *) @@ -447,11 +444,11 @@ module Set : sig (*@ axiom diff_mem : forall s s' x. mem x s' -> not (mem x (diff s s')) *) - + (*@ axiom diff_mem_fst : forall s s' x. not (mem x s') -> (mem x s <-> mem x (diff s s')) *) - + (*@ predicate subset (s s': 'a t) = forall x. mem x s -> mem x s'*) (** [subset s s'] is [s ⊂ s']. *) @@ -462,7 +459,7 @@ module Set : sig (*@ axiom set_map : forall f s x. mem x (map f s) <-> (exists y. f y = x && mem y s) *) - + (*@ function partition (f: 'a -> bool) (s: 'a t) : ('a t * 'a t) *) (** [partition f s] is the pair of sets [(s1, s2)], where [s1] is the set of all the elements of [s] that satisfy the predicate [f], and [s2] is the @@ -474,7 +471,7 @@ module Set : sig (*@ predicate finite (s : 'a t) = exists seq. forall x. mem x s -> Sequence.mem x seq *) - + (*@ axiom cardinal_nonneg : forall s. cardinal s >= 0 *) (*@ axiom cardinal_empty : cardinal empty = 0 *) @@ -489,7 +486,6 @@ module Set : sig then cardinal (add x s) = cardinal s else cardinal (add x s) = cardinal s + 1 *) - (*@ function of_seq (s: 'a Sequence.t) : 'a t *) (*@ function fold (f : 'a -> 'b -> 'b) (s : 'a t) (acc : 'b) : 'b *) @@ -499,7 +495,6 @@ end (*@ function ( [->] ) (f: 'a -> 'b) (x:'a) (y: 'b) : 'a -> 'b *) module Map : sig - (** Maps from keys of type ['a] to values of type ['b] are represented by Gospel functions of type ['a -> 'b]. *) @@ -509,7 +504,6 @@ module Map : sig (*@ axiom domain_mem : forall x m default. m x <> default -> Set.mem x (domain default m) *) - end (* The following modules are deprecated and only exist to ensure the tests pass. In the future, assuming this branch is merged, they should be removed and the tests changed*) 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-11-05 15:15.23: Job failed: Failed: Build failed