2024-11-05 18:15.55: New job: test ocaml-gospel/gospel https://github.com/ocaml-gospel/gospel.git#refs/pull/423/head (ce369d0e7c0efd8cc62d2b21c4ce4f4aada46174) (test:windows-server-2022-5.2_opam-2.2) Base: windows-server-2022-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 ce369d0e cat > Dockerfile <<'END-OF-DOCKERFILE' FROM windows-server-2022-ocaml-5.2 # windows-server-2022-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/Documents/./ RUN opam pin add -yn gospel.dev '/Users/opam/Documents/./' 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/Documents RUN cd /cygdrive/c/Users/opam/Documents && opam exec -- dune build @install @check @runtest && rm -rf _build END-OF-DOCKERFILE docker build . END-REPRO-BLOCK 2024-11-05 18:15.55: Using cache hint "ocaml-gospel/gospel-windows-server-2022-ocaml-5.2-windows-server-2022-5.2_opam-2.2-a24b7a4f5e80f822ede4d47b0d94fed0" 2024-11-05 18:15.55: Using OBuilder spec: ((from windows-server-2022-ocaml-5.2) (comment windows-server-2022-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/Documents/./)) (run (network host) (shell "opam pin add -yn gospel.dev '/Users/opam/Documents/./'")) (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/Documents)) (run (shell "cd /cygdrive/c/Users/opam/Documents && opam exec -- dune build @install @check @runtest && rm -rf _build")) ) 2024-11-05 18:15.55: Waiting for resource in pool OCluster 2024-11-05 18:15.55: Waiting for worker… 2024-11-05 18:16.10: Got resource from pool OCluster Building on odawa HEAD is now at 4830a84 Map Module HEAD is now at ce369d0 Rewrite Map module (from windows-server-2022-ocaml-5.2) 2024-11-05 18:16.10 ---> using "d06d42c2ce15c2a01b42f8b17cebab1b932321c607f2ddc4dd5ddd2822e824d3" from cache /: (comment windows-server-2022-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-05 18:16.10 ---> using "106aa912871619930ac59aa254d609baa632011f4a9e74a854e122c44e73f2c7" 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-05 18:16.10 ---> using "1edf023df73483549607b8dd205269dd0f35f596214f7217de078e74cfde510e" 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-05 18:16.10 ---> using "b224a7bf51823dc957bb52ad05583a31ee1cd5e7b618e002cc7d8b3c11d6ee52" 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")) From https://github.com/ocaml/opam-repository * branch master -> FETCH_HEAD 56e31a3bc1..2dff29abd6 master -> origin/master 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-05 18:16.10 ---> using "d224a0b65a608c34ca80163d6c252553763652a9e83f2c604519cece6b9ebc51" from cache /: (copy (src gospel.opam) (dst /Users/opam/Documents/./)) 2024-11-05 18:16.10 ---> using "c6d7f6481d0f018373a905b1c5e30e7edda88a0a8ef518ab88d4a7694a6fe2ba" from cache /: (run (network host) (shell "opam pin add -yn gospel.dev '/Users/opam/Documents/./'")) [gospel.dev] synchronised (file://C:/Users/opam/Documents/.) gospel is now pinned to file://C:/Users/opam/Documents/. (version dev) 2024-11-05 18:16.10 ---> using "a7f67e180de97a61df0c417d815ec98c1be5ef86bf6c52285435f98edceb9ba6" 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-05 18:16.10 ---> using "987241cacbf14eca3d9f39766e0142b11a4cb12db8b1660a44566d88141a1c8f" 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 dune.3.16.1, dune-build-info.3.16.1 (cached) -> retrieved odoc.2.4.3, odoc-parser.2.4.3 (cached) -> retrieved pp_loc.2.1.0 (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 dune.3.16.1 -> installed astring.0.8.5 -> installed camlp-streams.5.0.1 -> installed cppo.1.7.0 -> installed fmt.0.9.0 -> installed menhirCST.20240715 -> installed ptime.1.2.0 -> installed uutf.1.0.3 -> installed ppx_derivers.1.2.1 -> installed pp_loc.2.1.0 -> 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 ocaml-compiler-libs.v0.17.0 -> installed fpath.0.7.3 -> installed re.1.12.0 -> installed sexplib0.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-05 18:16.10 ---> using "1153137c0cee985b3cb5c01227340e856a8e84a724912dc6fe6bd4339c8a6189" from cache /: (copy (src .) (dst /Users/opam/Documents)) 2024-11-05 18:16.42 ---> saved as "622a6a3b9909c1dbc6ce93ab1113044d7818bb8363a1bc3e5af9c04822393359" /: (run (shell "cd /cygdrive/c/Users/opam/Documents && 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_56a2bd_dune\ocamlppecdb29" 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 "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/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 "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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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_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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/790213cbd662c02a74d373a2dc76c504/default/test/path/path_test.t _build/.sandbox/790213cbd662c02a74d373a2dc76c504/default/test/path/path_test.t.corrected diff --git a/_build/.sandbox/790213cbd662c02a74d373a2dc76c504/default/test/path/path_test.t b/_build/.sandbox/790213cbd662c02a74d373a2dc76c504/default/test/path/path_test.t.corrected index afb322e..4998e79 100644 --- a/_build/.sandbox/790213cbd662c02a74d373a2dc76c504/default/test/path/path_test.t +++ b/_build/.sandbox/790213cbd662c02a74d373a2dc76c504/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/21482ba81e77254f62452e8ab4d798e6/default/test/typechecker/process_gospel_file.t _build/.sandbox/21482ba81e77254f62452e8ab4d798e6/default/test/typechecker/process_gospel_file.t.corrected diff --git a/_build/.sandbox/21482ba81e77254f62452e8ab4d798e6/default/test/typechecker/process_gospel_file.t b/_build/.sandbox/21482ba81e77254f62452e8ab4d798e6/default/test/typechecker/process_gospel_file.t.corrected index 3e57eba..c2e96d2 100644 --- a/_build/.sandbox/21482ba81e77254f62452e8ab4d798e6/default/test/typechecker/process_gospel_file.t +++ b/_build/.sandbox/21482ba81e77254f62452e8ab4d798e6/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/81df526f1dd17a39f3ecb08616953744/default/test/ppx/odoc_output.t _build/.sandbox/81df526f1dd17a39f3ecb08616953744/default/test/ppx/odoc_output.t.corrected diff --git a/_build/.sandbox/81df526f1dd17a39f3ecb08616953744/default/test/ppx/odoc_output.t b/_build/.sandbox/81df526f1dd17a39f3ecb08616953744/default/test/ppx/odoc_output.t.corrected index 7aa3bee..78f1f4a 100644 --- a/_build/.sandbox/81df526f1dd17a39f3ecb08616953744/default/test/ppx/odoc_output.t +++ b/_build/.sandbox/81df526f1dd17a39f3ecb08616953744/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_56a2bd_dune\camlppxe8f2ac" "C:\Users\opam\AppData\Local\Temp\build_56a2bd_dune\camlppx9bcd1e" + + [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/Documents && opam exec -- dune build @install @check @runtest && rm -rf _build" failed with exit status 1 2024-11-05 18:17.31: Job failed: Failed: Build failed