Getting StartedDocumentation
Organisationsocaml-gospelgospele3efb7 ()windows-server-2022-amd64-5.2_opam-2.2

windows-server-2022-amd64-5.2_opam-2.2

Link Copied
Code Copied

Logs

Show raw logs
2024-11-07 16:11.28: New job: test ocaml-gospel/gospel https://github.com/ocaml-gospel/gospel.git#refs/pull/423/head (e3efb715d4b526e34808453bb047667b95f53a73) (windows-amd64:windows-server-2022-amd64-5.2_opam-2.2)
Base: windows-server-2022-amd64-ocaml-5.2
Opam project build


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 e3efb715
cat > Dockerfile <<'END-OF-DOCKERFILE'
FROM windows-server-2022-amd64-ocaml-5.2
# windows-server-2022-amd64-5.2_opam-2.2
USER 1000:1000
ENV CLICOLOR_FORCE="1"
ENV OPAMCOLOR="always"
RUN ln -f /usr/bin/opam-2.2 /usr/bin/opam
RUN opam init --reinit -ni
RUN uname -rs && opam exec -- ocaml -version && opam --version
RUN cd ~/opam-repository && (git cat-file -e 371a52f4a8b5c88dc9de4f5a5f6375fb0963297a || git fetch origin master) && git reset -q --hard 371a52f4a8b5c88dc9de4f5a5f6375fb0963297a && git log --no-decorate -n1 --oneline && opam update -u
COPY --chown=1000:1000 gospel.opam /Users/opam/src/./
RUN opam pin add -yn gospel.dev '/Users/opam/src/./'
ENV DEPS="arch-x86_64.1 astring.0.8.5 base-bigarray.base base-domains.base base-nnp.base base-threads.base base-unix.base camlp-streams.5.0.1 cmdliner.1.3.0 conf-mingw-w64-gcc-x86_64.1 cppo.1.7.0 crunch.3.3.1 dune.3.16.1 dune-build-info.3.16.1 flexdll.0.43 fmt.0.9.0 fpath.0.7.3 host-arch-x86_64.1 host-system-mingw.1 menhir.20240715 menhirCST.20240715 menhirLib.20240715 menhirSdk.20240715 mingw-w64-shims.0.2.0 ocaml.5.2.0 ocaml-base-compiler.5.2.0 ocaml-compiler-libs.v0.17.0 ocaml-config.3 ocaml-env-mingw64.1 ocaml-options-vanilla.1 ocamlbuild.0.15.0 ocamlfind.1.9.5 odoc.2.4.3 odoc-parser.2.4.3 pp_loc.2.1.0 ppx_derivers.1.2.1 ppx_deriving.6.0.3 ppxlib.0.33.0 ptime.1.2.0 re.1.12.0 result.1.5 seq.base sexplib0.v0.17.0 stdlib-shims.0.3.0 system-mingw.1 topkg.1.0.7 tyxml.4.6.0 uutf.1.0.3"
ENV CI="true"
ENV OCAMLCI="true"
RUN opam update --depexts && opam install --cli=2.2 --depext-only -y gospel.dev $DEPS
RUN opam install $DEPS
COPY --chown=1000:1000 . /Users/opam/src
RUN cd /cygdrive/c/Users/opam/src && opam exec -- dune build @install @check @runtest && rm -rf _build


END-OF-DOCKERFILE
docker build .
END-REPRO-BLOCK


2024-11-07 16:11.28: Using cache hint "ocaml-gospel/gospel-windows-server-2022-amd64-ocaml-5.2-windows-server-2022-amd64-5.2_opam-2.2-a24b7a4f5e80f822ede4d47b0d94fed0"
2024-11-07 16:11.28: Using OBuilder spec:
((from windows-server-2022-amd64-ocaml-5.2)
(comment windows-server-2022-amd64-5.2_opam-2.2)
(user (uid 1000) (gid 1000))
(env CLICOLOR_FORCE 1)
(env OPAMCOLOR always)
(run (shell "ln -f /usr/bin/opam-2.2 /usr/bin/opam"))
(run (shell "opam init --reinit -ni"))
(run (shell "uname -rs && opam exec -- ocaml -version && opam --version"))
(run (cache (opam-archives (target "c:\\Users\\opam\\AppData\\local\\opam\\download-cache")))
(network host)
(shell "cd ~/opam-repository && (git cat-file -e 371a52f4a8b5c88dc9de4f5a5f6375fb0963297a || git fetch origin master) && git reset -q --hard 371a52f4a8b5c88dc9de4f5a5f6375fb0963297a && git log --no-decorate -n1 --oneline && opam update -u"))
(copy (src gospel.opam) (dst /Users/opam/src/./))
(run (network host)
(shell "opam pin add -yn gospel.dev '/Users/opam/src/./'"))
(env DEPS "arch-x86_64.1 astring.0.8.5 base-bigarray.base base-domains.base base-nnp.base base-threads.base base-unix.base camlp-streams.5.0.1 cmdliner.1.3.0 conf-mingw-w64-gcc-x86_64.1 cppo.1.7.0 crunch.3.3.1 dune.3.16.1 dune-build-info.3.16.1 flexdll.0.43 fmt.0.9.0 fpath.0.7.3 host-arch-x86_64.1 host-system-mingw.1 menhir.20240715 menhirCST.20240715 menhirLib.20240715 menhirSdk.20240715 mingw-w64-shims.0.2.0 ocaml.5.2.0 ocaml-base-compiler.5.2.0 ocaml-compiler-libs.v0.17.0 ocaml-config.3 ocaml-env-mingw64.1 ocaml-options-vanilla.1 ocamlbuild.0.15.0 ocamlfind.1.9.5 odoc.2.4.3 odoc-parser.2.4.3 pp_loc.2.1.0 ppx_derivers.1.2.1 ppx_deriving.6.0.3 ppxlib.0.33.0 ptime.1.2.0 re.1.12.0 result.1.5 seq.base sexplib0.v0.17.0 stdlib-shims.0.3.0 system-mingw.1 topkg.1.0.7 tyxml.4.6.0 uutf.1.0.3")
(env CI true)
(env OCAMLCI true)
(run (cache (opam-archives (target "c:\\Users\\opam\\AppData\\local\\opam\\download-cache")))
(network host)
(shell "opam update --depexts && opam install --cli=2.2 --depext-only -y gospel.dev $DEPS"))
(run (cache (opam-archives (target "c:\\Users\\opam\\AppData\\local\\opam\\download-cache")))
(network host)
(shell "opam install $DEPS"))
(copy (src .) (dst /Users/opam/src))
(run (shell "cd /cygdrive/c/Users/opam/src && opam exec -- dune build @install @check @runtest && rm -rf _build"))
)


2024-11-07 16:11.28: Waiting for resource in pool OCluster
2024-11-07 22:21.56: Waiting for worker…
2024-11-08 00:16.38: Got resource from pool OCluster
Building on odawa
All commits already cached
HEAD is now at e3efb71 Rewrite Map module


(from windows-server-2022-amd64-ocaml-5.2)
2024-11-08 00:16.38 ---> using "112de547835816fcbe31275d69498e33d422e32a95556906be9d3491487c8b0d" from cache


/: (comment windows-server-2022-amd64-5.2_opam-2.2)


/: (user (uid 1000) (gid 1000))


/: (env CLICOLOR_FORCE 1)


/: (env OPAMCOLOR always)


/: (run (shell "ln -f /usr/bin/opam-2.2 /usr/bin/opam"))
2024-11-08 00:16.38 ---> using "222150cdc39ce03baa08b6dceb88795bedeb63ece9c3d938b17acd015061df11" from cache


/: (run (shell "opam init --reinit -ni"))
No configuration file found, using built-in defaults.


<><> Unix support infrastructure ><><><><><><><><><><><><><><><><><><><><><><><>


opam and the OCaml ecosystem in general require various Unix tools in order to operate correctly. At present, this requires the installation of Cygwin to provide these tools.


