On This Page
package alt-ergo-free
alt-ergo-free 2.0.0
Error log
The package failed to build. The error log from opam follows.
[NOTE] Package dune is already installed (current version is 3.17.2).
[NOTE] Package ocamlfind is already installed (current version is 1.9.8).
The following actions will be performed:
=== install 11 packages
- install alt-ergo-free 2.0.0
- install camlzip 1.07
- install conf-autoconf 0.2
- install conf-gmp 4
- install conf-pkg-config 4
- install menhir 20211128
- install menhirLib 20211128
- install menhirSdk 20211128
- install num 1.5-1
- install ocplib-simplex 0.4.1
- install zarith 1.14
The following system packages will first need to be installed:
autoconf libgmp-dev pkg-config zlib1g-dev
<><> Handling external dependencies <><><><><><><><><><><><><><><><><><><><><><>
opam believes some required external dependencies are missing. opam can:
> 1. Run apt-get to install them (may need root/sudo access)
2. Display the recommended apt-get command and wait while you run it manually (e.g. in another terminal)
3. Continue anyway, and, upon success, permanently register that this external dependency is present, but not detectable
4. Abort the installation
[1/2/3/4] 1
+ /usr/bin/sudo "apt-get" "install" "-qq" "-yy" "autoconf" "libgmp-dev" "pkg-config" "zlib1g-dev"
- debconf: delaying package configuration, since apt-utils is not installed
- Selecting previously unselected package m4.
- (Reading database ...
(Reading database ... 5%
(Reading database ... 10%
(Reading database ... 15%
(Reading database ... 20%
(Reading database ... 25%
(Reading database ... 30%
(Reading database ... 35%
(Reading database ... 40%
(Reading database ... 45%
(Reading database ... 50%
(Reading database ... 55%
(Reading database ... 60%
(Reading database ... 65%
(Reading database ... 70%
(Reading database ... 75%
(Reading database ... 80%
(Reading database ... 85%
(Reading database ... 90%
(Reading database ... 95%
(Reading database ... 100%
(Reading database ... 18745 files and directories currently installed.)
- Preparing to unpack .../00-m4_1.4.19-3_amd64.deb ...
- Unpacking m4 (1.4.19-3) ...
- Selecting previously unselected package autoconf.
- Preparing to unpack .../01-autoconf_2.71-3_all.deb ...
- Unpacking autoconf (2.71-3) ...
- Selecting previously unselected package autotools-dev.
- Preparing to unpack .../02-autotools-dev_20220109.1_all.deb ...
- Unpacking autotools-dev (20220109.1) ...
- Selecting previously unselected package automake.
- Preparing to unpack .../03-automake_1%3a1.16.5-1.3_all.deb ...
- Unpacking automake (1:1.16.5-1.3) ...
- Selecting previously unselected package libgmpxx4ldbl:amd64.
- Preparing to unpack .../04-libgmpxx4ldbl_2%3a6.2.1+dfsg1-1.1_amd64.deb ...
- Unpacking libgmpxx4ldbl:amd64 (2:6.2.1+dfsg1-1.1) ...
- Selecting previously unselected package libgmp-dev:amd64.
- Preparing to unpack .../05-libgmp-dev_2%3a6.2.1+dfsg1-1.1_amd64.deb ...
- Unpacking libgmp-dev:amd64 (2:6.2.1+dfsg1-1.1) ...
- Selecting previously unselected package libpkgconf3:amd64.
- Preparing to unpack .../06-libpkgconf3_1.8.1-1_amd64.deb ...
- Unpacking libpkgconf3:amd64 (1.8.1-1) ...
- Selecting previously unselected package pkgconf-bin.
- Preparing to unpack .../07-pkgconf-bin_1.8.1-1_amd64.deb ...
- Unpacking pkgconf-bin (1.8.1-1) ...
- Selecting previously unselected package pkgconf:amd64.
- Preparing to unpack .../08-pkgconf_1.8.1-1_amd64.deb ...
- Unpacking pkgconf:amd64 (1.8.1-1) ...
- Selecting previously unselected package pkg-config:amd64.
- Preparing to unpack .../09-pkg-config_1.8.1-1_amd64.deb ...
- Unpacking pkg-config:amd64 (1.8.1-1) ...
- Selecting previously unselected package zlib1g-dev:amd64.
- Preparing to unpack .../10-zlib1g-dev_1%3a1.2.13.dfsg-1_amd64.deb ...
- Unpacking zlib1g-dev:amd64 (1:1.2.13.dfsg-1) ...
- Setting up m4 (1.4.19-3) ...
- Setting up autotools-dev (20220109.1) ...
- Setting up libpkgconf3:amd64 (1.8.1-1) ...
- Setting up libgmpxx4ldbl:amd64 (2:6.2.1+dfsg1-1.1) ...
- Setting up pkgconf-bin (1.8.1-1) ...
- Setting up autoconf (2.71-3) ...
- Setting up zlib1g-dev:amd64 (1:1.2.13.dfsg-1) ...
- Setting up automake (1:1.16.5-1.3) ...
- update-alternatives: using /usr/bin/automake-1.16 to provide /usr/bin/automake (automake) in auto mode
- Setting up libgmp-dev:amd64 (2:6.2.1+dfsg1-1.1) ...
- Setting up pkgconf:amd64 (1.8.1-1) ...
- Setting up pkg-config:amd64 (1.8.1-1) ...
- Processing triggers for libc-bin (2.36-9+deb12u9) ...
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved conf-gmp.4 (cached)
-> retrieved camlzip.1.07 (cached)
-> retrieved alt-ergo-free.2.0.0 (cached)
-> retrieved menhir.20211128, menhirLib.20211128, menhirSdk.20211128 (cached)
-> installed conf-autoconf.0.2
-> installed conf-gmp.4
-> installed conf-pkg-config.4
-> retrieved num.1.5-1 (cached)
-> retrieved ocplib-simplex.0.4.1 (cached)
-> retrieved zarith.1.14 (cached)
-> installed camlzip.1.07
-> installed menhirLib.20211128
-> installed menhirSdk.20211128
-> installed num.1.5-1
-> installed zarith.1.14
-> installed ocplib-simplex.0.4.1
-> installed menhir.20211128
[ERROR] The compilation of alt-ergo-free.2.0.0 failed at "make".
#=== ERROR while compiling alt-ergo-free.2.0.0 ================================#
# context 2.3.0 | linux/x86_64 | ocaml-base-compiler.4.14.2 | file:///src
# path ~/.opam/4.14/.opam-switch/build/alt-ergo-free.2.0.0
# command /usr/bin/make
# exit-code 2
# env-file ~/.opam/log/alt-ergo-free-113-94d8c3.env
# output-file ~/.opam/log/alt-ergo-free-113-94d8c3.out
### output ###
# autoconf
# configure.in:315: warning: AC_OUTPUT should be used without arguments.
# configure.in:315: You should run autoupdate.
# ./configure
# checking for ocp-ocamlc... no
# checking for ocamlc... ocamlc
# ocaml version is 4.14.2
# ocaml library path is /home/opam/.opam/4.14/lib/ocaml
# checking for ocamlfind... yes
# ocamlfind found zarith in -I /home/opam/.opam/4.14/lib/zarith
# ocamlfind found camlzip in -I /home/opam/.opam/4.14/lib/camlzip/../zip
# ocamlfind found ocplib-simplex in -I /home/opam/.opam/4.14/lib/ocplib-simplex
# checking for ocp-ocamlopt... no
# checking for ocamlopt... ocamlopt
# checking ocamlopt version... ok
# checking for ocp-ocamlc.opt... no
# checking for ocamlc.opt... ocamlc.opt
# checking ocamlc.opt version... ok
# checking for ocp-ocamlopt.opt... no
# checking for ocamlopt.opt... ocamlopt.opt
# checking ocamlc.opt version... ok
# checking for ocamldep... ocamldep
# checking for ocamllex... ocamllex
# checking for ocamllex.opt... ocamllex.opt
# checking for menhir... menhir
# ocamlfind: Package `lablgtk2.sourceview2' not found
# checking for /home/opam/.opam/4.14/lib/ocaml/lablgtk2/lablgtksourceview2.cma... no
# Will not be able to compile GUI. Please install the *liblablgtksourceview2-ocaml-dev* Debian package - or use the GODI caml package system *http://godi.ocaml-programming.de/* - or compile from sources *http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html*
# checking for ocamlweb... true
# checking platform... configure: creating ./config.status
# config.status: creating Makefile.configurable
# config.status: WARNING: 'Makefile.configurable.in' seems to ignore the --datarootdir setting
# menhir -v parsers/why/why_parser.mly
# ocamllex.opt parsers/why/why_lexer.mll > /dev/null
# ocamldep -slash -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I plugins/common -I plugins/satML -I plugins/fm-simplex lib/util/*.ml* lib/structures/*.ml* lib/reasoners/*.ml* lib/frontend/*.ml* tools/text/*.ml* \
# tools/gui/*.ml* parsers/why/*.ml* plugins/common/*ml* plugins/satML/*ml* plugins/fm-simplex/*ml* > .depend
# autoconf
# configure.in:315: warning: AC_OUTPUT should be used without arguments.
# configure.in:315: You should run autoupdate.
# ./configure
# checking for ocp-ocamlc... no
# checking for ocamlc... ocamlc
# ocaml version is 4.14.2
# ocaml library path is /home/opam/.opam/4.14/lib/ocaml
# checking for ocamlfind... yes
# ocamlfind found zarith in -I /home/opam/.opam/4.14/lib/zarith
# ocamlfind found camlzip in -I /home/opam/.opam/4.14/lib/camlzip/../zip
# ocamlfind found ocplib-simplex in -I /home/opam/.opam/4.14/lib/ocplib-simplex
# checking for ocp-ocamlopt... no
# checking for ocamlopt... ocamlopt
# checking ocamlopt version... ok
# checking for ocp-ocamlc.opt... no
# checking for ocamlc.opt... ocamlc.opt
# checking ocamlc.opt version... ok
# checking for ocp-ocamlopt.opt... no
# checking for ocamlopt.opt... ocamlopt.opt
# checking ocamlc.opt version... ok
# checking for ocamldep... ocamldep
# checking for ocamllex... ocamllex
# checking for ocamllex.opt... ocamllex.opt
# checking for menhir... menhir
# ocamlfind: Package `lablgtk2.sourceview2' not found
# checking for /home/opam/.opam/4.14/lib/ocaml/lablgtk2/lablgtksourceview2.cma... no
# Will not be able to compile GUI. Please install the *liblablgtksourceview2-ocaml-dev* Debian package - or use the GODI caml package system *http://godi.ocaml-programming.de/* - or compile from sources *http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html*
# checking for ocamlweb... true
# checking platform... configure: creating ./config.status
# config.status: creating Makefile.configurable
# config.status: WARNING: 'Makefile.configurable.in' seems to ignore the --datarootdir setting
# ocamlopt.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 @NUMLIB@ -I /home/opam/.opam/4.14/lib/zarith -I /home/opam/.opam/4.14/lib/camlzip/../zip -I /home/opam/.opam/4.14/lib/ocplib-simplex -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I plugins/common -I plugins/satML -I plugins/fm-simplex -for-pack AltErgo lib/util/config.ml
# don't know what to do with @NUMLIB@
# Usage: ocamlopt <options> <files>
# Try 'ocamlopt --help' for more information.
# -fPIC Generate position-independent machine code (default)
# -fno-PIC Generate position-dependent machine code
# -a Build a library
# -alert <list> Enable or disable alerts according to <list>:
# +<alertname> enable alert <alertname>
# -<alertname> disable alert <alertname>
# ++<alertname> treat <alertname> as fatal error
# --<alertname> treat <alertname> as non-fatal
# @<alertname> enable <alertname> and treat it as fatal error
# <alertname> can be 'all' to refer to all alert names
# -absname Show absolute filenames in error messages
# -afl-instrument Enable instrumentation for afl-fuzz
# -afl-inst-ratio Configure percentage of branches instrumented
# (advanced, see afl-fuzz docs for AFL_INST_RATIO)
# -annot (deprecated) Save information in <filename>.annot
# -bin-annot Save typedtree in <filename>.cmt
# -inline-branch-factor <n>|<round>=<n>[,...] Estimate the probability of a branch being cold as 1/(1+n) (used for inlining) (default 0.10)
# -c Compile only (do not link)
# -cc <command> Use <command> as the C compiler and linker
# -cclib <opt> Pass option <opt> to the C linker
# -ccopt <opt> Pass option <opt> to the C compiler and linker
# -clambda-checks Instrument clambda code with closure and field access checks (for debugging the compiler)
# -Oclassic Make inlining decisions at function definition time rather than at the call site (replicates previous behaviour of the compiler)
# -color {auto|always|never} Enable or disable colors in compiler messages
# The following settings are supported:
# auto use heuristics to enable colors only if supported
# always enable colors
# never disable colors
# The default setting is 'auto', and the current heuristic
# checks that the TERM environment variable exists and is
# not empty or "dumb", and that isatty(stderr) holds.
# If the option is not specified, these setting can alternatively
# be set through the OCAML_COLOR environment variable.
# -error-style {contextual|short} Control the way error messages and warnings are printed
# The following settings are supported:
# short only print the error and its location
# contextual like "short", but also display the source code
# snippet corresponding to the location of the error
# The default setting is 'contextual'.
# If the option is not specified, these setting can alternatively
# be set through the OCAML_ERROR_STYLE environment variable.
# -compact Optimize code size rather than speed
# -config Print configuration values and exit
# -config-var Print the value of a configuration variable, without a newline, and exit
# (print nothing and exit with error value if the variable does not exist)
# -dtypes (deprecated) same as -annot
# -for-pack <ident> Generate code that can later be `packed' with
# ocamlopt -pack -o <ident>.cmx
# -g Record debugging information for exception backtrace
# -function-sections Generate each function in a separate section if target supports it
# -stop-after {parsing|typing|scheduling|emit} Stop after the given compilation pass.
# -save-ir-after {scheduling} Save intermediate representation after the given compilation pass(may be specified more than once).
# -i Print inferred interface
# -I <dir> Add <dir> to the list of include directories
# -impl <file> Compile <file> as a .ml file
# -inline <n>|<round>=<n>[,...] Aggressiveness of inlining (default 1.25, higher numbers mean more aggressive)
# -inline-toplevel <n>|<round>=<n>[,...] Aggressiveness of inlining at toplevel (higher numbers mean more aggressive)
# -inline-alloc-cost <n>|<round>=<n>[,...] The cost of not removing an allocation during inlining (default 7, higher numbers more costly)
# -inline-branch-cost <n>|<round>=<n>[,...] The cost of not removing a conditional during inlining (default 5, higher numbers more costly)
# -inline-call-cost <n>|<round>=<n>[,...] The cost of not removing a call during inlining (default 5, higher numbers more costly)
# -inline-prim-cost <n>|<round>=<n>[,...] The cost of not removing a primitive during inlining (default 3, higher numbers more costly)
# -inline-indirect-cost <n>|<round>=<n>[,...] The cost of not removing an indirect call during inlining (default 4, higher numbers more costly)
# -inline-lifting-benefit <n>|<round>=<n>[,...] The benefit of lifting definitions to toplevel during inlining (default 1300, higher numbers more beneficial)
# -inlining-report Emit `.<round>.inlining' file(s) (one per round) showing the inliner's decisions
# -insn-sched Run the instruction scheduling pass (default)
# -intf <file> Compile <file> as a .mli file
# -intf-suffix <string> Suffix for interface files (default: .mli)
# -keep-docs Keep documentation strings in .cmi files
# -no-keep-docs Do not keep documentation strings in .cmi files (default)
# -keep-locs Keep locations in .cmi files (default)
# -no-keep-locs Do not keep locations in .cmi files
# -labels Use commuting label mode
# -linkall Link all modules, even unused ones
# -inline-max-depth <n>|<round>=<n>[,...] Maximum depth of search for inlining opportunities inside inlined functions (default 1)
# -alias-deps Do record dependencies for module aliases
# -no-alias-deps Do not record dependencies for module aliases
# -linscan Use the linear scan register allocator
# -app-funct Activate applicative functors
# -no-app-funct Deactivate applicative functors
# -no-float-const-prop Deactivate constant propagation for floating-point operations
# -noassert Do not compile assertion checks
# -noautolink Do not automatically link C libraries specified in .cmxa files
# -nodynlink Enable optimizations for code that will not be dynlinked
# -no-insn-sched Do not run the instruction scheduling pass
# -nolabels Ignore non-optional labels in types
# -nostdlib Do not add default directory to the list of include directories
# -nopervasives (undocumented)
# -no-unbox-free-vars-of-closures Do not unbox variables that will appear inside function closures
# -no-unbox-specialised-args Do not unbox arguments to which functions have been specialised
# -o <file> Set output file name to <file>
# -O2 Apply increased optimization for speed
# -O3 Apply aggressive optimization for speed (may significantly increase code size and compilation time)
# -opaque Does not generate cross-module optimization information
# (reduces necessary recompilation on module change)
# -open <module> Opens the module <module> before typing
# -output-obj Output an object file instead of an executable
# -output-complete-obj Output an object file, including runtime, instead of an executable
# -p (no longer supported)
# -pack Package the given .cmx files into one .cmx
# -plugin <plugin> (no longer supported)
# -pp <command> Pipe sources through preprocessor <command>
# -ppx <command> Pipe abstract syntax trees through preprocessor <command>
# -principal Check principality of type inference
# -no-principal Do not check principality of type inference (default)
# -rectypes Allow arbitrary recursive types
# -no-rectypes Do not allow arbitrary recursive types (default)
# -remove-unused-arguments Remove unused function arguments
# -rounds <n> Repeat tree optimization and inlining phases this many times (default 1). Rounds are numbered starting from zero.
# -runtime-variant <str> Use the <str> variant of the run-time system
# -with-runtime Include the runtime system in the generated program (default)
# -without-runtime Do not include the runtime system in the generated program.
# -S Keep intermediate assembly file
# -safe-string (was set when configuring the compiler)
# -shared Produce a dynlinkable plugin
# -short-paths Shorten paths in types
# -strict-sequence Left-hand part of a sequence must have type unit
# -no-strict-sequence Left-hand part of a sequence need not have type unit (default)
# -strict-formats Reject invalid formats accepted by legacy implementations
# (Warning: Invalid formats may behave differently from
# previous OCaml versions, and will become always-rejected
# in future OCaml versions. You should always use this flag
# to detect invalid formats so you can fix them.)
# -no-strict-formats Accept invalid formats accepted by legacy implementations (default)
# (Warning: Invalid formats may behave differently from
# previous OCaml versions, and will become always-rejected
# in future OCaml versions. You should never use this flag
# and instead fix invalid formats.)
# -thread (deprecated) same as -I +threads
# -unbox-closures Pass free variables via specialised arguments rather than closures
# -unbox-closures-factor <n > 0> Scale the size threshold above which unbox-closures will slow down indirect calls rather than duplicating a function (default 10)
# -inline-max-unroll <n>|<round>=<n>[,...] Unroll recursive functions at most this many times (default 0)
# -unboxed-types unannotated unboxable types will be unboxed
# -no-unboxed-types unannotated unboxable types will not be unboxed (default)
# -unsafe Do not compile bounds checking on array and string access
# -unsafe-string (option not available)
# -v Print compiler version and location of standard library and exit
# -verbose Print calls to external commands
# -version Print version and exit
# --version Print version and exit
# -vnum Print version number and exit
# -w <list> Enable or disable warnings according to <list>:
# +<spec> enable warnings in <spec>
# -<spec> disable warnings in <spec>
# @<spec> enable warnings in <spec> and treat them as errors
# <spec> can be:
# <num> a single warning number
# <num1>..<num2> a range of consecutive warning numbers
# <letter> a predefined set
# default setting is "+a-4-7-9-27-29-30-32..42-44-45-48-50-60-66..70"
# -warn-error <list> Enable or disable error status for warnings according
# to <list>. See option -w for the syntax of <list>.
# Default setting is "-a+31"
# -warn-help Show description of warning numbers
# -where Print location of standard library and exit
# - <file> Treat <file> as a file name (even if it starts with `-')
# -match-context-rows <n> (advanced, see manual section 11.2.)
# -dno-unique-ids (undocumented)
# -dunique-ids (undocumented)
# -dno-locations (undocumented)
# -dlocations (undocumented)
# -dsource (undocumented)
# -dparsetree (undocumented)
# -dtypedtree (undocumented)
# -dshape (undocumented)
# -drawlambda (undocumented)
# -dlambda (undocumented)
# -drawclambda (undocumented)
# -dclambda (undocumented)
# -dcmm-invariants Extra sanity checks on Cmm
# -dflambda Print Flambda terms
# -drawflambda Print Flambda terms after closure conversion
# -dflambda-invariants Check Flambda invariants around each pass
# -dflambda-no-invariants Do not Check Flambda invariants around each pass
# -dflambda-let <stamp> Print when the given Flambda [Let] is created
# -dflambda-verbose Print Flambda terms including around each pass
# -dcmm (undocumented)
# -dsel (undocumented)
# -dcombine (undocumented)
# -dcse (undocumented)
# -dlive (undocumented)
# -dspill (undocumented)
# -dsplit (undocumented)
# -dinterf (undocumented)
# -dprefer (undocumented)
# -dalloc (undocumented)
# -dreload (undocumented)
# -dscheduling (undocumented)
# -dlinear (undocumented)
# -dinterval (undocumented)
# -dstartup (undocumented)
# -dtimings Print timings information for each pass
# -dprofile Print performance information for each pass
# The columns are: time alloc top-heap absolute-top-heap.
# -dump-into-file dump output like -dlambda into <target>.dump
# -dump-dir <dir> dump output like -dlambda into <dir>/<target>.dump
# -dump-pass Record transformations performed by these passes:
# unbox-closures unbox-specialised-args unbox-free-vars-of-closures
# remove-free-vars-equal-to-args remove-unused-arguments unused-arguments
# -args <file> Read additional newline-terminated command line arguments
# from <file>
# -args0 <file> Read additional null character terminated command line arguments
# from <file>
# -depend <options> Compute dependencies (use 'ocamlopt -depend -help' for details)
# -help Display this list of options
# --help Display this list of options
# make: *** [Makefile.users:273: lib/util/config.cmx] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build alt-ergo-free 2.0.0
+-
+- The following changes have been performed
| - install camlzip 1.07
| - install conf-autoconf 0.2
| - install conf-gmp 4
| - install conf-pkg-config 4
| - install menhir 20211128
| - install menhirLib 20211128
| - install menhirSdk 20211128
| - install num 1.5-1
| - install ocplib-simplex 0.4.1
| - install zarith 1.14
+-
# To update the current shell environment, run: eval $(opam env)
The former state can be restored with:
/usr/bin/opam switch import "/home/opam/.opam/4.14/.opam-switch/backup/state-20250205160546.export"
On This Page