Build:
- 0
2026-10-22 02:38.11: New job: build why3.1.9.0 (7fbed74512c1)
2026-10-22 02:38.11: Waiting for resource in pool day11-builds
2026-10-22 04:26.56: Got resource from pool day11-builds
2026-10-22 04:26.56: [profile full] build why3.1.9.0
2026-10-22 04:26.56: build why3.1.9.0 (7fbed74512c1)
=== DEPENDENCIES (21 transitive) ===
base-threads.base ca51096a9c5b
base-unix.base 88a83b7ed333
compiler-cloning.enabled 1aa529c962c5
conf-gmp.5 d0211a82c71f
conf-pkg-config.5 26be2768a637
cppo.1.8.0 c8c950977062
dune.3.24.2 26ca61ae030f
menhir.20250912 7c2f2dfefc62
menhirCST.20250912 8322add54084
menhirLib.20250912 f1f1ce30d7d5
menhirSdk.20250912 ba2eb6a36b37
ocaml.5.5.1 b4ae7c74216a
ocaml-base-compiler.5.5.1 cae593a5c5a1
ocaml-compiler.5.5.1 22179c97969c
ocaml-compiler-libs.v0.17.0 596d9d0b2572
ocamlfind.1.9.9~preview 27baeb7469d0
ppx_derivers.1.2.1 5eb599f8af66
ppx_deriving.6.2.0 eaf878f28729
ppxlib.0.39.0 f671a9e391c2
sexplib0.v0.17.0 db7a30dcb806
zarith.1.14 bddddc68b0d9
=== STDOUT ===
Processing: [default: loading data]
[why3.1.9.0: dl]
[why3.1.9.0: extract]
-> retrieved why3.1.9.0 (https://opam.ocaml.org/cache)
[why3: touch configure]
+ /usr/bin/touch "configure" (CWD=/home/opam/.opam/default/.opam-switch/build/why3.1.9.0)
[why3: ./configure]
+ /home/opam/.opam/default/.opam-switch/build/why3.1.9.0/./configure "--prefix" "/home/opam/.opam/default" "--disable-frama-c" "--disable-coq-libs" "--disable-js-of-ocaml" "--disable-re" "--enable-ocamlfind" "--disable-mpfr" "--disable-zip" "--disable-hypothesis-selection" "--disable-stackify" "--disable-ide" (CWD=/home/opam/.opam/default/.opam-switch/build/why3.1.9.0)
- checking executable suffix... <none>
- checking for ocamlc... ocamlc
- checking ocaml os type... Unix
- checking for gcc... gcc
- checking whether the C compiler works... yes
- checking for C compiler default output file name... a.out
- checking for suffix of executables...
- checking whether we are cross compiling... no
- checking for suffix of object files... o
- checking whether the compiler supports GNU C... yes
- checking whether gcc accepts -g... yes
- checking for gcc option to enable C11 features... none needed
- checking for a race-free mkdir -p... /usr/bin/mkdir -p
- checking for a BSD-compatible install... /usr/bin/install -c
- configure: ocaml version is 5.5.1
- configure: ocaml library path is /home/opam/.opam/default/lib/ocaml
- checking for ocamlopt... ocamlopt
- checking ocamlopt version... ok
- checking for ocamlc.opt... ocamlc.opt
- checking ocamlc.opt version... ok
- checking for ocamlopt.opt... ocamlopt.opt
- checking ocamlc.opt version... ok
- checking for ocamldep... ocamldep
- checking for ocamldep.opt... ocamldep.opt
- checking for ocamllex... ocamllex
- checking for ocamllex.opt... ocamllex.opt
- checking for ocamlyacc... ocamlyacc
- checking for ocamldoc... ocamldoc
- checking for ocamldoc.opt... ocamldoc.opt
- checking for dune... dune
- checking for menhir... menhir
- checking for ocamlfind... ocamlfind
- checking for ppxlib using ocamlfind... yes
- checking for sphinx-build... no
- configure: WARNING: cannot find sphinx-build, documentation disabled.
- checking for emacs... no
- configure: WARNING: cannot find emacs, compilation of why3.elc disabled.
- checking for zarith using ocamlfind... yes
- checking for /home/opam/.opam/default/lib/zarith/z.cmi... yes
- checking for menhirLib using ocamlfind... yes
- checking for /home/opam/.opam/default/lib/menhirLib/menhirLib.cmi... yes
- checking for ppx_sexp_conv using ocamlfind... no
- checking for pvs... no
- checking for isabelle... no
- checking for javac... no
- checking for java... no
- configure: creating ./config.status
- config.status: creating Makefile
- config.status: creating src/config.sh
- config.status: creating src/dune
- config.status: creating src/util/dune
- config.status: creating src/why3deps/dune
- config.status: creating src/jessie/Makefile
- config.status: creating src/jessie/.merlin
- config.status: creating bin/dune
- config.status: creating lib/plugins/dune
- config.status: creating plugins/cfg/dune
- config.status: creating lib/coq/version
- config.status: creating lib/pvs/version
- config.status: creating bench/java/Makefile
- config.status: creating doc/javaexamples/Makefile
- config.status: executing chmod commands
-
- Summary
- -----------------------------------------
- Verbose make : no
- OCaml compiler : yes
- Version : 5.5.1
- Library path : /home/opam/.opam/default/lib/ocaml
- Ocamlfind : yes
- Native compilation : yes
- Memory profiling : no (disabled by default)
- PPX : yes
- S-expressions support : no (ppx_sexp_conv not found)
- Javascript support : no (disabled by user)
- MPFR support : no (disabled by user)
- Re support : no (disabled by user)
- Build environment
- OCaml OS Type : Unix
- Build environment type : Posix
- Components
- Why3 library : yes
- GTK IDE : no (disabled by user)
- Web IDE : no (Javascript support not available)
- Compressed sessions : no (disabled by user)
- Hypothesis selection : no (disabled by user)
- Stackify : no (disabled by user)
- Invariant inference(exp): no (disabled by default)
- Inference with BDDs(exp): no (disabled by default)
- Frama-C support : no
- Documentation : no (sphinx-build not found)
- Support for interactive proof assistants
- Coq : no (disabled by user)
- PVS : no (pvs not found)
- Isabelle : no (isabelle not found)
- Installable : yes
- Binary path : ${exec_prefix}/bin
- Library path : ${exec_prefix}/lib/why3
- Data path : ${prefix}/share/why3
- OCaml library path : /home/opam/.opam/default/lib/why3
- Relocatable : no
[why3: make all]
+ /usr/bin/make "DUNEJOBS=39" "all" "byte" (CWD=/home/opam/.opam/default/.opam-switch/build/why3.1.9.0)
- Generate src/util/config.ml
- Read 3 sample input sentences and 3 error messages.
- menhir --strict src/parser/parser_common.mly src/parser/parser.mly --base src/parser/parser --compile-errors \
- src/parser/handcrafted.messages > src/parser/parser_messages.ml
- Read 3 sample input sentences and 3 error messages.
- dune build --root . --only-packages=why3 -j 39 @opt why3.install
- File "src/util/vector.ml", line 21, characters 22-30:
- 21 | let create ?capacity:(capacity: (int) option) ~dummy:(dummy: 'a) : 'a t =
- ^^^^^^^^
- Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased.
- File "src/ppx/debug_optim.ml", line 14, characters 22-74:
- 14 | Exp.pexp_ident ~loc { txt = Ldot ((Lident "Debug"), "test_flag"); loc }
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 40 [name-out-of-scope]: this record of type Location.loc contains
- fields that are not visible in the current scope: txt loc.
- They will not be selected if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 14, characters 30-34:
- 14 | Exp.pexp_ident ~loc { txt = Ldot ((Lident "Debug"), "test_flag"); loc }
- ^^^^
- Warning 40 [name-out-of-scope]: Ldot was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 14, characters 37-43:
- 14 | Exp.pexp_ident ~loc { txt = Ldot ((Lident "Debug"), "test_flag"); loc }
- ^^^^^^
- Warning 40 [name-out-of-scope]: Lident was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", lines 16-17, characters 22-6:
- 16 | ......................{ txt = Ldot ((Lident "Debug"), "dprintf_no_expansion");
- 17 | loc }
- Warning 40 [name-out-of-scope]: this record of type Location.loc contains
- fields that are not visible in the current scope: txt loc.
- They will not be selected if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 16, characters 30-34:
- 16 | Exp.pexp_ident ~loc { txt = Ldot ((Lident "Debug"), "dprintf_no_expansion");
- ^^^^
- Warning 40 [name-out-of-scope]: Ldot was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 16, characters 37-43:
- 16 | Exp.pexp_ident ~loc { txt = Ldot ((Lident "Debug"), "dprintf_no_expansion");
- ^^^^^^
- Warning 40 [name-out-of-scope]: Lident was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 21, characters 3-7:
- 21 | (Ldot (Lident "Debug","dprintf"))
- ^^^^
- Warning 40 [name-out-of-scope]: Ldot was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 21, characters 9-15:
- 21 | (Ldot (Lident "Debug","dprintf"))
- ^^^^^^
- Warning 40 [name-out-of-scope]: Lident was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", lines 24-29, characters 8-38:
- 24 | ........{ pexp_desc =
- 25 | Pexp_apply ({ pexp_desc =
- 26 | Pexp_ident { txt = Ldot (Lident "Debug", "dprintf")}},
- 27 | ((flag :: _) as args))
- 28 | ;
- 29 | pexp_loc = loc }...
- Warning 40 [name-out-of-scope]: this record of type Astlib.Ast_502.Parsetree.expression
- contains fields that are not visible in the current scope:
- pexp_desc pexp_loc.
- They will not be selected if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 25, characters 10-20:
- 25 | Pexp_apply ({ pexp_desc =
- ^^^^^^^^^^
- Warning 40 [name-out-of-scope]: Pexp_apply was selected from type Astlib.Ast_502.Parsetree.expression_desc.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", lines 25-26, characters 22-77:
- 25 | ......................{ pexp_desc =
- 26 | Pexp_ident { txt = Ldot (Lident "Debug", "dprintf")}}.
- Warning 40 [name-out-of-scope]: this record of type Astlib.Ast_502.Parsetree.expression
- contains fields that are not visible in the current scope: pexp_desc.
- They will not be selected if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 26, characters 24-34:
- 26 | Pexp_ident { txt = Ldot (Lident "Debug", "dprintf")}},
- ^^^^^^^^^^
- Warning 40 [name-out-of-scope]: Pexp_ident was selected from type Astlib.Ast_502.Parsetree.expression_desc.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 26, characters 35-76:
- 26 | Pexp_ident { txt = Ldot (Lident "Debug", "dprintf")}},
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 40 [name-out-of-scope]: this record of type Location.loc contains
- fields that are not visible in the current scope: txt.
- They will not be selected if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 26, characters 43-47:
- 26 | Pexp_ident { txt = Ldot (Lident "Debug", "dprintf")}},
- ^^^^
- Warning 40 [name-out-of-scope]: Ldot was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 26, characters 49-55:
- 26 | Pexp_ident { txt = Ldot (Lident "Debug", "dprintf")}},
- ^^^^^^
- Warning 40 [name-out-of-scope]: Lident was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
- File "src/util/vector.ml", line 21, characters 22-30:
- 21 | let create ?capacity:(capacity: (int) option) ~dummy:(dummy: 'a) : 'a t =
- ^^^^^^^^
- Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased.
- File "src/ppx/debug_optim.ml", line 14, characters 22-74:
- 14 | Exp.pexp_ident ~loc { txt = Ldot ((Lident "Debug"), "test_flag"); loc }
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 40 [name-out-of-scope]: this record of type Location.loc contains
- fields that are not visible in the current scope: txt loc.
- They will not be selected if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 14, characters 30-34:
- 14 | Exp.pexp_ident ~loc { txt = Ldot ((Lident "Debug"), "test_flag"); loc }
- ^^^^
- Warning 40 [name-out-of-scope]: Ldot was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 14, characters 37-43:
- 14 | Exp.pexp_ident ~loc { txt = Ldot ((Lident "Debug"), "test_flag"); loc }
- ^^^^^^
- Warning 40 [name-out-of-scope]: Lident was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", lines 16-17, characters 22-6:
- 16 | ......................{ txt = Ldot ((Lident "Debug"), "dprintf_no_expansion");
- 17 | loc }
- Warning 40 [name-out-of-scope]: this record of type Location.loc contains
- fields that are not visible in the current scope: txt loc.
- They will not be selected if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 16, characters 30-34:
- 16 | Exp.pexp_ident ~loc { txt = Ldot ((Lident "Debug"), "dprintf_no_expansion");
- ^^^^
- Warning 40 [name-out-of-scope]: Ldot was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 16, characters 37-43:
- 16 | Exp.pexp_ident ~loc { txt = Ldot ((Lident "Debug"), "dprintf_no_expansion");
- ^^^^^^
- Warning 40 [name-out-of-scope]: Lident was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 21, characters 3-7:
- 21 | (Ldot (Lident "Debug","dprintf"))
- ^^^^
- Warning 40 [name-out-of-scope]: Ldot was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 21, characters 9-15:
- 21 | (Ldot (Lident "Debug","dprintf"))
- ^^^^^^
- Warning 40 [name-out-of-scope]: Lident was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", lines 24-29, characters 8-38:
- 24 | ........{ pexp_desc =
- 25 | Pexp_apply ({ pexp_desc =
- 26 | Pexp_ident { txt = Ldot (Lident "Debug", "dprintf")}},
- 27 | ((flag :: _) as args))
- 28 | ;
- 29 | pexp_loc = loc }...
- Warning 40 [name-out-of-scope]: this record of type Astlib.Ast_502.Parsetree.expression
- contains fields that are not visible in the current scope:
- pexp_desc pexp_loc.
- They will not be selected if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 25, characters 10-20:
- 25 | Pexp_apply ({ pexp_desc =
- ^^^^^^^^^^
- Warning 40 [name-out-of-scope]: Pexp_apply was selected from type Astlib.Ast_502.Parsetree.expression_desc.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", lines 25-26, characters 22-77:
- 25 | ......................{ pexp_desc =
- 26 | Pexp_ident { txt = Ldot (Lident "Debug", "dprintf")}}.
- Warning 40 [name-out-of-scope]: this record of type Astlib.Ast_502.Parsetree.expression
- contains fields that are not visible in the current scope: pexp_desc.
- They will not be selected if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 26, characters 24-34:
- 26 | Pexp_ident { txt = Ldot (Lident "Debug", "dprintf")}},
- ^^^^^^^^^^
- Warning 40 [name-out-of-scope]: Pexp_ident was selected from type Astlib.Ast_502.Parsetree.expression_desc.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 26, characters 35-76:
- 26 | Pexp_ident { txt = Ldot (Lident "Debug", "dprintf")}},
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 40 [name-out-of-scope]: this record of type Location.loc contains
- fields that are not visible in the current scope: txt.
- They will not be selected if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 26, characters 43-47:
- 26 | Pexp_ident { txt = Ldot (Lident "Debug", "dprintf")}},
- ^^^^
- Warning 40 [name-out-of-scope]: Ldot was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
-
- File "src/ppx/debug_optim.ml", line 26, characters 49-55:
- 26 | Pexp_ident { txt = Ldot (Lident "Debug", "dprintf")}},
- ^^^^^^
- Warning 40 [name-out-of-scope]: Lident was selected from type Astlib.Longident.t.
- It is not visible in the current scope, and will not be selected
- if the type becomes unknown.
- gcc -Wall -O -g -o src/server/logging.o -c src/server/logging.c
- gcc -Wall -O -g -o src/server/arraylist.o -c src/server/arraylist.c
- gcc -Wall -O -g -o src/server/options.o -c src/server/options.c
- gcc -Wall -O -g -o src/server/queue.o -c src/server/queue.c
- gcc -Wall -O -g -o src/server/readbuf.o -c src/server/readbuf.c
- gcc -Wall -O -g -o src/server/request.o -c src/server/request.c
- gcc -Wall -O -g -o src/server/proc.o -c src/server/proc.c
- gcc -Wall -O -g -o src/server/writebuf.o -c src/server/writebuf.c
- gcc -Wall -O -g -o src/server/server-unix.o -c src/server/server-unix.c
- gcc -Wall -O -g -o src/server/server-win.o -c src/server/server-win.c
- gcc -Wall -o lib/why3server src/server/logging.o src/server/arraylist.o src/server/options.o src/server/queue.o src/server/readbuf.o src/server/request.o src/server/proc.o src/server/writebuf.o src/server/server-unix.o src/server/server-win.o
- gcc -Wall -O -g -o src/server/cpulimit-unix.o -c src/server/cpulimit-unix.c
- gcc -Wall -O -g -o src/server/cpulimit-win.o -c src/server/cpulimit-win.c
- gcc -Wall -o lib/why3cpulimit src/server/cpulimit-unix.o src/server/cpulimit-win.o
- Generate drivers/coq-realizations.aux
- Generate drivers/pvs-realizations.aux
- Generate drivers/isabelle-realizations.aux
- dune build --root . --only-packages=why3 -j 39 @byte
- dune build --root . --only-packages=why3 -j 39 why3.install
-> compiled why3.1.9.0
[why3: make install]
+ /usr/bin/make "install" "install-lib" (CWD=/home/opam/.opam/default/.opam-switch/build/why3.1.9.0)
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/plugins
- /usr/bin/install -c -m 644 lib/plugins/genequlin.cma lib/plugins/dimacs.cma lib/plugins/tptp.cma lib/plugins/python.cma lib/plugins/microc.cma lib/plugins/coma.cma lib/plugins/cfg.cma lib/plugins/forward_propagation.cma lib/plugins/genequlin.cmxs lib/plugins/dimacs.cmxs lib/plugins/tptp.cmxs lib/plugins/python.cmxs lib/plugins/microc.cmxs lib/plugins/coma.cmxs lib/plugins/cfg.cmxs lib/plugins/forward_propagation.cmxs /home/opam/.opam/default/lib/why3/plugins
- /usr/bin/mkdir -p /home/opam/.opam/default/bin
- /usr/bin/install -c bin/why3.opt /home/opam/.opam/default/bin/why3
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/commands
- /usr/bin/install -c -m 644 bin/why3config.cmxs bin/why3execute.cmxs bin/why3extract.cmxs bin/why3prove.cmxs bin/why3realize.cmxs bin/why3replay.cmxs bin/why3show.cmxs bin/why3wc.cmxs bin/why3bench.cmxs /home/opam/.opam/default/lib/why3/commands
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3
- /usr/bin/install -c lib/why3server /home/opam/.opam/default/lib/why3/why3server
- /usr/bin/install -c lib/why3cpulimit /home/opam/.opam/default/lib/why3/why3cpulimit
- /usr/bin/install -c lib/why3-call-pvs /home/opam/.opam/default/lib/why3/why3-call-pvs
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/commands
- /usr/bin/install -c -m 644 bin/why3webserver.cmxs /home/opam/.opam/default/lib/why3/commands
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/commands
- /usr/bin/install -c -m 644 bin/why3session.cmxs /home/opam/.opam/default/lib/why3/commands
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/commands
- /usr/bin/install -c -m 644 bin/why3shell.cmxs /home/opam/.opam/default/lib/why3/commands
- cp -f bin/isabelle_client.opt /home/opam/.opam/default/bin/isabelle_client
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/commands
- /usr/bin/install -c -m 644 bin/why3pp.cmxs /home/opam/.opam/default/lib/why3/commands
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/commands
- /usr/bin/install -c -m 644 bin/why3doc.cmxs /home/opam/.opam/default/lib/why3/commands
- /usr/bin/mkdir -p /home/opam/.opam/default/share/why3
- /usr/bin/mkdir -p /home/opam/.opam/default/share/why3/vim
- /usr/bin/mkdir -p /home/opam/.opam/default/share/why3/vim/ftdetect
- /usr/bin/mkdir -p /home/opam/.opam/default/share/why3/vim/syntax
- /usr/bin/mkdir -p /home/opam/.opam/default/share/why3/lang
- /usr/bin/mkdir -p /home/opam/.opam/default/share/why3/stdlib
- /usr/bin/mkdir -p /home/opam/.opam/default/share/why3/stdlib/mach
- /usr/bin/mkdir -p /home/opam/.opam/default/share/why3/stdlib/mach/java
- /usr/bin/mkdir -p /home/opam/.opam/default/share/why3/drivers
- /usr/bin/mkdir -p /home/opam/.opam/default/share/why3/extraction_drivers
- /usr/bin/install -c -m 644 stdlib/*.mlw /home/opam/.opam/default/share/why3/stdlib
- /usr/bin/install -c -m 644 stdlib/mach/*.mlw /home/opam/.opam/default/share/why3/stdlib/mach
- /usr/bin/install -c -m 644 stdlib/mach/java/*.mlw /home/opam/.opam/default/share/why3/stdlib/mach/java
- /usr/bin/install -c -m 644 drivers/*.drv drivers/*.gen /home/opam/.opam/default/share/why3/drivers
- /usr/bin/install -c -m 644 extraction_drivers/*.drv /home/opam/.opam/default/share/why3/extraction_drivers
- /usr/bin/install -c -m 644 LICENSE /home/opam/.opam/default/share/why3/
- /usr/bin/install -c -m 644 share/provers-detection-data.conf /home/opam/.opam/default/share/why3/
- /usr/bin/install -c -m 644 share/why3session.dtd /home/opam/.opam/default/share/why3
- /usr/bin/install -c -m 644 share/Makefile.config /home/opam/.opam/default/share/why3
- /usr/bin/install -c -m 644 share/vim/ftdetect/why3.vim /home/opam/.opam/default/share/why3/vim/ftdetect/why3.vim
- /usr/bin/install -c -m 644 share/vim/syntax/why3.vim /home/opam/.opam/default/share/why3/vim/syntax/why3.vim
- /usr/bin/install -c -m 644 share/lang/why3.lang /home/opam/.opam/default/share/why3/lang/why3.lang
- /usr/bin/install -c -m 644 share/lang/why3c.lang /home/opam/.opam/default/share/why3/lang/why3c.lang
- /usr/bin/install -c -m 644 share/lang/why3py.lang /home/opam/.opam/default/share/why3/lang/why3py.lang
- /usr/bin/install -c -m 644 share/lang/coma.lang /home/opam/.opam/default/share/why3/lang/coma.lang
- /usr/bin/mkdir -p /home/opam/.opam/default/share/why3/drivers
- /usr/bin/install -c -m 644 drivers/coq-realizations.aux /home/opam/.opam/default/share/why3/drivers/
- /usr/bin/mkdir -p /home/opam/.opam/default/share/why3/drivers/
- /usr/bin/install -c -m 644 drivers/pvs-realizations.aux /home/opam/.opam/default/share/why3/drivers/
- /usr/bin/install -c -m 644 drivers/isabelle-realizations.aux /home/opam/.opam/default/share/why3/drivers/
- /usr/bin/mkdir -p /home/opam/.opam/default/share/emacs/site-lisp/
- /usr/bin/install -c -m 644 share/emacs/why3.el /home/opam/.opam/default/share/emacs/site-lisp/why3.el
- if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then \
- /usr/bin/install -c share/bash/why3 /etc/bash_completion.d; \
- fi
- dune install --root . --prefix /home/opam/.opam/default \
- --libdir /home/opam/.opam/default/lib --section lib,libexec why3
-> installed why3.1.9.0
[WARNING] Opam package conf-pkg-config.5 depends on the following system package that can no longer be found: pkg-config
=== STDERR ===
2026-10-22 04:29.17: OK: build why3.1.9.0 (runc: 130.3s, disk: 33KB)
2026-10-22 04:29.17: Job succeeded