Getting StartedDocumentation
Organisationsocaml-gospelgospel8542bf ()windows-server-2022-amd64-4.14_opam-2.3

windows-server-2022-amd64-4.14_opam-2.3

Link Copied
Code Copied

Logs

Show raw logs
2025-02-21 09:51.11: New job: test ocaml-gospel/gospel https://github.com/ocaml-gospel/gospel.git#refs/pull/433/head (8542bfbd061f512282451abc6576d0480f61dfd9) (windows-amd64:windows-server-2022-amd64-4.14_opam-2.3)
Base: windows-server-2022-amd64-ocaml-4.14
Opam project build


To reproduce locally:


git clone --recursive "https://github.com/ocaml-gospel/gospel.git" && cd "gospel" && git fetch origin "refs/pull/433/head" && git reset --hard 8542bfbd
cat > Dockerfile <<'END-OF-DOCKERFILE'
FROM windows-server-2022-amd64-ocaml-4.14
# windows-server-2022-amd64-4.14_opam-2.3
USER 1000:1000
ENV CLICOLOR_FORCE="1"
ENV OPAMCOLOR="always"
RUN ln -f /usr/bin/opam-2.3 /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 4022a684b64be8161a05cf897f492f8680792469 || git fetch origin master) && git reset -q --hard 4022a684b64be8161a05cf897f492f8680792469 && 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/./'
RUN echo '(lang dune 3.0)' > '/cygdrive/c/Users/opam/src/./dune-project'
ENV DEPS="arch-x86_64.1 astring.0.8.5 base-bigarray.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.8.0 crunch.4.0.0 dune.3.17.2 dune-build-info.3.17.2 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.4.14.2 ocaml-base-compiler.4.14.2 ocaml-compiler-libs.v0.12.4 ocaml-config.3 ocaml-env-mingw64.1 ocaml-options-vanilla.1 ocamlbuild.0.15.0 ocamlfind.1.9.8 odoc.2.4.4 odoc-parser.2.4.4 pp_loc.2.1.0 ppx_derivers.1.2.1 ppx_deriving.6.0.3 ppxlib.0.35.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.3 --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


2025-02-21 09:51.11: Using cache hint "ocaml-gospel/gospel-windows-server-2022-amd64-ocaml-4.14-windows-server-2022-amd64-4.14_opam-2.3-e5a692c01e0f76d26a252200d714df33"
2025-02-21 09:51.11: Using OBuilder spec:
((from windows-server-2022-amd64-ocaml-4.14)
(comment windows-server-2022-amd64-4.14_opam-2.3)
(user (uid 1000) (gid 1000))
(env CLICOLOR_FORCE 1)
(env OPAMCOLOR always)
(run (shell "ln -f /usr/bin/opam-2.3 /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 4022a684b64be8161a05cf897f492f8680792469 || git fetch origin master) && git reset -q --hard 4022a684b64be8161a05cf897f492f8680792469 && 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/./'"))
(run (network host)
(shell "echo '(lang dune 3.0)' > '/cygdrive/c/Users/opam/src/./dune-project'"))
(env DEPS "arch-x86_64.1 astring.0.8.5 base-bigarray.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.8.0 crunch.4.0.0 dune.3.17.2 dune-build-info.3.17.2 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.4.14.2 ocaml-base-compiler.4.14.2 ocaml-compiler-libs.v0.12.4 ocaml-config.3 ocaml-env-mingw64.1 ocaml-options-vanilla.1 ocamlbuild.0.15.0 ocamlfind.1.9.8 odoc.2.4.4 odoc-parser.2.4.4 pp_loc.2.1.0 ppx_derivers.1.2.1 ppx_deriving.6.0.3 ppxlib.0.35.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.3 --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"))
)


2025-02-21 09:51.11: Waiting for resource in pool OCluster
2025-02-21 09:51.11: Waiting for worker…
2025-02-21 10:05.56: Got resource from pool OCluster
Building on odawa
All commits already cached
HEAD is now at 8542bfb Update Changelog


(from windows-server-2022-amd64-ocaml-4.14)
2025-02-21 10:05.56 ---> using "55c9cbebb0e098c78ccc09b1cc6e84ec9f0bd2275b7cebf331cc913575946dc0" from cache


/: (comment windows-server-2022-amd64-4.14_opam-2.3)


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


/: (env CLICOLOR_FORCE 1)


/: (env OPAMCOLOR always)


