leonardoalt · May 3, 2025 15:29
diff --git a/log b/log
 ./INSTALL                                 
 + cargo run --bin creusot-install --
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.14s
     Running `target/debug/creusot-install`
 Building prelude...
 Installing Why3 and Why3find...
 Package creusot-deps does not exist, create as a NEW package? [y/n] y
 The following additional pinnings are required by creusot-deps.dev:
  - why3.git-9c6f at git+https://gitlab.inria.fr/why3/why3.git#9c6f54fbb
  - why3-ide.git-9c6f at git+https://gitlab.inria.fr/why3/why3.git#9c6f54fbb
  - why3find.git-d227 at git+https://git.frama-c.com/pub/why3find.git#d227fc5
 Pin and install them? [y/n] y
 [why3.git-9c6f] synchronised (no changes)
 why3 is now pinned to git+https://gitlab.inria.fr/why3/why3.git#9c6f54fbb (version git-9c6f)
 [why3-ide.git-9c6f] synchronised (no changes)
 why3-ide is now pinned to git+https://gitlab.inria.fr/why3/why3.git#9c6f54fbb (version git-9c6f)
 [why3find.git-d227] synchronised (no changes)
 why3find is now pinned to git+https://git.frama-c.com/pub/why3find.git#d227fc5 (version git-d227)
 creusot-deps is now pinned to file:///home/leo/.local/share/creusot (version dev)

 <><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
 Switch invariant: []
 [NOTE] No invariant was set, you may want to use `opam switch set-invariant' to keep a stable compiler version on upgrades.
 The following actions will be performed:
 === install 46 packages
  ∗ base-bigarray        base              [required by cairo2]
  ∗ base-domains         base
  ∗ base-effects         base
  ∗ base-nnp             base
  ∗ base-threads         base              [required by dune]
  ∗ base-unix            base              [required by dune]
  ∗ cairo2               0.6.5             [required by lablgtk3]
  ∗ camlp-streams        5.0.1             [required by lablgtk3, lablgtk3-sourceview3]
  ∗ camlzip              1.13              [required by creusot-deps]
  ∗ conf-autoconf        0.2               [required by why3, why3-ide]
  ∗ conf-cairo           1                 [required by cairo2]
  ∗ conf-gmp             5                 [required by zarith]
  ∗ conf-gtk3            18                [required by lablgtk3]
  ∗ conf-gtksourceview3  0+2               [required by lablgtk3-sourceview3]
  ∗ conf-pkg-config      4                 [required by conf-zlib, zarith]
  ∗ conf-zlib            1                 [required by camlzip]
  ∗ conf-zmq             0.1               [required by zmq]
  ∗ creusot-deps         dev (pinned)
  ∗ csexp                1.5.2             [required by dune-private-libs]
  ∗ dune                 3.18.2            [required by ocamlgraph, why3find]
  ∗ dune-configurator    3.18.2            [required by zmq]
  ∗ dune-private-libs    3.18.2            [required by dune-site]
  ∗ dune-site            3.18.2            [required by why3find]
  ∗ dyn                  3.18.2            [required by dune-private-libs]
  ∗ lablgtk3             3.1.5             [required by why3-ide]
  ∗ lablgtk3-sourceview3 3.1.5             [required by why3-ide]
  ∗ menhir               20240715          [required by why3]
  ∗ menhirCST            20240715          [required by menhir]
  ∗ menhirLib            20240715          [required by menhir]
  ∗ menhirSdk            20240715          [required by menhir]
  ∗ ocaml                5.3.0             [required by creusot-deps]
  ∗ ocaml-config         3                 [required by ocaml]
  ∗ ocaml-system         5.3.0             [required by ocaml]
  ∗ ocamlfind            1.9.8             [required by why3, camlzip, why3-ide]
  ∗ ocamlgraph           2.2.0             [required by creusot-deps]
  ∗ ordering             3.18.2            [required by dyn, stdune]
  ∗ pp                   2.0.0             [required by dune-private-libs]
  ∗ seq                  base              [required by yojson]
  ∗ stdune               3.18.2            [required by dune-private-libs]
  ∗ terminal_size        0.2.0             [required by why3find]
  ∗ why3                 git-9c6f (pinned) [required by creusot-deps]
  ∗ why3-ide             git-9c6f (pinned) [required by creusot-deps]
  ∗ why3find             git-d227 (pinned) [required by creusot-deps]
  ∗ yojson               2.2.2             [required by why3find]
  ∗ zarith               1.14              [required by creusot-deps]
  ∗ zmq                  5.3.0             [required by why3find]

 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
 ∗ installed base-bigarray.base
 ∗ installed base-threads.base
 ∗ installed base-unix.base
 ⬇ retrieved camlp-streams.5.0.1  (cached)
 ⬇ retrieved conf-gmp.5  (cached)
 ∗ installed conf-pkg-config.4
 ∗ installed conf-gmp.5
 ∗ installed conf-gtk3.18
 ∗ installed conf-zlib.1
 ∗ installed conf-cairo.1
 ∗ installed conf-gtksourceview3.0+2
 ∗ installed conf-autoconf.0.2
 ⬇ retrieved conf-zmq.0.1  (https://opam.ocaml.org/cache)
 ⬇ retrieved camlzip.1.13  (https://opam.ocaml.org/cache)
 ⬇ retrieved cairo2.0.6.5  (https://opam.ocaml.org/cache)
 ∗ installed conf-zmq.0.1
 ⬇ retrieved csexp.1.5.2  (https://opam.ocaml.org/cache)
 ⬇ retrieved dune.3.18.2, dune-configurator.3.18.2, dune-private-libs.3.18.2, dune-site.3.18.2, dyn.3.18.2, ordering.3.18.2, stdune.3.18.2  (cached)
 ⬇ retrieved ocaml-config.3  (cached)
 ⬇ retrieved ocaml-system.5.3.0  (cached)
 ⬇ retrieved ocamlfind.1.9.8  (cached)
 ⬇ retrieved menhir.20240715, menhirCST.20240715, menhirLib.20240715, menhirSdk.20240715  (https://opam.ocaml.org/cache)
 ∗ installed ocaml-system.5.3.0
 ∗ installed ocaml-config.3
 ⬇ retrieved lablgtk3.3.1.5, lablgtk3-sourceview3.3.1.5  (https://opam.ocaml.org/cache)
 ⬇ retrieved seq.base  (cached)
 ⬇ retrieved ocamlgraph.2.2.0  (cached)
 ∗ installed ocaml.5.3.0
 ∗ installed base-domains.base
 ∗ installed base-effects.base
 ∗ installed base-nnp.base
 ∗ installed seq.base
 ⬇ retrieved terminal_size.0.2.0  (https://opam.ocaml.org/cache)
 ⬇ retrieved pp.2.0.0  (https://opam.ocaml.org/cache)
 ⬇ retrieved why3find.git-d227  (no changes)
 ⬇ retrieved yojson.2.2.2  (cached)
 ⬇ retrieved zarith.1.14  (cached)
 ⬇ retrieved zmq.5.3.0  (https://opam.ocaml.org/cache)
 ⬇ retrieved why3.git-9c6f  (no changes)
 ⬇ retrieved why3-ide.git-9c6f  (no changes)
 ∗ installed ocamlfind.1.9.8
 ∗ installed camlzip.1.13
 ∗ installed zarith.1.14
 ∗ installed dune.3.18.2
 ∗ installed csexp.1.5.2
 ∗ installed menhirCST.20240715
 ∗ installed camlp-streams.5.0.1
 ∗ installed menhirSdk.20240715
 ∗ installed pp.2.0.0
 ∗ installed menhirLib.20240715
 ∗ installed ordering.3.18.2
 ∗ installed terminal_size.0.2.0
 ∗ installed dune-configurator.3.18.2
 ∗ installed dyn.3.18.2
 ∗ installed yojson.2.2.2
 ∗ installed ocamlgraph.2.2.0
 ∗ installed zmq.5.3.0
 ∗ installed cairo2.0.6.5
 ∗ installed stdune.3.18.2
 ∗ installed dune-private-libs.3.18.2
 ∗ installed dune-site.3.18.2
 ∗ installed lablgtk3.3.1.5
 ∗ installed lablgtk3-sourceview3.3.1.5
 ∗ installed menhir.20240715
 [ERROR] The compilation of why3.git-9c6f failed at "make -j7 all byte".

 #=== ERROR while compiling why3.git-9c6f ======================================#
 # context     2.3.0 | linux/x86_64 |  | pinned(git+https://gitlab.inria.fr/why3/why3.git#9c6f54fbb#9c6f54fbbafd39bba127c64fbc33d02c38a3d455)
 # path        ~/.local/share/creusot/_opam/.opam-switch/build/why3.git-9c6f
 # command     ~/.opam/opam-init/hooks/sandbox.sh build make -j7 all byte
 # exit-code   2
 # env-file    ~/.opam/log/why3-50397-b38c88.env
 # output-file ~/.opam/log/why3-50397-b38c88.out
 ### output ###
 # src/server/cpulimit-unix.c:95:23: error: assignment to ‘__sighandler_t’ {aka ‘void (*)(int)’} from incompatible pointer type ‘void (*)(void)’ [-Wincompatible-pointer-types]
 # [...]
 #       |                       ^
 # src/server/cpulimit-unix.c:45:6: note: ‘wallclock_timelimit_reached’ declared here
 #    45 | void wallclock_timelimit_reached() {
 #       |      ^~~~~~~~~~~~~~~~~~~~~~~~~~~
 # In file included from src/server/cpulimit-unix.c:22:
 # /usr/include/signal.h:72:16: note: ‘__sighandler_t’ declared here
 #    72 | typedef void (*__sighandler_t) (int);
 #       |                ^~~~~~~~~~~~~~
 # Ocamlopt src/util/config.ml
 # make: *** [Makefile:805: src/server/cpulimit-unix.o] Error 1
 # make: *** Waiting for unfinished jobs....


 #=== ERROR while fetching sources for creusot-deps.dev ========================#
 OpamSolution.Fetch_fail("\"rsync\": command not found.")


 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
 ┌─ The following actions failed
 │ ⬇ fetch creusot-deps dev
 │ λ build why3         git-9c6f
 └─ 
 ┌─ The following changes have been performed (the rest was aborted)
 │ ∗ install base-bigarray        base
 │ ∗ install base-domains         base
 │ ∗ install base-effects         base
 │ ∗ install base-nnp             base
 │ ∗ install base-threads         base
 │ ∗ install base-unix            base
 │ ∗ install cairo2               0.6.5
 │ ∗ install camlp-streams        5.0.1
 │ ∗ install camlzip              1.13
 │ ∗ install conf-autoconf        0.2
 │ ∗ install conf-cairo           1
 │ ∗ install conf-gmp             5
 │ ∗ install conf-gtk3            18
 │ ∗ install conf-gtksourceview3  0+2
 │ ∗ install conf-pkg-config      4
 │ ∗ install conf-zlib            1
 │ ∗ install conf-zmq             0.1
 │ ∗ install csexp                1.5.2
 │ ∗ install dune                 3.18.2
 │ ∗ install dune-configurator    3.18.2
 │ ∗ install dune-private-libs    3.18.2
 │ ∗ install dune-site            3.18.2
 │ ∗ install dyn                  3.18.2
 │ ∗ install lablgtk3             3.1.5
 │ ∗ install lablgtk3-sourceview3 3.1.5
 │ ∗ install menhir               20240715
 │ ∗ install menhirCST            20240715
 │ ∗ install menhirLib            20240715
 │ ∗ install menhirSdk            20240715
 │ ∗ install ocaml                5.3.0
 │ ∗ install ocaml-config         3
 │ ∗ install ocaml-system         5.3.0
 │ ∗ install ocamlfind            1.9.8
 │ ∗ install ocamlgraph           2.2.0
 │ ∗ install ordering             3.18.2
 │ ∗ install pp                   2.0.0
 │ ∗ install seq                  base
 │ ∗ install stdune               3.18.2
 │ ∗ install terminal_size        0.2.0
 │ ∗ install yojson               2.2.2
 │ ∗ install zarith               1.14
 │ ∗ install zmq                  5.3.0
 └─ 
 # To update the current shell environment, run: eval $(opam env --switch=/home/leo/.local/share/creusot)
 Switch initialisation failed: clean up? ('n' will leave the switch partially installed) [y/n] y
 Error: Failed to create opam switch
	./INSTALL
	+ cargo run --bin creusot-install --
	Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.14s
	Running `target/debug/creusot-install`
	Building prelude...
	Installing Why3 and Why3find...
	Package creusot-deps does not exist, create as a NEW package? [y/n] y
	The following additional pinnings are required by creusot-deps.dev:
	- why3.git-9c6f at git+https://gitlab.inria.fr/why3/why3.git#9c6f54fbb
	- why3-ide.git-9c6f at git+https://gitlab.inria.fr/why3/why3.git#9c6f54fbb
	- why3find.git-d227 at git+https://git.frama-c.com/pub/why3find.git#d227fc5
	Pin and install them? [y/n] y
	[why3.git-9c6f] synchronised (no changes)
	why3 is now pinned to git+https://gitlab.inria.fr/why3/why3.git#9c6f54fbb (version git-9c6f)
	[why3-ide.git-9c6f] synchronised (no changes)
	why3-ide is now pinned to git+https://gitlab.inria.fr/why3/why3.git#9c6f54fbb (version git-9c6f)
	[why3find.git-d227] synchronised (no changes)
	why3find is now pinned to git+https://git.frama-c.com/pub/why3find.git#d227fc5 (version git-d227)
	creusot-deps is now pinned to file:///home/leo/.local/share/creusot (version dev)

	<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
	Switch invariant: []
	[NOTE] No invariant was set, you may want to use `opam switch set-invariant' to keep a stable compiler version on upgrades.
	The following actions will be performed:
	=== install 46 packages
	∗ base-bigarray base [required by cairo2]
	∗ base-domains base
	∗ base-effects base
	∗ base-nnp base
	∗ base-threads base [required by dune]
	∗ base-unix base [required by dune]
	∗ cairo2 0.6.5 [required by lablgtk3]
	∗ camlp-streams 5.0.1 [required by lablgtk3, lablgtk3-sourceview3]
	∗ camlzip 1.13 [required by creusot-deps]
	∗ conf-autoconf 0.2 [required by why3, why3-ide]
	∗ conf-cairo 1 [required by cairo2]
	∗ conf-gmp 5 [required by zarith]
	∗ conf-gtk3 18 [required by lablgtk3]
	∗ conf-gtksourceview3 0+2 [required by lablgtk3-sourceview3]
	∗ conf-pkg-config 4 [required by conf-zlib, zarith]
	∗ conf-zlib 1 [required by camlzip]
	∗ conf-zmq 0.1 [required by zmq]
	∗ creusot-deps dev (pinned)
	∗ csexp 1.5.2 [required by dune-private-libs]
	∗ dune 3.18.2 [required by ocamlgraph, why3find]
	∗ dune-configurator 3.18.2 [required by zmq]
	∗ dune-private-libs 3.18.2 [required by dune-site]
	∗ dune-site 3.18.2 [required by why3find]
	∗ dyn 3.18.2 [required by dune-private-libs]
	∗ lablgtk3 3.1.5 [required by why3-ide]
	∗ lablgtk3-sourceview3 3.1.5 [required by why3-ide]
	∗ menhir 20240715 [required by why3]
	∗ menhirCST 20240715 [required by menhir]
	∗ menhirLib 20240715 [required by menhir]
	∗ menhirSdk 20240715 [required by menhir]
	∗ ocaml 5.3.0 [required by creusot-deps]
	∗ ocaml-config 3 [required by ocaml]
	∗ ocaml-system 5.3.0 [required by ocaml]
	∗ ocamlfind 1.9.8 [required by why3, camlzip, why3-ide]
	∗ ocamlgraph 2.2.0 [required by creusot-deps]
	∗ ordering 3.18.2 [required by dyn, stdune]
	∗ pp 2.0.0 [required by dune-private-libs]
	∗ seq base [required by yojson]
	∗ stdune 3.18.2 [required by dune-private-libs]
	∗ terminal_size 0.2.0 [required by why3find]
	∗ why3 git-9c6f (pinned) [required by creusot-deps]
	∗ why3-ide git-9c6f (pinned) [required by creusot-deps]
	∗ why3find git-d227 (pinned) [required by creusot-deps]
	∗ yojson 2.2.2 [required by why3find]
	∗ zarith 1.14 [required by creusot-deps]
	∗ zmq 5.3.0 [required by why3find]

	<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
	∗ installed base-bigarray.base
	∗ installed base-threads.base
	∗ installed base-unix.base
	⬇ retrieved camlp-streams.5.0.1 (cached)
	⬇ retrieved conf-gmp.5 (cached)
	∗ installed conf-pkg-config.4
	∗ installed conf-gmp.5
	∗ installed conf-gtk3.18
	∗ installed conf-zlib.1
	∗ installed conf-cairo.1
	∗ installed conf-gtksourceview3.0+2
	∗ installed conf-autoconf.0.2
	⬇ retrieved conf-zmq.0.1 (https://opam.ocaml.org/cache)
	⬇ retrieved camlzip.1.13 (https://opam.ocaml.org/cache)
	⬇ retrieved cairo2.0.6.5 (https://opam.ocaml.org/cache)
	∗ installed conf-zmq.0.1
	⬇ retrieved csexp.1.5.2 (https://opam.ocaml.org/cache)
	⬇ retrieved dune.3.18.2, dune-configurator.3.18.2, dune-private-libs.3.18.2, dune-site.3.18.2, dyn.3.18.2, ordering.3.18.2, stdune.3.18.2 (cached)
	⬇ retrieved ocaml-config.3 (cached)
	⬇ retrieved ocaml-system.5.3.0 (cached)
	⬇ retrieved ocamlfind.1.9.8 (cached)
	⬇ retrieved menhir.20240715, menhirCST.20240715, menhirLib.20240715, menhirSdk.20240715 (https://opam.ocaml.org/cache)
	∗ installed ocaml-system.5.3.0
	∗ installed ocaml-config.3
	⬇ retrieved lablgtk3.3.1.5, lablgtk3-sourceview3.3.1.5 (https://opam.ocaml.org/cache)
	⬇ retrieved seq.base (cached)
	⬇ retrieved ocamlgraph.2.2.0 (cached)
	∗ installed ocaml.5.3.0
	∗ installed base-domains.base
	∗ installed base-effects.base
	∗ installed base-nnp.base
	∗ installed seq.base
	⬇ retrieved terminal_size.0.2.0 (https://opam.ocaml.org/cache)
	⬇ retrieved pp.2.0.0 (https://opam.ocaml.org/cache)
	⬇ retrieved why3find.git-d227 (no changes)
	⬇ retrieved yojson.2.2.2 (cached)
	⬇ retrieved zarith.1.14 (cached)
	⬇ retrieved zmq.5.3.0 (https://opam.ocaml.org/cache)
	⬇ retrieved why3.git-9c6f (no changes)
	⬇ retrieved why3-ide.git-9c6f (no changes)
	∗ installed ocamlfind.1.9.8
	∗ installed camlzip.1.13
	∗ installed zarith.1.14
	∗ installed dune.3.18.2
	∗ installed csexp.1.5.2
	∗ installed menhirCST.20240715
	∗ installed camlp-streams.5.0.1
	∗ installed menhirSdk.20240715
	∗ installed pp.2.0.0
	∗ installed menhirLib.20240715
	∗ installed ordering.3.18.2
	∗ installed terminal_size.0.2.0
	∗ installed dune-configurator.3.18.2
	∗ installed dyn.3.18.2
	∗ installed yojson.2.2.2
	∗ installed ocamlgraph.2.2.0
	∗ installed zmq.5.3.0
	∗ installed cairo2.0.6.5
	∗ installed stdune.3.18.2
	∗ installed dune-private-libs.3.18.2
	∗ installed dune-site.3.18.2
	∗ installed lablgtk3.3.1.5
	∗ installed lablgtk3-sourceview3.3.1.5
	∗ installed menhir.20240715
	[ERROR] The compilation of why3.git-9c6f failed at "make -j7 all byte".

	#=== ERROR while compiling why3.git-9c6f ======================================#
	# context 2.3.0 \| linux/x86_64 \| \| pinned(git+https://gitlab.inria.fr/why3/why3.git#9c6f54fbb#9c6f54fbbafd39bba127c64fbc33d02c38a3d455)
	# path ~/.local/share/creusot/_opam/.opam-switch/build/why3.git-9c6f
	# command ~/.opam/opam-init/hooks/sandbox.sh build make -j7 all byte
	# exit-code 2
	# env-file ~/.opam/log/why3-50397-b38c88.env
	# output-file ~/.opam/log/why3-50397-b38c88.out
	### output ###
	# src/server/cpulimit-unix.c:95:23: error: assignment to ‘__sighandler_t’ {aka ‘void ()(int)’} from incompatible pointer type ‘void ()(void)’ [-Wincompatible-pointer-types]
	# [...]
	# \| ^
	# src/server/cpulimit-unix.c:45:6: note: ‘wallclock_timelimit_reached’ declared here
	# 45 \| void wallclock_timelimit_reached() {
	# \| ^~~~~~~~~~~~~~~~~~~~~~~~~~~
	# In file included from src/server/cpulimit-unix.c:22:
	# /usr/include/signal.h:72:16: note: ‘__sighandler_t’ declared here
	# 72 \| typedef void (*__sighandler_t) (int);
	# \| ^~~~~~~~~~~~~~
	# Ocamlopt src/util/config.ml
	# make: *** [Makefile:805: src/server/cpulimit-unix.o] Error 1
	# make: *** Waiting for unfinished jobs....


	#=== ERROR while fetching sources for creusot-deps.dev ========================#
	OpamSolution.Fetch_fail("\"rsync\": command not found.")


	<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
	┌─ The following actions failed
	│ ⬇ fetch creusot-deps dev
	│ λ build why3 git-9c6f
	└─
	┌─ The following changes have been performed (the rest was aborted)
	│ ∗ install base-bigarray base
	│ ∗ install base-domains base
	│ ∗ install base-effects base
	│ ∗ install base-nnp base
	│ ∗ install base-threads base
	│ ∗ install base-unix base
	│ ∗ install cairo2 0.6.5
	│ ∗ install camlp-streams 5.0.1
	│ ∗ install camlzip 1.13
	│ ∗ install conf-autoconf 0.2
	│ ∗ install conf-cairo 1
	│ ∗ install conf-gmp 5
	│ ∗ install conf-gtk3 18
	│ ∗ install conf-gtksourceview3 0+2
	│ ∗ install conf-pkg-config 4
	│ ∗ install conf-zlib 1
	│ ∗ install conf-zmq 0.1
	│ ∗ install csexp 1.5.2
	│ ∗ install dune 3.18.2
	│ ∗ install dune-configurator 3.18.2
	│ ∗ install dune-private-libs 3.18.2
	│ ∗ install dune-site 3.18.2
	│ ∗ install dyn 3.18.2
	│ ∗ install lablgtk3 3.1.5
	│ ∗ install lablgtk3-sourceview3 3.1.5
	│ ∗ install menhir 20240715
	│ ∗ install menhirCST 20240715
	│ ∗ install menhirLib 20240715
	│ ∗ install menhirSdk 20240715
	│ ∗ install ocaml 5.3.0
	│ ∗ install ocaml-config 3
	│ ∗ install ocaml-system 5.3.0
	│ ∗ install ocamlfind 1.9.8
	│ ∗ install ocamlgraph 2.2.0
	│ ∗ install ordering 3.18.2
	│ ∗ install pp 2.0.0
	│ ∗ install seq base
	│ ∗ install stdune 3.18.2
	│ ∗ install terminal_size 0.2.0
	│ ∗ install yojson 2.2.2
	│ ∗ install zarith 1.14
	│ ∗ install zmq 5.3.0
	└─
	# To update the current shell environment, run: eval $(opam env --switch=/home/leo/.local/share/creusot)
	Switch initialisation failed: clean up? ('n' will leave the switch partially installed) [y/n] y
	Error: Failed to create opam switch