How should opam obtain Unix tools?
> 1. Use tools found in PATH (Cygwin installation at C:\cygwin64)
2. Automatically create an internal Cygwin installation that will be managed by opam (recommended)
3. Use Cygwin installation found in C:\cygwin64
4. Use another existing Cygwin/MSYS2 installation
5. Abort initialisation


[1/2/3/4/5] 1
Checking for available remotes: rsync and local, git.
- you won't be able to use mercurial repositories unless you install the hg command on your system.
- you won't be able to use darcs repositories unless you install the darcs command on your system.


<><> Updating repositories ><><><><><><><><><><><><><><><><><><><><><><><><><><>
[default] no changes from file://C:/Users/opam/opam-repository
2024-11-08 00:16.38 ---> using "004edafede42d00c8911fe96056b9048b76567fb3ed0c138bd6fc45c62313942" from cache


/: (run (shell "uname -rs && opam exec -- ocaml -version && opam --version"))
CYGWIN_NT-10.0-20348 3.5.4-1.x86_64
The OCaml toplevel, version 5.2.0
2.2.1
2024-11-08 00:16.38 ---> using "999c3c7b46aec339a45f42331444bced8e3750e681a11f1b1f3b5aa484fcdfcd" from cache


/: (run (cache (opam-archives (target "c:\\Users\\opam\\AppData\\local\\opam\\download-cache")))
(network host)
(shell "cd ~/opam-repository && (git cat-file -e 371a52f4a8b5c88dc9de4f5a5f6375fb0963297a || git fetch origin master) && git reset -q --hard 371a52f4a8b5c88dc9de4f5a5f6375fb0963297a && git log --no-decorate -n1 --oneline && opam update -u"))
371a52f4a8 Merge pull request #26816 from maiste/release-dune-3.16.1


<><> Updating package repositories ><><><><><><><><><><><><><><><><><><><><><><>
[default] synchronised from file://C:/Users/opam/opam-repository


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-08 00:16.38 ---> using "cb751ccf6189d6bd201a5b1841a3615635b5717f1eefa38cf54ca5171f65f2ad" from cache


/: (copy (src gospel.opam) (dst /Users/opam/src/./))
2024-11-08 00:16.38 ---> using "c53986b733ced404f82c3ada561174de48c689b6e196865d1299fb7e5a16a2f7" from cache