/: (run (shell "ln -f /usr/bin/opam-2.3 /usr/bin/opam"))
2025-02-21 10:05.56 ---> using "fe3978d598c814685c6ee8922c3ae17147a3127f83af70ca6588d6b26847cd93" 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
2025-02-21 10:05.56 ---> using "0caf41f56a7e1f8a9ba062ae44d7d1f50471f3874e543c30c0d1c2b229f1e062" 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 4.14.2
2.3.0
2025-02-21 10:05.56 ---> using "6a7802e4db8e302e8ba8d87ff4e9376ae777099db0cd03bdab21ff27a442740c" 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 4022a684b64be8161a05cf897f492f8680792469 || git fetch origin master) && git reset -q --hard 4022a684b64be8161a05cf897f492f8680792469 && git log --no-decorate -n1 --oneline && opam update -u"))
From https://github.com/ocaml/opam-repository
* branch                  master     -> FETCH_HEAD
11bdbee611..4022a684b6  master     -> origin/master
4022a684b6 Merge pull request #27464 from hannesm/release-crunch-v4.0.0


<><> 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.
# To update the current shell environment, run: eval $(opam env)
2025-02-21 10:05.56 ---> using "00d834c335f737e603e2b17889bbb22ace83d491b5d2155623f1a5e0691af028" from cache


/: (copy (src gospel.opam) (dst /Users/opam/src/./))
2025-02-21 10:05.56 ---> using "7c11e76ac05866b09645934dbb4e7ec2416b0d79f08a195b3a93259ad1f11833" 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)
2025-02-21 10:06.02 ---> saved as "b2a6f609b775f3913864c9996872db3eb520e994e5684c6a5d070df900787328"


/: (run (network host)
(shell "echo '(lang dune 3.0)' > '/cygdrive/c/Users/opam/src/./dune-project'"))
2025-02-21 10:06.20 ---> saved as "e5439e9af239e6864f1c3b5edea05d57fca8df9d422608b4742b8b322f7458fd"


/: (env DEPS "arch-x86_64.1 astring.0.8.5 base-bigarray.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.8.0 crunch.4.0.0 dune.3.17.2 dune-build-info.3.17.2 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.4.14.2 ocaml-base-compiler.4.14.2 ocaml-compiler-libs.v0.12.4 ocaml-config.3 ocaml-env-mingw64.1 ocaml-options-vanilla.1 ocamlbuild.0.15.0 ocamlfind.1.9.8 odoc.2.4.4 odoc-parser.2.4.4 pp_loc.2.1.0 ppx_derivers.1.2.1 ppx_deriving.6.0.3 ppxlib.0.35.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.3 --depext-only -y gospel.dev $DEPS"))


<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[gospel.dev] synchronised (file://C:/Users/opam/src/.)


[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 4.14.2).
[NOTE] Package ocaml is already installed (current version is 4.14.2).
[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-bigarray is already installed (current version is base).
[NOTE] Package arch-x86_64 is already installed (current version is 1).
2025-02-21 10:06.44 ---> saved as "2ee1a593ea6c62855826f5e3141300898e1ab7045603bb7dc1a27f7f7b3490c7"


/: (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 4.14.2).
[NOTE] Package ocaml is already installed (current version is 4.14.2).
[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-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.8.0
- install crunch              4.0.0
- install dune                3.17.2
- install dune-build-info     3.17.2
- 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.12.4
- install ocamlbuild          0.15.0
- install ocamlfind           1.9.8
- install odoc                2.4.4
- install odoc-parser         2.4.4
- install pp_loc              2.1.0
- install ppx_derivers        1.2.1
- install ppx_deriving        6.0.3
- install ppxlib              0.35.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.8.0  (cached)
-> retrieved fmt.0.9.0  (cached)
-> retrieved fpath.0.7.3  (cached)
-> retrieved crunch.4.0.0  (https://github.com/mirage/ocaml-crunch/releases/download/v4.0.0/crunch-4.0.0.tbz)
-> retrieved menhir.20240715, menhirCST.20240715, menhirLib.20240715, menhirSdk.20240715  (cached)
-> retrieved ocaml-compiler-libs.v0.12.4  (cached)
-> retrieved ocamlbuild.0.15.0  (cached)
-> retrieved ocamlfind.1.9.8  (https://github.com/ocaml/ocamlfind/archive/refs/tags/findlib-1.9.8.tar.gz)
-> retrieved pp_loc.2.1.0  (cached)
-> retrieved ppx_derivers.1.2.1  (cached)
-> retrieved ppx_deriving.6.0.3  (cached)
-> retrieved odoc.2.4.4, odoc-parser.2.4.4  (cached)
-> retrieved dune.3.17.2, dune-build-info.3.17.2  (https://github.com/ocaml/dune/releases/download/3.17.2/dune-3.17.2.tbz)
-> retrieved ptime.1.2.0  (cached)
-> retrieved re.1.12.0  (cached)
-> retrieved seq.base  (cached)
-> installed seq.base
-> retrieved result.1.5  (cached)
-> retrieved sexplib0.v0.17.0  (cached)
-> retrieved stdlib-shims.0.3.0  (cached)
-> retrieved ppxlib.0.35.0  (https://github.com/ocaml-ppx/ppxlib/releases/download/0.35.0/ppxlib-0.35.0.tbz)
-> retrieved topkg.1.0.7  (cached)
-> retrieved tyxml.4.6.0  (cached)
-> retrieved uutf.1.0.3  (cached)
-> installed cmdliner.1.3.0
-> installed ocamlbuild.0.15.0
[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\4.14.2\.opam-switch\build\ocamlfind.1.9.8\src\findlib\ocamlfind.exe
[WARNING] Automatically adding .exe to C:\Users\opam\AppData\Local\opam\4.14.2\.opam-switch\build\ocamlfind.1.9.8\src\findlib\ocamlfind_opt.exe
[WARNING] C:\Users\opam\AppData\Local\opam\4.14.2\bin\safe_camlp4 is a script; the command won't be available
-> installed ocamlfind.1.9.8
-> installed topkg.1.0.7
-> installed uutf.1.0.3
-> installed astring.0.8.5
-> installed fmt.0.9.0
-> installed ptime.1.2.0
-> installed fpath.0.7.3
-> installed dune.3.17.2
-> installed camlp-streams.5.0.1
-> installed cppo.1.8.0
-> installed crunch.4.0.0
-> installed menhirCST.20240715
-> installed ppx_derivers.1.2.1
-> installed stdlib-shims.0.3.0
-> installed pp_loc.2.1.0
-> installed result.1.5
-> installed menhirLib.20240715
-> installed menhirSdk.20240715
-> installed sexplib0.v0.17.0
-> installed dune-build-info.3.17.2
-> installed re.1.12.0
-> installed ocaml-compiler-libs.v0.12.4
-> installed odoc-parser.2.4.4
-> installed tyxml.4.6.0
-> installed odoc.2.4.4
-> installed ppxlib.0.35.0
-> installed menhir.20240715
-> installed ppx_deriving.6.0.3
Done.
# To update the current shell environment, run: eval $(opam env)
2025-02-21 10:08.50 ---> saved as "dc8e530f62bacae668c8cdec8f48fb4039f887e02ab1858e1d0458f96acf430d"


/: (copy (src .) (dst /Users/opam/src))
2025-02-21 10:09.09 ---> saved as "ef99f40f7e161531412f984e6d90c3df96d2a0570433606b20693d71867a8500"


/: (run (shell "cd /cygdrive/c/Users/opam/src && opam exec -- dune build @install @check @runtest && rm -rf _build"))
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_d5f3e5_dune\ocamlpp2f9a6d"


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 4603246..2d2c057 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 "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 887a747..dcafbde 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/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..cc61e91 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/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_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 ac658c2..3450bc6 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_content = Sequence.map (fun (x, _) -> x) xs.list_content
*)
+(* {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 6eee4f6..dcb3670 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).v > 0 *)
+(* {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 36bb95d..34e00da 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/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 b7bbd59..9bfe86f 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.array_content
ensures  Sequence.permut (old a.array_content) a.array_content *)
+(* {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 08294e2..c189efc 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.v >= 0
| None -> true *)
+(* {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/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 5d4c885..be92ec0 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 Sequence._exists (fun (None | Some _) -> false) os.list_content
*)
+(* {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 ca85106..d6333a5 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_content = Sequence.map (fun (x, _, _) : 'a -> x) ys.list_content
*)
+(* {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/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/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/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 b0b2c48..409ef36 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/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 7d76ca8..483ce30 100644
--- a/_build/default/test/syntax/constants.mli
+++ b/_build/default/test/syntax/constants.mli.output
@@ -6,3 +6,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/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 c717c4e..6de25d6 100644
--- a/_build/default/test/syntax/bitvector.mli
+++ b/_build/default/test/syntax/bitvector.mli.output
@@ -24,3 +24,8 @@ val mem : int -> t -> bool
(*@ b = mem i bv
checks 0 <= i.v < bv.size.v
ensures b <-> mem i.v bv *)
+(* {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/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/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 a21c363..44317a6 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.v = x.v + y.v
ensures r.v > 2
ensures r.v = 3 *)
+(* {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 7eaacb0..f0bef3a 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.v = fibonacci i
requires b.v = fibonacci (i+1)
ensures r.v = fibonacci (i+n.v) *)
+(* {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 b43ad96..48349b1 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.v = pow 2 i
ensures x.v = pow 2 r.v *)
+(* {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/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 897266d..b14a0a6 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/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 667956f..1e73859 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/patterns/pattern_inlined_record.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/pattern_inlined_record.mli _build/default/test/patterns/pattern_inlined_record.mli.output
diff --git a/_build/default/test/patterns/pattern_inlined_record.mli b/_build/default/test/patterns/pattern_inlined_record.mli.output
index da067a3..0d80dd4 100644
--- a/_build/default/test/patterns/pattern_inlined_record.mli
+++ b/_build/default/test/patterns/pattern_inlined_record.mli.output
@@ -4,3 +4,8 @@
match a with
| A { a } -> a
*)
+(* {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/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/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/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/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/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/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/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 fa11257..0512fa8 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 Sequence.map (fun x -> x.v) r.list_content = Sequence.map ((fun x y -> x * y.v) s.v) v.list_content *)
+(* {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/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/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 bf0cfd5..06389ec 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/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/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/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 c73e8c2..424eb32 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/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/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/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/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 00d8320..a029279 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).v = 0 *)
+(* {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 2bb93bc..7eea9d2 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.v = 0 *)
+(* {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 1d6c568..c84c5d9 100644
--- a/_build/default/test/vocal/HashTable.mli
+++ b/_build/default/test/vocal/HashTable.mli.output
@@ -120,3 +120,8 @@ module Make (K : HashedType) : sig
(*@ b = mem h k
ensures b <-> h.view k <> Sequence.empty *)
end
+(* {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 7abc9dd..d89cad0 100644
--- a/_build/default/test/vocal/Lists.mli
+++ b/_build/default/test/vocal/Lists.mli.output
@@ -25,3 +25,8 @@ val map : ('a -> 'b) -> 'a list -> 'b list
ensures forall i. 0 <= i < Sequence.length l.list_content ->
r.list_content[i] = f (l.list_content[i])
equivalent "Sequence.rev (Sequence.map f (Sequence.rev l.list_content))" *)
+(* {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 e0c9ee9..f02f58a 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.array_content
ensures  sorted a.array_content
ensures  Sequence.permut (old a.array_content) a.array_content *)
+(* {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 fc2ed47..0efd58d 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/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 155edc8..7ae5c38 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.array_content r 0 (Sequence.length a.array_content) > Sequence.length a.array_content
raises   Not_found ->
forall c. 2 * num a.array_content c 0 (Sequence.length a.array_content) <= Sequence.length a.array_content *)
+(* {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 aa966bd..c04e1ca 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/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 57d0155..fa5e9cc 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/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 8ba8b90..733db41 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/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 ea93653..6d4b192 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/Order.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/Order.mli _build/default/test/vocal/Order.mli.output
diff --git a/_build/default/test/vocal/Order.mli b/_build/default/test/vocal/Order.mli.output
index 86f3f95..088e455 100644
--- a/_build/default/test/vocal/Order.mli
+++ b/_build/default/test/vocal/Order.mli.output
@@ -6,3 +6,8 @@
(cmp x y <= 0 -> cmp y z <  0 -> cmp x z <  0) /\
(cmp x y <  0 -> cmp y z <= 0 -> cmp x z <  0) /\
(cmp x y <  0 -> cmp y z <  0 -> cmp x z <  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/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/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 feed9dd..6f1967d 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/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/55d0950b4c3e1adcf3016bdf88761980/default/test/typechecker/process_gospel_file.t _build/.sandbox/55d0950b4c3e1adcf3016bdf88761980/default/test/typechecker/process_gospel_file.t.corrected
diff --git a/_build/.sandbox/55d0950b4c3e1adcf3016bdf88761980/default/test/typechecker/process_gospel_file.t b/_build/.sandbox/55d0950b4c3e1adcf3016bdf88761980/default/test/typechecker/process_gospel_file.t.corrected
index 7fa7722..19648d1 100644
--- a/_build/.sandbox/55d0950b4c3e1adcf3016bdf88761980/default/test/typechecker/process_gospel_file.t
+++ b/_build/.sandbox/55d0950b4c3e1adcf3016bdf88761980/default/test/typechecker/process_gospel_file.t.corrected
@@ -15,7 +15,15 @@ the `.gospel` file.
>     ensures t.contents = Sequence.init n.v (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/1255705d12ae53c81e5e9484224ba969/default/test/ppx/odoc_output.t _build/.sandbox/1255705d12ae53c81e5e9484224ba969/default/test/ppx/odoc_output.t.corrected
diff --git a/_build/.sandbox/1255705d12ae53c81e5e9484224ba969/default/test/ppx/odoc_output.t b/_build/.sandbox/1255705d12ae53c81e5e9484224ba969/default/test/ppx/odoc_output.t.corrected
index 7aa3bee..1d3af33 100644
--- a/_build/.sandbox/1255705d12ae53c81e5e9484224ba969/default/test/ppx/odoc_output.t
+++ b/_build/.sandbox/1255705d12ae53c81e5e9484224ba969/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_d5f3e5_dune\camlppxa886dc" "C:\Users\opam\AppData\Local\Temp\build_d5f3e5_dune\camlppxd88a97"

+  

+  [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
2025-02-21 10:09.43: Job failed: Failed: Build failed