/: (run (network host)
(shell "opam pin add -yn gospel.dev '/Users/opam/src/./'"))
[gospel.dev] synchronised (file://C:/Users/opam/src/.)
gospel is now pinned to file://C:/Users/opam/src/. (version dev)
2024-11-08 00:16.38 ---> using "f38b02a5bb6eef582ae819d64a3e06f7e878e7aa42f5ec529fe29c07f34a21e1" from cache


/: (env DEPS "arch-x86_64.1 astring.0.8.5 base-bigarray.base base-domains.base base-nnp.base base-threads.base base-unix.base camlp-streams.5.0.1 cmdliner.1.3.0 conf-mingw-w64-gcc-x86_64.1 cppo.1.7.0 crunch.3.3.1 dune.3.16.1 dune-build-info.3.16.1 flexdll.0.43 fmt.0.9.0 fpath.0.7.3 host-arch-x86_64.1 host-system-mingw.1 menhir.20240715 menhirCST.20240715 menhirLib.20240715 menhirSdk.20240715 mingw-w64-shims.0.2.0 ocaml.5.2.0 ocaml-base-compiler.5.2.0 ocaml-compiler-libs.v0.17.0 ocaml-config.3 ocaml-env-mingw64.1 ocaml-options-vanilla.1 ocamlbuild.0.15.0 ocamlfind.1.9.5 odoc.2.4.3 odoc-parser.2.4.3 pp_loc.2.1.0 ppx_derivers.1.2.1 ppx_deriving.6.0.3 ppxlib.0.33.0 ptime.1.2.0 re.1.12.0 result.1.5 seq.base sexplib0.v0.17.0 stdlib-shims.0.3.0 system-mingw.1 topkg.1.0.7 tyxml.4.6.0 uutf.1.0.3")


/: (env CI true)


/: (env OCAMLCI true)


/: (run (cache (opam-archives (target "c:\\Users\\opam\\AppData\\local\\opam\\download-cache")))
(network host)
(shell "opam update --depexts && opam install --cli=2.2 --depext-only -y gospel.dev $DEPS"))


<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[gospel.dev] synchronised (no changes)


[NOTE] Package system-mingw is already installed (current version is 1).
[NOTE] Package ocaml-options-vanilla is already installed (current version is 1).
[NOTE] Package ocaml-env-mingw64 is already installed (current version is 1).
[NOTE] Package ocaml-config is already installed (current version is 3).
[NOTE] Package ocaml-base-compiler is already installed (current version is 5.2.0).
[NOTE] Package ocaml is already installed (current version is 5.2.0).
[NOTE] Package mingw-w64-shims is already installed (current version is 0.2.0).
[NOTE] Package host-system-mingw is already installed (current version is 1).
[NOTE] Package host-arch-x86_64 is already installed (current version is 1).
[NOTE] Package flexdll is already installed (current version is 0.43).
[NOTE] Package conf-mingw-w64-gcc-x86_64 is already installed (current version is 1).
[NOTE] Package base-unix is already installed (current version is base).
[NOTE] Package base-threads is already installed (current version is base).
[NOTE] Package base-nnp is already installed (current version is base).
[NOTE] Package base-domains is already installed (current version is base).
[NOTE] Package base-bigarray is already installed (current version is base).
[NOTE] Package arch-x86_64 is already installed (current version is 1).
2024-11-08 00:16.38 ---> using "874f487d862e1b3928d49b1185f9d5c2f95665d97dbcac17b7b62b09f79b8800" from cache


/: (run (cache (opam-archives (target "c:\\Users\\opam\\AppData\\local\\opam\\download-cache")))
(network host)
(shell "opam install $DEPS"))
[NOTE] Package system-mingw is already installed (current version is 1).
[NOTE] Package ocaml-options-vanilla is already installed (current version is 1).
[NOTE] Package ocaml-env-mingw64 is already installed (current version is 1).
[NOTE] Package ocaml-config is already installed (current version is 3).
[NOTE] Package ocaml-base-compiler is already installed (current version is 5.2.0).
[NOTE] Package ocaml is already installed (current version is 5.2.0).
[NOTE] Package mingw-w64-shims is already installed (current version is 0.2.0).
[NOTE] Package host-system-mingw is already installed (current version is 1).
[NOTE] Package host-arch-x86_64 is already installed (current version is 1).
[NOTE] Package flexdll is already installed (current version is 0.43).
[NOTE] Package conf-mingw-w64-gcc-x86_64 is already installed (current version is 1).
[NOTE] Package base-unix is already installed (current version is base).
[NOTE] Package base-threads is already installed (current version is base).
[NOTE] Package base-nnp is already installed (current version is base).
[NOTE] Package base-domains is already installed (current version is base).
[NOTE] Package base-bigarray is already installed (current version is base).
[NOTE] Package arch-x86_64 is already installed (current version is 1).
The following actions will be performed:
=== install 31 packages
- install astring             0.8.5
- install camlp-streams       5.0.1
- install cmdliner            1.3.0
- install cppo                1.7.0
- install crunch              3.3.1
- install dune                3.16.1
- install dune-build-info     3.16.1
- install fmt                 0.9.0
- install fpath               0.7.3
- install menhir              20240715
- install menhirCST           20240715
- install menhirLib           20240715
- install menhirSdk           20240715
- install ocaml-compiler-libs v0.17.0
- install ocamlbuild          0.15.0
- install ocamlfind           1.9.5
- install odoc                2.4.3
- install odoc-parser         2.4.3
- install pp_loc              2.1.0
- install ppx_derivers        1.2.1
- install ppx_deriving        6.0.3
- install ppxlib              0.33.0
- install ptime               1.2.0
- install re                  1.12.0
- install result              1.5
- install seq                 base
- install sexplib0            v0.17.0
- install stdlib-shims        0.3.0
- install topkg               1.0.7
- install tyxml               4.6.0
- install uutf                1.0.3


<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved astring.0.8.5  (cached)
-> retrieved camlp-streams.5.0.1  (cached)
-> retrieved cmdliner.1.3.0  (cached)
-> retrieved cppo.1.7.0  (cached)
-> retrieved crunch.3.3.1  (cached)
-> retrieved fmt.0.9.0  (cached)
-> retrieved fpath.0.7.3  (cached)
-> retrieved ocaml-compiler-libs.v0.17.0  (cached)
-> retrieved menhir.20240715, menhirCST.20240715, menhirLib.20240715, menhirSdk.20240715  (cached)
-> retrieved ocamlbuild.0.15.0  (cached)
-> retrieved ocamlfind.1.9.5  (cached)
-> retrieved pp_loc.2.1.0  (cached)
-> retrieved dune.3.16.1, dune-build-info.3.16.1  (cached)
-> retrieved odoc.2.4.3, odoc-parser.2.4.3  (cached)
-> retrieved ppx_derivers.1.2.1  (cached)
-> retrieved ppx_deriving.6.0.3  (cached)
-> retrieved ptime.1.2.0  (cached)
-> retrieved ppxlib.0.33.0  (cached)
-> retrieved seq.base  (cached)
-> retrieved re.1.12.0  (cached)
-> retrieved result.1.5  (cached)
-> retrieved sexplib0.v0.17.0  (cached)
-> retrieved stdlib-shims.0.3.0  (cached)
-> retrieved topkg.1.0.7  (cached)
-> retrieved tyxml.4.6.0  (cached)
-> retrieved uutf.1.0.3  (cached)
-> installed cmdliner.1.3.0
-> installed seq.base
[WARNING] .install file is missing .exe extension for src/findlib/ocamlfind
[WARNING] .install file is missing .exe extension for src/findlib/ocamlfind_opt
[WARNING] Automatically adding .exe to C:\Users\opam\AppData\Local\opam\5.2.0\.opam-switch\build\ocamlfind.1.9.5\src\findlib\ocamlfind.exe
[WARNING] Automatically adding .exe to C:\Users\opam\AppData\Local\opam\5.2.0\.opam-switch\build\ocamlfind.1.9.5\src\findlib\ocamlfind_opt.exe
[WARNING] C:\Users\opam\AppData\Local\opam\5.2.0\bin\safe_camlp4 is a script; the command won't be available
-> installed ocamlfind.1.9.5
-> installed ocamlbuild.0.15.0
-> installed topkg.1.0.7
-> installed uutf.1.0.3
-> installed astring.0.8.5
-> installed dune.3.16.1
-> installed camlp-streams.5.0.1
-> installed cppo.1.7.0
-> installed fmt.0.9.0
-> installed fpath.0.7.3
-> installed menhirCST.20240715
-> installed ptime.1.2.0
-> installed ppx_derivers.1.2.1
-> installed stdlib-shims.0.3.0
-> installed result.1.5
-> installed crunch.3.3.1
-> installed dune-build-info.3.16.1
-> installed menhirLib.20240715
-> installed menhirSdk.20240715
-> installed pp_loc.2.1.0
-> installed sexplib0.v0.17.0
-> installed re.1.12.0
-> installed ocaml-compiler-libs.v0.17.0
-> installed odoc-parser.2.4.3
-> installed tyxml.4.6.0
-> installed odoc.2.4.3
-> installed ppxlib.0.33.0
-> installed ppx_deriving.6.0.3
-> installed menhir.20240715
Done.
# Run eval $(opam env) to update the current shell environment
2024-11-08 00:16.38 ---> using "1ffb6d0f24d5b45a808123151248d7ae0f57a082e030c33b7c2097b7cc54fc51" from cache


/: (copy (src .) (dst /Users/opam/src))
2024-11-08 00:16.58 ---> saved as "ea0e818bfdd683b881eba01f5d3f6fcfd7f014458f30e26fad093d8249fd1e39"


/: (run (shell "cd /cygdrive/c/Users/opam/src && opam exec -- dune build @install @check @runtest && rm -rf _build"))
(cd _build/default && C:\Users\opam\AppData\Local\opam\5.2.0\bin\ocamlopt.opt.exe -w @1..3@5..28@30..39@43@46..47@49..57@61..62-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -I src/.gospel.objs/byte -I src/.gospel.objs/native -I C:/Users/opam/AppData/Local/opam/5.2.0/lib/ocaml\compiler-libs -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\findlib -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\fmt -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\ocaml-compiler-libs\common -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\ocaml-compiler-libs\shadow -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\pp_loc -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\ppx_derivers -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\ppx_deriving/runtime -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\ppxlib -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\ppxlib\ast -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\ppxlib\astlib -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\ppxlib\print_diff -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\ppxlib\stdppx -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\ppxlib\traverse_builtins -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\sexplib0 -I C:\Users\opam\AppData\Local\opam\5.2.0\lib\stdlib-shims -intf-suffix .ml -no-alias-deps -opaque -open Gospel -o src/.gospel.objs/native/gospel__Typing.cmx -c -impl src/typing.pp.ml)
File "_none_", line 1:
Warning 58 [no-cmx-file]: no cmx file was found in path for module Findlib, and its interface was not compiled with -opaque
File "test/ppx/dune", lines 9-16, characters 0-196:
9 | (rule
10 |  (targets odoc_of_gospel.actual.mli)
11 |  (deps
12 |   (:pp pp.exe)
13 |   (:input odoc_of_gospel.mli)
14 |   (:gospel %{bin:gospel}))
15 |  (action
16 |   (run %{pp} --intf %{input} -pp "%{gospel} pps" -o %{targets})))
(cd _build/default/test/ppx && ./pp.exe --intf odoc_of_gospel.mli -pp "../../../install/default/bin/gospel.exe pps" -o odoc_of_gospel.actual.mli)
'..' is not recognized as an internal or external command,
operable program or batch file.
File "odoc_of_gospel.mli", line 1:
Error: Error while running external preprocessor
Command line: ../../../install/default/bin/gospel.exe pps "odoc_of_gospel.mli" > "C:\Users\opam\AppData\Local\Temp\build_c803c7_dune\ocamlpp696a78"


File "test/typechecker/open.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/typechecker/open.mli _build/default/test/typechecker/open.mli.output
diff --git a/_build/default/test/typechecker/open.mli b/_build/default/test/typechecker/open.mli.output
index cfd2167..50358f8 100644
--- a/_build/default/test/typechecker/open.mli
+++ b/_build/default/test/typechecker/open.mli.output
@@ -1,7 +1,7 @@
(*@ open Int_not_bool1 *)


(* {gospel_expected|
-   [125] File "./int_not_bool1.mli", line 1, characters 48-49:
+   [125] File ".\int_not_bool1.mli", line 1, characters 48-49:

1 | (*@ function rec f (x: bool) (y: int): bool = f y x *)
^
Error: This term has type int but a term was expected of type bool.
File "test/vocal/Arrays.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/vocal/Arrays.mli _build/default/test/vocal/Arrays.mli.output
diff --git a/_build/default/test/vocal/Arrays.mli b/_build/default/test/vocal/Arrays.mli.output
index 4291bbe..eb6ed5d 100644
--- a/_build/default/test/vocal/Arrays.mli
+++ b/_build/default/test/vocal/Arrays.mli.output
@@ -73,3 +73,8 @@ val knuth_shuffle : 'a array -> unit
(*@ knuth_shuffle a
modifies a
ensures  Array.permut (old a) a *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/typechecker/partial_application.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/typechecker/partial_application.mli _build/default/test/typechecker/partial_application.mli.output
diff --git a/_build/default/test/typechecker/partial_application.mli b/_build/default/test/typechecker/partial_application.mli.output
index a82485f..97de15e 100644
--- a/_build/default/test/typechecker/partial_application.mli
+++ b/_build/default/test/typechecker/partial_application.mli.output
@@ -7,3 +7,8 @@ val mems : 'a -> 'a list list -> bool
(* This is not; should it be? *)
ensures r = List._exists (List.mem x) xss
*)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "examples/Stack.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/examples/Stack.mli _build/default/examples/Stack.mli.output
diff --git a/_build/default/examples/Stack.mli b/_build/default/examples/Stack.mli.output
index b80476b..e4ce5fc 100644
--- a/_build/default/examples/Stack.mli
+++ b/_build/default/examples/Stack.mli.output
@@ -36,3 +36,8 @@ module type S = sig
ensures s1.view = (old s1.view ++ old s2.view)
ensures s2.view = Sequence.empty *)
end
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/typechecker/mutually_recursive_ghost_type.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/typechecker/mutually_recursive_ghost_type.mli _build/default/test/typechecker/mutually_recursive_ghost_type.mli.output
diff --git a/_build/default/test/typechecker/mutually_recursive_ghost_type.mli b/_build/default/test/typechecker/mutually_recursive_ghost_type.mli.output
index 1ee0524..c803465 100644
--- a/_build/default/test/typechecker/mutually_recursive_ghost_type.mli
+++ b/_build/default/test/typechecker/mutually_recursive_ghost_type.mli.output
@@ -1 +1,6 @@
(*@ type a = A and b = B of a *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/coercions/constr_literal.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/coercions/constr_literal.mli _build/default/test/coercions/constr_literal.mli.output
diff --git a/_build/default/test/coercions/constr_literal.mli b/_build/default/test/coercions/constr_literal.mli.output
index bbeec6c..4718b2f 100644
--- a/_build/default/test/coercions/constr_literal.mli
+++ b/_build/default/test/coercions/constr_literal.mli.output
@@ -3,3 +3,8 @@
val f : int -> int
(*@ y = f x
requires A 42i = A 42i *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/abstract_functions.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/abstract_functions.mli _build/default/test/syntax/abstract_functions.mli.output
diff --git a/_build/default/test/syntax/abstract_functions.mli b/_build/default/test/syntax/abstract_functions.mli.output
index f48eb0c..d381091 100644
--- a/_build/default/test/syntax/abstract_functions.mli
+++ b/_build/default/test/syntax/abstract_functions.mli.output
@@ -61,3 +61,8 @@
(*@ function h14 (x: 'a): test *)


(*@ function h15 (x: test): integer *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/patterns/allsorts.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/patterns/allsorts.mli _build/default/test/patterns/allsorts.mli.output
diff --git a/_build/default/test/patterns/allsorts.mli b/_build/default/test/patterns/allsorts.mli.output
index b09e742..8003882 100644
--- a/_build/default/test/patterns/allsorts.mli
+++ b/_build/default/test/patterns/allsorts.mli.output
@@ -202,3 +202,8 @@ val f16 : t16 -> int
| C (y,z) when (match y with A -> true | _ -> false) -> true
| _ -> true
*)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/literals/ints.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/literals/ints.mli _build/default/test/literals/ints.mli.output
diff --git a/_build/default/test/literals/ints.mli b/_build/default/test/literals/ints.mli.output
index 8c0887d..be68f72 100644
--- a/_build/default/test/literals/ints.mli
+++ b/_build/default/test/literals/ints.mli.output
@@ -8,3 +8,8 @@ val f : int -> int
requires 42 = 0x16
requires A 42i = A 0x16i
requires A 42i = A 43i *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/coercions/basic.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/coercions/basic.mli _build/default/test/coercions/basic.mli.output
diff --git a/_build/default/test/coercions/basic.mli b/_build/default/test/coercions/basic.mli.output
index 4ef5d58..9e799dd 100644
--- a/_build/default/test/coercions/basic.mli
+++ b/_build/default/test/coercions/basic.mli.output
@@ -3,3 +3,8 @@ type t2


(*@ function c (x: t1) : t2 *)
(*@ coercion *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/patterns/fun_pair.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/patterns/fun_pair.mli _build/default/test/patterns/fun_pair.mli.output
diff --git a/_build/default/test/patterns/fun_pair.mli b/_build/default/test/patterns/fun_pair.mli.output
index 1c505f8..5f7581e 100644
--- a/_build/default/test/patterns/fun_pair.mli
+++ b/_build/default/test/patterns/fun_pair.mli.output
@@ -2,3 +2,8 @@ val f : (int * 'a) list -> int list
(*@ ys = f xs
ensures ys = List.map (fun (x, _) -> x) xs
*)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/patterns/fun_triple.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/patterns/fun_triple.mli _build/default/test/patterns/fun_triple.mli.output
diff --git a/_build/default/test/patterns/fun_triple.mli b/_build/default/test/patterns/fun_triple.mli.output
index 4c1f1f1..ee91ee1 100644
--- a/_build/default/test/patterns/fun_triple.mli
+++ b/_build/default/test/patterns/fun_triple.mli.output
@@ -2,3 +2,8 @@ val f : ('a * 'b * 'c) list -> 'a list
(*@ xs = f ys
ensures xs = List.map (fun (x, _, _) : 'a -> x) ys
*)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/patterns/inner_cast.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/patterns/inner_cast.mli _build/default/test/patterns/inner_cast.mli.output
diff --git a/_build/default/test/patterns/inner_cast.mli b/_build/default/test/patterns/inner_cast.mli.output
index fb424cb..221dfcd 100644
--- a/_build/default/test/patterns/inner_cast.mli
+++ b/_build/default/test/patterns/inner_cast.mli.output
@@ -3,3 +3,8 @@ val f : int option -> int
requires match x with
| Some (y:int) -> y >= 0
| None -> true *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/patterns/allsorts2.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/patterns/allsorts2.mli _build/default/test/patterns/allsorts2.mli.output
diff --git a/_build/default/test/patterns/allsorts2.mli b/_build/default/test/patterns/allsorts2.mli.output
index f1cf02c..5a95dc5 100644
--- a/_build/default/test/patterns/allsorts2.mli
+++ b/_build/default/test/patterns/allsorts2.mli.output
@@ -26,3 +26,8 @@ type t2 = B of int * int


(*@ function f (x: t2) : unit =
match x with B _ -> () *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/patterns/fun_option.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/patterns/fun_option.mli _build/default/test/patterns/fun_option.mli.output
diff --git a/_build/default/test/patterns/fun_option.mli b/_build/default/test/patterns/fun_option.mli.output
index 03fb62a..b2a1941 100644
--- a/_build/default/test/patterns/fun_option.mli
+++ b/_build/default/test/patterns/fun_option.mli.output
@@ -2,3 +2,8 @@ val f : 'a option list -> bool
(*@ b = f os
ensures List._exists (fun (None | Some _) -> false) os
*)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/patterns/expressions_raises.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/patterns/expressions_raises.mli _build/default/test/patterns/expressions_raises.mli.output
diff --git a/_build/default/test/patterns/expressions_raises.mli b/_build/default/test/patterns/expressions_raises.mli.output
index 4e9cbb7..6736a36 100644
--- a/_build/default/test/patterns/expressions_raises.mli
+++ b/_build/default/test/patterns/expressions_raises.mli.output
@@ -23,3 +23,8 @@ val f : int -> t -> bool
(* raises E _ -> false *)
raises F _ -> true
raises F (_, _) -> true *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/pure/pure_promoted.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/pure/pure_promoted.mli _build/default/test/pure/pure_promoted.mli.output
diff --git a/_build/default/test/pure/pure_promoted.mli b/_build/default/test/pure/pure_promoted.mli.output
index 4d45055..6fb1af5 100644
--- a/_build/default/test/pure/pure_promoted.mli
+++ b/_build/default/test/pure/pure_promoted.mli.output
@@ -6,3 +6,8 @@ val f : int -> int
val g : int -> int
(*@ y = g x
requires f x > 0 *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/bitvector.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/bitvector.mli _build/default/test/syntax/bitvector.mli.output
diff --git a/_build/default/test/syntax/bitvector.mli b/_build/default/test/syntax/bitvector.mli.output
index 403961c..e6bc7d5 100644
--- a/_build/default/test/syntax/bitvector.mli
+++ b/_build/default/test/syntax/bitvector.mli.output
@@ -22,3 +22,8 @@ val mem : int -> t -> bool
(*@ b = mem i bv
checks 0 <= i < bv.size
ensures b <-> mem i bv *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/constants.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/constants.mli _build/default/test/syntax/constants.mli.output
diff --git a/_build/default/test/syntax/constants.mli b/_build/default/test/syntax/constants.mli.output
index b9939c4..d55d354 100644
--- a/_build/default/test/syntax/constants.mli
+++ b/_build/default/test/syntax/constants.mli.output
@@ -12,3 +12,8 @@ val y : t
val modify_y : unit -> unit
(*@ modify_y ()
modifies y *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/expressions.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/expressions.mli _build/default/test/syntax/expressions.mli.output
diff --git a/_build/default/test/syntax/expressions.mli b/_build/default/test/syntax/expressions.mli.output
index 265917e..40d4f3c 100644
--- a/_build/default/test/syntax/expressions.mli
+++ b/_build/default/test/syntax/expressions.mli.output
@@ -30,3 +30,8 @@ val f : int -> int -> int
ensures r = x + y
ensures r > 2
ensures r = 3 *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/allsorts_labels.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/allsorts_labels.mli _build/default/test/syntax/allsorts_labels.mli.output
diff --git a/_build/default/test/syntax/allsorts_labels.mli b/_build/default/test/syntax/allsorts_labels.mli.output
index de6c60c..56c02a7 100644
--- a/_build/default/test/syntax/allsorts_labels.mli
+++ b/_build/default/test/syntax/allsorts_labels.mli.output
@@ -54,3 +54,8 @@ val f : int ref -> unit
val f : int ref -> unit
(*@ f x
modifies x *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/ghost_arg2.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/ghost_arg2.mli _build/default/test/syntax/ghost_arg2.mli.output
diff --git a/_build/default/test/syntax/ghost_arg2.mli b/_build/default/test/syntax/ghost_arg2.mli.output
index 4feead3..ab8840a 100644
--- a/_build/default/test/syntax/ghost_arg2.mli
+++ b/_build/default/test/syntax/ghost_arg2.mli.output
@@ -7,3 +7,8 @@ val fib : int -> int -> int -> int
requires a = fibonacci i
requires b = fibonacci (i+1)
ensures r = fibonacci (i+n) *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/basic_functions_axioms.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/basic_functions_axioms.mli _build/default/test/syntax/basic_functions_axioms.mli.output
diff --git a/_build/default/test/syntax/basic_functions_axioms.mli b/_build/default/test/syntax/basic_functions_axioms.mli.output
index 1d370cf..1f48bc8 100644
--- a/_build/default/test/syntax/basic_functions_axioms.mli
+++ b/_build/default/test/syntax/basic_functions_axioms.mli.output
@@ -125,3 +125,8 @@ type 'a t6 = { xx : 'a; yy : int }
| {y = B; x} -> {yy=int_of_integer 10; xx = b.y }
| {x; y} -> {xx=y;yy=x}
*)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/constructor_arity5.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/constructor_arity5.mli _build/default/test/syntax/constructor_arity5.mli.output
diff --git a/_build/default/test/syntax/constructor_arity5.mli b/_build/default/test/syntax/constructor_arity5.mli.output
index dbab198..ff5d30c 100644
--- a/_build/default/test/syntax/constructor_arity5.mli
+++ b/_build/default/test/syntax/constructor_arity5.mli.output
@@ -5,3 +5,8 @@ val f : (int * int) option -> unit
| Some (_,_) -> true
| _ -> false
*)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/exceptions.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/exceptions.mli _build/default/test/syntax/exceptions.mli.output
diff --git a/_build/default/test/syntax/exceptions.mli b/_build/default/test/syntax/exceptions.mli.output
index 0f7befc..a18bd28 100644
--- a/_build/default/test/syntax/exceptions.mli
+++ b/_build/default/test/syntax/exceptions.mli.output
@@ -47,3 +47,8 @@ val f : 'a -> 'a
raises E11 'a' -> true
raises E11 ('a' | 'b') -> true
raises E11 ('c'..'z') -> true *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/ghost_arg1.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/ghost_arg1.mli _build/default/test/syntax/ghost_arg1.mli.output
diff --git a/_build/default/test/syntax/ghost_arg1.mli b/_build/default/test/syntax/ghost_arg1.mli.output
index f21e39a..fee1d0e 100644
--- a/_build/default/test/syntax/ghost_arg1.mli
+++ b/_build/default/test/syntax/ghost_arg1.mli.output
@@ -19,3 +19,8 @@ val log2_existsb : int -> int
(*@ r = log2_existsb x
requires exists i. i >= 0 /\ x = pow 2 i
ensures x = pow 2 r *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/infix.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/infix.mli _build/default/test/syntax/infix.mli.output
diff --git a/_build/default/test/syntax/infix.mli b/_build/default/test/syntax/infix.mli.output
index 06ee431..47048be 100644
--- a/_build/default/test/syntax/infix.mli
+++ b/_build/default/test/syntax/infix.mli.output
@@ -5,3 +5,8 @@ val ( == ) : 'a -> 'a -> bool
val ( == ) : 'a -> 'a -> bool
(*@ r = x == y
ensures r <-> x = y *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/literals.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/literals.mli _build/default/test/syntax/literals.mli.output
diff --git a/_build/default/test/syntax/literals.mli b/_build/default/test/syntax/literals.mli.output
index 67078e3..5dcb94c 100644
--- a/_build/default/test/syntax/literals.mli
+++ b/_build/default/test/syntax/literals.mli.output
@@ -9,3 +9,8 @@ val g : char -> string
(*@ y = g x
requires x = 'c'
ensures y = "c" *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/invariants.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/invariants.mli _build/default/test/syntax/invariants.mli.output
diff --git a/_build/default/test/syntax/invariants.mli b/_build/default/test/syntax/invariants.mli.output
index 80104d8..6b1fd9d 100644
--- a/_build/default/test/syntax/invariants.mli
+++ b/_build/default/test/syntax/invariants.mli.output
@@ -6,3 +6,8 @@ type t2 = private A | B


type t3 = private int * int
(*@ with x invariant 1 > 0 *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/keyword_as_prefix.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/keyword_as_prefix.mli _build/default/test/syntax/keyword_as_prefix.mli.output
diff --git a/_build/default/test/syntax/keyword_as_prefix.mli b/_build/default/test/syntax/keyword_as_prefix.mli.output
index ae54f16..2ba3a60 100644
--- a/_build/default/test/syntax/keyword_as_prefix.mli
+++ b/_build/default/test/syntax/keyword_as_prefix.mli.output
@@ -3,3 +3,8 @@ val function' : int -> int


val lemma_not_lemma : int -> int
(*@ lemma_not_lemma x *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/open2.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/open2.mli _build/default/test/syntax/open2.mli.output
diff --git a/_build/default/test/syntax/open2.mli b/_build/default/test/syntax/open2.mli.output
index 3623fc3..4549864 100644
--- a/_build/default/test/syntax/open2.mli
+++ b/_build/default/test/syntax/open2.mli.output
@@ -1,3 +1,8 @@
open Type


type t2 = t
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/open3.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/open3.mli _build/default/test/syntax/open3.mli.output
diff --git a/_build/default/test/syntax/open3.mli b/_build/default/test/syntax/open3.mli.output
index d4ac2fa..e893e9a 100644
--- a/_build/default/test/syntax/open3.mli
+++ b/_build/default/test/syntax/open3.mli.output
@@ -3,3 +3,8 @@ open Types_functions
type t3 = t1 * int t2


(*@ function f4 (x: int t2) (y: t1) : t3 = (y,x) *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/modules1.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/modules1.mli _build/default/test/syntax/modules1.mli.output
diff --git a/_build/default/test/syntax/modules1.mli b/_build/default/test/syntax/modules1.mli.output
index f569d90..8508155 100644
--- a/_build/default/test/syntax/modules1.mli
+++ b/_build/default/test/syntax/modules1.mli.output
@@ -16,3 +16,8 @@ type int
* module A : TA with type 'a t := 'a t1 *)


(* @ function t1 (x:'a t1) : float = A.f x *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/open_gospelstdlib_module.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/open_gospelstdlib_module.mli _build/default/test/syntax/open_gospelstdlib_module.mli.output
diff --git a/_build/default/test/syntax/open_gospelstdlib_module.mli b/_build/default/test/syntax/open_gospelstdlib_module.mli.output
index fe72e63..f0fdad5 100644
--- a/_build/default/test/syntax/open_gospelstdlib_module.mli
+++ b/_build/default/test/syntax/open_gospelstdlib_module.mli.output
@@ -1,3 +1,8 @@
type 'a t = 'a list


(*@ open Set *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/module_with.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/module_with.mli _build/default/test/syntax/module_with.mli.output
diff --git a/_build/default/test/syntax/module_with.mli b/_build/default/test/syntax/module_with.mli.output
index 61b82fe..3957203 100644
--- a/_build/default/test/syntax/module_with.mli
+++ b/_build/default/test/syntax/module_with.mli.output
@@ -7,3 +7,8 @@ module type B = sig


module C : A with type t = t
end
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/no_specification.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/no_specification.mli _build/default/test/syntax/no_specification.mli.output
diff --git a/_build/default/test/syntax/no_specification.mli b/_build/default/test/syntax/no_specification.mli.output
index 7477a25..ce0f23b 100644
--- a/_build/default/test/syntax/no_specification.mli
+++ b/_build/default/test/syntax/no_specification.mli.output
@@ -1 +1,6 @@
val f : int -> unit
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/modules2.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/modules2.mli _build/default/test/syntax/modules2.mli.output
diff --git a/_build/default/test/syntax/modules2.mli b/_build/default/test/syntax/modules2.mli.output
index b7f461b..04a9aa9 100644
--- a/_build/default/test/syntax/modules2.mli
+++ b/_build/default/test/syntax/modules2.mli.output
@@ -59,3 +59,8 @@ val default : MF.ft -> MF.ft
requires MF.fp1 y
ensures MF.fp2 x
*)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/partial_application.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/partial_application.mli _build/default/test/syntax/partial_application.mli.output
diff --git a/_build/default/test/syntax/partial_application.mli b/_build/default/test/syntax/partial_application.mli.output
index 22fce72..a8d89a5 100644
--- a/_build/default/test/syntax/partial_application.mli
+++ b/_build/default/test/syntax/partial_application.mli.output
@@ -2,3 +2,8 @@ val scalar_product : int list -> int -> int list


(*@ r = scalar_product v s
ensures List.map integer_of_int r = List.map ((fun x y -> x * integer_of_int y) (integer_of_int s)) v *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/stdlib_exceptions.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/stdlib_exceptions.mli _build/default/test/syntax/stdlib_exceptions.mli.output
diff --git a/_build/default/test/syntax/stdlib_exceptions.mli b/_build/default/test/syntax/stdlib_exceptions.mli.output
index 7bb8db9..5a168a6 100644
--- a/_build/default/test/syntax/stdlib_exceptions.mli
+++ b/_build/default/test/syntax/stdlib_exceptions.mli.output
@@ -9,3 +9,8 @@ val find : ('a -> bool) -> 'a list -> 'a
val invalid_arg : string -> 'a
(*@ raises  Invalid_argument _ -> true
ensures false *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/pure.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/pure.mli _build/default/test/syntax/pure.mli.output
diff --git a/_build/default/test/syntax/pure.mli b/_build/default/test/syntax/pure.mli.output
index ccd95db..dd88a20 100644
--- a/_build/default/test/syntax/pure.mli
+++ b/_build/default/test/syntax/pure.mli.output
@@ -3,3 +3,8 @@ val f : int -> int * int


val f : int -> int * int * int
(*@ pure *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/open_qualified.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/open_qualified.mli _build/default/test/syntax/open_qualified.mli.output
diff --git a/_build/default/test/syntax/open_qualified.mli b/_build/default/test/syntax/open_qualified.mli.output
index 3f2e886..ec7f177 100644
--- a/_build/default/test/syntax/open_qualified.mli
+++ b/_build/default/test/syntax/open_qualified.mli.output
@@ -4,3 +4,8 @@ type t4 = t3
type t5 = int Types_functions.t2


(*@ function f5 (x: 'a Types_functions.t2) : Types_functions.t1 *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/recursive_invariants.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/recursive_invariants.mli _build/default/test/syntax/recursive_invariants.mli.output
diff --git a/_build/default/test/syntax/recursive_invariants.mli b/_build/default/test/syntax/recursive_invariants.mli.output
index 191afa8..e887bfb 100644
--- a/_build/default/test/syntax/recursive_invariants.mli
+++ b/_build/default/test/syntax/recursive_invariants.mli.output
@@ -12,3 +12,8 @@ type u = private { tag : int; next : u }
val f : u -> u
(*@ y = f x
requires x.tag = 0 *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/type_decl.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/type_decl.mli _build/default/test/syntax/type_decl.mli.output
diff --git a/_build/default/test/syntax/type_decl.mli b/_build/default/test/syntax/type_decl.mli.output
index 9c44fc4..46422e3 100644
--- a/_build/default/test/syntax/type_decl.mli
+++ b/_build/default/test/syntax/type_decl.mli.output
@@ -43,3 +43,8 @@ and 'b t22 = C of 'b
type t23 = u
and u = C of v
and v = t23
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/vocal/Vector.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/vocal/Vector.mli _build/default/test/vocal/Vector.mli.output
diff --git a/_build/default/test/vocal/Vector.mli b/_build/default/test/vocal/Vector.mli.output
index 93c6ea6..39e2082 100644
--- a/_build/default/test/vocal/Vector.mli
+++ b/_build/default/test/vocal/Vector.mli.output
@@ -330,3 +330,8 @@ val unsafe_resize: 'a t -> int -> unit
val unsafe_get : 'a t -> int -> 'a
val unsafe_set : 'a t -> int -> 'a -> unit
*)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/type.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/type.mli _build/default/test/syntax/type.mli.output
diff --git a/_build/default/test/syntax/type.mli b/_build/default/test/syntax/type.mli.output
index 63c57c4..322ec22 100644
--- a/_build/default/test/syntax/type.mli
+++ b/_build/default/test/syntax/type.mli.output
@@ -1 +1,6 @@
type t
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/vocal/PairingHeap.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/vocal/PairingHeap.mli _build/default/test/vocal/PairingHeap.mli.output
diff --git a/_build/default/test/vocal/PairingHeap.mli b/_build/default/test/vocal/PairingHeap.mli.output
index 4a7c79f..76bd68e 100644
--- a/_build/default/test/vocal/PairingHeap.mli
+++ b/_build/default/test/vocal/PairingHeap.mli.output
@@ -63,3 +63,8 @@ end) : sig
ensures  forall y. y <> minimum h -> Bag.multiplicity y h'.bag = Bag.multiplicity y h.bag
ensures  Bag.cardinal h'.bag = Bag.cardinal h.bag - 1 *)
end
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/vocal/Mjrty.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/vocal/Mjrty.mli _build/default/test/vocal/Mjrty.mli.output
diff --git a/_build/default/test/vocal/Mjrty.mli b/_build/default/test/vocal/Mjrty.mli.output
index 1457939..3bddf84 100644
--- a/_build/default/test/vocal/Mjrty.mli
+++ b/_build/default/test/vocal/Mjrty.mli.output
@@ -26,3 +26,8 @@ val mjrty : string array -> string
ensures  2 * num a r 0 (Array.length a) > Array.length a
raises   Not_found ->
forall c. 2 * num a c 0 (Array.length a) <= Array.length a *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/vocal/RingBuffer.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/vocal/RingBuffer.mli _build/default/test/vocal/RingBuffer.mli.output
diff --git a/_build/default/test/vocal/RingBuffer.mli b/_build/default/test/vocal/RingBuffer.mli.output
index 532fb72..3dbf41c 100644
--- a/_build/default/test/vocal/RingBuffer.mli
+++ b/_build/default/test/vocal/RingBuffer.mli.output
@@ -62,3 +62,8 @@ val copy : 'a buffer -> 'a buffer
ensures b.capacity = r.capacity
ensures forall i. 0 <= i < length r.sequence ->
b.sequence[i] = r.sequence[i] *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/vocal/PriorityQueue.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/vocal/PriorityQueue.mli _build/default/test/vocal/PriorityQueue.mli.output
diff --git a/_build/default/test/vocal/PriorityQueue.mli b/_build/default/test/vocal/PriorityQueue.mli.output
index a6b2a36..9646a23 100644
--- a/_build/default/test/vocal/PriorityQueue.mli
+++ b/_build/default/test/vocal/PriorityQueue.mli.output
@@ -84,3 +84,8 @@ end) : sig
modifies h
ensures  h.bag = Bag.add x (old h).bag *)
end
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/predicates.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/predicates.mli _build/default/test/syntax/predicates.mli.output
diff --git a/_build/default/test/syntax/predicates.mli b/_build/default/test/syntax/predicates.mli.output
index 1561fea..158ea51 100644
--- a/_build/default/test/syntax/predicates.mli
+++ b/_build/default/test/syntax/predicates.mli.output
@@ -19,3 +19,8 @@ val merge : int array -> int array -> int array
(*@ requires n >= 0
variant n
ensures result >= 0 *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/vocal/Queue.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/vocal/Queue.mli _build/default/test/vocal/Queue.mli.output
diff --git a/_build/default/test/vocal/Queue.mli b/_build/default/test/vocal/Queue.mli.output
index dcfeadf..f9ff4f7 100644
--- a/_build/default/test/vocal/Queue.mli
+++ b/_build/default/test/vocal/Queue.mli.output
@@ -41,3 +41,8 @@ val transfer : 'a t -> 'a t -> unit
modifies q1.view, q2.view
ensures  q1.view = Sequence.empty
ensures  q2.view = old q2.view ++ old q1.view *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/types_functions2.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/types_functions2.mli _build/default/test/syntax/types_functions2.mli.output
diff --git a/_build/default/test/syntax/types_functions2.mli b/_build/default/test/syntax/types_functions2.mli.output
index 656fa8a..750ecea 100644
--- a/_build/default/test/syntax/types_functions2.mli
+++ b/_build/default/test/syntax/types_functions2.mli.output
@@ -30,3 +30,8 @@ type ('a, 'b) t7 = 'a t6
match x with
| {x;y} -> {x;y}
*)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/qualified.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/qualified.mli _build/default/test/syntax/qualified.mli.output
diff --git a/_build/default/test/syntax/qualified.mli b/_build/default/test/syntax/qualified.mli.output
index 2b86a3e..7e44580 100644
--- a/_build/default/test/syntax/qualified.mli
+++ b/_build/default/test/syntax/qualified.mli.output
@@ -1,3 +1,8 @@
(*@ type t3 = Open2.t2 *)


(*@ type t4 = Type.t *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/types_functions.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/types_functions.mli _build/default/test/syntax/types_functions.mli.output
diff --git a/_build/default/test/syntax/types_functions.mli b/_build/default/test/syntax/types_functions.mli.output
index 5d991d8..2ef13ba 100644
--- a/_build/default/test/syntax/types_functions.mli
+++ b/_build/default/test/syntax/types_functions.mli.output
@@ -6,3 +6,8 @@ type 'a t2
(*@ function f2 (x: int) : t1 *)


(*@ function f3 (x: int) : int t2 = f1 (f2 x) *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/syntax/types.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/syntax/types.mli _build/default/test/syntax/types.mli.output
diff --git a/_build/default/test/syntax/types.mli b/_build/default/test/syntax/types.mli.output
index 591c6c9..9d2b48b 100644
--- a/_build/default/test/syntax/types.mli
+++ b/_build/default/test/syntax/types.mli.output
@@ -2,3 +2,8 @@ type t = int -> int
type u = (int -> int) ref
type v = private { x : int -> int }
(*@ with self invariant self.x 0i = 0 *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/vocal/UnionFind.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/vocal/UnionFind.mli _build/default/test/vocal/UnionFind.mli.output
diff --git a/_build/default/test/vocal/UnionFind.mli b/_build/default/test/vocal/UnionFind.mli.output
index edd4eb7..b7fd9ef 100644
--- a/_build/default/test/vocal/UnionFind.mli
+++ b/_build/default/test/vocal/UnionFind.mli.output
@@ -121,3 +121,8 @@ val union : 'a elem -> 'a elem -> unit
uf1.img x = if mem x (old uf1.dom) then old (uf1.img x)
else old (uf2.img x)
*)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/vocal/Lists.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/vocal/Lists.mli _build/default/test/vocal/Lists.mli.output
diff --git a/_build/default/test/vocal/Lists.mli b/_build/default/test/vocal/Lists.mli.output
index faa877c..82859c2 100644
--- a/_build/default/test/vocal/Lists.mli
+++ b/_build/default/test/vocal/Lists.mli.output
@@ -24,3 +24,8 @@ val map : ('a -> 'b) -> 'a list -> 'b list
ensures forall i. 0 <= i < List.length l ->
List.nth r i = f (List.nth l i)
equivalent "List.rev (List.map f (List.rev l))" *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/vocal/FM19.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/vocal/FM19.mli _build/default/test/vocal/FM19.mli.output
diff --git a/_build/default/test/vocal/FM19.mli b/_build/default/test/vocal/FM19.mli.output
index f5c1463..fd7c297 100644
--- a/_build/default/test/vocal/FM19.mli
+++ b/_build/default/test/vocal/FM19.mli.output
@@ -110,3 +110,8 @@ val f : tt -> tt -> tt -> tt -> int -> tt * tt * int
requires true (* P in the paper *)
modifies p1, p2.left  consumes p3
ensures  true (* Q in the paper *) *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/vocal/HashTable.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/vocal/HashTable.mli _build/default/test/vocal/HashTable.mli.output
diff --git a/_build/default/test/vocal/HashTable.mli b/_build/default/test/vocal/HashTable.mli.output
index bcb99ca..f515b78 100644
--- a/_build/default/test/vocal/HashTable.mli
+++ b/_build/default/test/vocal/HashTable.mli.output
@@ -115,3 +115,8 @@ module Make (K : HashedType) : sig
(*@ b = mem h k
ensures b <-> h.view k <> [] *)
end
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/vocal/CountingSort.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/vocal/CountingSort.mli _build/default/test/vocal/CountingSort.mli.output
diff --git a/_build/default/test/vocal/CountingSort.mli b/_build/default/test/vocal/CountingSort.mli.output
index 3650081..e850840 100644
--- a/_build/default/test/vocal/CountingSort.mli
+++ b/_build/default/test/vocal/CountingSort.mli.output
@@ -30,3 +30,8 @@ val in_place_counting_sort : int -> int array -> unit
modifies a
ensures  sorted a
ensures  Array.permut (old a) a *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/vocal/ZipperList.mli", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/default/test/vocal/ZipperList.mli _build/default/test/vocal/ZipperList.mli.output
diff --git a/_build/default/test/vocal/ZipperList.mli b/_build/default/test/vocal/ZipperList.mli.output
index ef92442..e642cb7 100644
--- a/_build/default/test/vocal/ZipperList.mli
+++ b/_build/default/test/vocal/ZipperList.mli.output
@@ -92,3 +92,8 @@ val focused : 'a t -> 'a option
ensures match r with
| None   -> z.idx = Sequence.length z.seq
| Some x -> z.idx < Sequence.length z.seq /\ x = z.seq[z.idx] *)
+(* {gospel_expected|

+   [125] gospel: internal error, uncaught exception:

+                 Failure("output_value: not a binary channel")

+                 

+   |gospel_expected} *)

File "test/path/path_test.t", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/.sandbox/bf685a8d24c8320622def43e8ec1ff52/default/test/path/path_test.t _build/.sandbox/bf685a8d24c8320622def43e8ec1ff52/default/test/path/path_test.t.corrected
diff --git a/_build/.sandbox/bf685a8d24c8320622def43e8ec1ff52/default/test/path/path_test.t b/_build/.sandbox/bf685a8d24c8320622def43e8ec1ff52/default/test/path/path_test.t.corrected
index afb322e..4998e79 100644
--- a/_build/.sandbox/bf685a8d24c8320622def43e8ec1ff52/default/test/path/path_test.t
+++ b/_build/.sandbox/bf685a8d24c8320622def43e8ec1ff52/default/test/path/path_test.t.corrected
@@ -66,11 +66,9 @@ First, create a test artifact:
infix =
a_1
a_1
-  Gospelstdlib.integer_of_int
Path_test.M.f
n_1
Gospelstdlib.infix +
-  Gospelstdlib.integer_of_int
n_1
Path_test.M.Nested
Path_test.M.Nested.x_4
File "test/typechecker/process_gospel_file.t", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/.sandbox/9a23cbc2485553eeacbf2fbf40c76803/default/test/typechecker/process_gospel_file.t _build/.sandbox/9a23cbc2485553eeacbf2fbf40c76803/default/test/typechecker/process_gospel_file.t.corrected
diff --git a/_build/.sandbox/9a23cbc2485553eeacbf2fbf40c76803/default/test/typechecker/process_gospel_file.t b/_build/.sandbox/9a23cbc2485553eeacbf2fbf40c76803/default/test/typechecker/process_gospel_file.t.corrected
index 3e57eba..c2e96d2 100644
--- a/_build/.sandbox/9a23cbc2485553eeacbf2fbf40c76803/default/test/typechecker/process_gospel_file.t
+++ b/_build/.sandbox/9a23cbc2485553eeacbf2fbf40c76803/default/test/typechecker/process_gospel_file.t.corrected
@@ -15,7 +15,15 @@ the `.gospel` file.
>     ensures t.contents = Sequence.init n (fun _ -> a) *)
> EOF
$ gospel check --verbose foo.mli > foo
+  gospel: internal error, uncaught exception:

+          Failure("output_value: not a binary channel")

+          

+  [125]

$ gospel check --verbose foo.gospel > bar
+  gospel: internal error, uncaught exception:

+          Failure("input_value: not a binary channel")

+          

+  [125]

$ tail -q -n $(wc -l < bar) foo > baz
$ diff -s baz bar
Files baz and bar are identical
File "test/ppx/odoc_output.t", line 1, characters 0-0:
C:\cygwin64\bin\git.exe --no-pager diff --no-index --color=always -u --ignore-cr-at-eol _build/.sandbox/c1cc47ff0299e50a144b7d68dc7cbb15/default/test/ppx/odoc_output.t _build/.sandbox/c1cc47ff0299e50a144b7d68dc7cbb15/default/test/ppx/odoc_output.t.corrected
diff --git a/_build/.sandbox/c1cc47ff0299e50a144b7d68dc7cbb15/default/test/ppx/odoc_output.t b/_build/.sandbox/c1cc47ff0299e50a144b7d68dc7cbb15/default/test/ppx/odoc_output.t.corrected
index 7aa3bee..455e8bd 100644
--- a/_build/.sandbox/c1cc47ff0299e50a144b7d68dc7cbb15/default/test/ppx/odoc_output.t
+++ b/_build/.sandbox/c1cc47ff0299e50a144b7d68dc7cbb15/default/test/ppx/odoc_output.t.corrected
@@ -3,23 +3,40 @@ In this file, we are testing output from Odoc after the ppx rewriting.
First, we compile the file, running the source preprocessor and the ppx:


$ ocamlc -bin-annot -pp "gospel pps" -ppx "./pp.exe -as-ppx" odoc_of_gospel.mli
+  '.' is not recognized as an internal or external command,

+  operable program or batch file.

+  File "odoc_of_gospel.mli", line 1:

+  Error: Error while running external preprocessor

+  Command line: ./pp.exe -as-ppx "C:\Users\opam\AppData\Local\Temp\build_c803c7_dune\camlppx411ec9" "C:\Users\opam\AppData\Local\Temp\build_c803c7_dune\camlppx8630ff"

+  

+  [2]



Then run Odoc


$ odoc compile odoc_of_gospel.cmti
+  odoc: FILE argument: no 'odoc_of_gospel.cmti' file or directory

+  Usage: odoc compile [OPTION]… FILE

+  Try 'odoc compile --help' or 'odoc --help' for more information.

+  [2]



We test the html and the latex outputs


$ odoc html-generate odoc_of_gospel.odoc -o tmp
+  odoc: FILE.odocl argument: no 'odoc_of_gospel.odoc' file or directory

+  Usage: odoc html-generate [OPTION]… FILE.odocl

+  Try 'odoc html-generate --help' or 'odoc --help' for more information.

+  [2]

$ odoc latex-generate odoc_of_gospel.odoc -o tmp
+  odoc: FILE.odocl argument: no 'odoc_of_gospel.odoc' file or directory

+  Usage: odoc latex-generate [--extra-suffix=SUFFIX] [--syntax=SYNTAX] [--with-children=BOOL] [OPTION]… FILE.odocl

+  Try 'odoc latex-generate --help' or 'odoc --help' for more information.

+  [2]



As the output is not stable through odoc versions, we just check that the files
are generated:


$ find tmp -name \*.tex
-  tmp/Odoc_of_gospel.tex
$ find tmp -name \*.html
-  tmp/Odoc_of_gospel/index.html


This is not the case for the man output, here we can test the output.
Though, to be sure the diff is meaningful, let's set terminal's number of
@@ -27,51 +44,10 @@ columns:


$ export COLUMNS=80
$ odoc man-generate odoc_of_gospel.odoc -o tmp
+  odoc: FILE.odocl argument: no 'odoc_of_gospel.odoc' file or directory

+  Usage: odoc man-generate [--extra-suffix=SUFFIX] [--syntax=SYNTAX] [OPTION]… FILE.odocl

+  Try 'odoc man-generate --help' or 'odoc --help' for more information.

+  [2]

$ grep -v '^\.' tmp/Odoc_of_gospel.3o
-  
-  Odoc_of_gospel
-  \fBModule Odoc_of_gospel\fR
-  Module informal documentation
-  An axiom declaration
-  Gospel declaration:
-      axiom a : true 
-  A logical function declaration without definition
-  Gospel declaration:
-      function f : integer -> integer 
-  A logical function definition
-  Gospel declaration:
-      function g (i : integer) : integer = i + 1 
-  A logical function declaration with assertions
-  Gospel declaration:
-      function h (i : integer) : integer = i - 1 
-      requires i > 0
-      ensures result >= 0 
-  A logical predicate definition
-  Gospel declaration:
-      predicate p (i : integer) = i = 42 
-  A ghost type declaration
-  Gospel declaration:
-      type casper 
-  \f[CB]type\fR 'a t
-  A program type declaration with specifications
-  Gospel specification:
-      model m : 'a sequence
-      with x
-      invariant true 
-  
-  \f[CB]val\fR prog_fun : int \f[CB]\->\fR int
-  A program function with specifications
-  Gospel specification:
-      y = prog_fun x
-      requires true
-      ensures true 
-  
-  \f[CB]val\fR multiple_gospel_attribute : int \f[CB]\->\fR int
-  Gospel specification:
-      y = multiple_gospel_attribute x 
-  Gospel specification:
-      requires true 
-  Gospel specification:
-      ensures true 
-  
-  
+  grep: tmp/Odoc_of_gospel.3o: No such file or directory

+  [2]

"cd /cygdrive/c/Users/opam/src && opam exec -- dune build @install @check @runtest && rm -rf _build" failed with exit status 1
2024-11-08 00:17.49: Job failed: Failed: Build failed