(2020-09-25 05:58:45 UTC)
# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-m4 1 Virtual package relying on m4
coq 8.10.0 Formal proof management system
num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.07.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.07.1 Official release 4.07.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.8.1 A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: [
"Érik Martin-Dorel <erik.martin-dorel@irit.fr>"
"Pierre Roux <pierre.roux@onera.fr>"
]
homepage: "https://sourcesup.renater.fr/validsdp/"
dev-repo: "git+https://github.com/validsdp/validsdp.git"
bug-reports: "https://github.com/validsdp/validsdp/issues"
license: "LGPL-2.1-or-later"
build: [
["sh" "-c" "./configure"]
[make "-j%{jobs}%"]
]
install: [make "install"]
depends: [
"ocaml"
"coq" {>= "8.7" & < "8.11~"}
"coq-bignums"
"coq-flocq" {>= "3.1.0"}
"coq-interval" {>= "3.4.0" & < "4~"}
"coq-mathcomp-field" {>= "1.8" & < "1.10~"}
"coq-libvalidsdp" {= "0.6.0"}
"coq-mathcomp-multinomials" {>= "1.2"}
"coq-coqeal" {>= "1.0.0"}
"coq-paramcoq" {>= "1.1.0"}
"osdp" {>= "1.0"}
"ocamlfind" {build}
"conf-autoconf" {build}
]
synopsis: "ValidSDP"
description: """
ValidSDP is a library for the Coq formal proof assistant. It provides
reflexive tactics to prove multivariate inequalities involving
real-valued variables and rational constants, using SDP solvers as
untrusted back-ends and verified checkers based on libValidSDP.
Once installed, you can import the following modules:
From Coq Require Import Reals.
From ValidSDP Require Import validsdp.
"""
tags: [
"keyword:libValidSDP"
"keyword:ValidSDP"
"keyword:floating-point arithmetic"
"keyword:Cholesky decomposition"
"category:ValidSDP"
"category:Miscellaneous/Coq Extensions"
"logpath:ValidSDP"
]
authors: [
"Érik Martin-Dorel <erik.martin-dorel@irit.fr>"
"Pierre Roux <pierre.roux@onera.fr>"
]
url {
src: "https://github.com/validsdp/validsdp/releases/download/v0.6.0/validsdp-0.6.0.tar.gz"
checksum: "sha256=ba7de610de209cce431bc93ff599ac21eb14d649a815ec9cfae27e064d0ea3bf"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-validsdp.0.6.0 coq.8.10.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 2h opam install -y --deps-only coq-validsdp.0.6.0 coq.8.10.0opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-validsdp.0.6.0 coq.8.10.0# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-autoconf 0.1 Virtual package relying on autoconf installation conf-csdp 1 Virtual package relying on a CSDP binary system installation conf-findutils 1 Virtual package relying on findutils conf-g++ 1.0 Virtual package relying on the g++ compiler (for C++) conf-gmp 2 Virtual package relying on a GMP lib system installation conf-m4 1 Virtual package relying on m4 conf-perl 1 Virtual package relying on perl conf-which 1 Virtual package relying on which coq 8.10.0 Formal proof management system coq-bignums 8.10.0 Bignums, the Coq library of arbitrary large numbers coq-coqeal 1.0.2 CoqEAL - The Coq Effective Algebra Library coq-coquelicot 3.1.0 A Coq formalization of real analysis compatible with the standard library coq-flocq 3.3.1 A formalization of floating-point arithmetic for the Coq system coq-interval 3.4.2 A Coq tactic for proving bounds on real-valued expressions automatically coq-libvalidsdp 0.6.0 LibValidSDP coq-mathcomp-algebra 1.9.0 Mathematical Components Library on Algebra coq-mathcomp-bigenough 1.0.0 A small library to do epsilon - N reasonning coq-mathcomp-field 1.9.0 Mathematical Components Library on Fields coq-mathcomp-fingroup 1.9.0 Mathematical Components Library on finite groups coq-mathcomp-finmap 1.3.4 Finite sets, finite maps, finitely supported functions, orders coq-mathcomp-multinomials 1.4 A Multivariate polynomial Library for the Mathematical Components Library coq-mathcomp-solvable 1.9.0 Mathematical Components Library on finite groups (II) coq-mathcomp-ssreflect 1.9.0 Small Scale Reflection coq-paramcoq 1.1.2+coq8.10 Plugin for generating parametricity statements to perform refinement proofs num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.07.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.07.1 Official release 4.07.1 ocaml-config 1 OCaml Switch Configuration ocamlbuild 0.14.0 OCamlbuild is a build system with builtin rules to easily build most OCaml projects. ocamlfind 1.8.1 A library manager for OCaml ocplib-simplex 0.4 A library implementing a simplex algorithm, in a functional style, for solving systems of linear inequalities and optimizing linear objective functions osdp 1.0.0 OCaml Interface to SDP solvers zarith 1.10 Implements arithmetic and logical operations over arbitrary-precision integers [NOTE] Package coq is already installed (current version is 8.10.0). The following actions will be performed: - install coq-validsdp 0.6.0 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-validsdp.0.6.0: http] [coq-validsdp.0.6.0] downloaded from https://github.com/validsdp/validsdp/releases/download/v0.6.0/validsdp-0.6.0.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-validsdp: sh] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "sh" "-c" "./configure" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-validsdp.0.6.0) - checking for ocamlc... ocamlc - checking for coqc... coqc - checking Coq version... 8.10.0 - checking for ocamlfind... ocamlfind - checking for Mathcomp... - yes - checking for Flocq... - yes - checking for Coq-interval... - yes - checking for Multinomials... - yes - checking for CoqEAL... - yes - checking for OSDP... 1.0.0 - checking for coq-bignums... - yes - checking for libValidSDP... - yes - checking for sdpa... no - configure: Optional dependency sdpa was not found. - configure: creating ./config.status - config.status: creating Makefile - config.status: creating _CoqProject - - Now run 'make && make install' to build and install ValidSDP 0.6.0 - (or run 'make help' to get for more info on the available rules) - Processing 1/2: [coq-validsdp: make] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j7" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-validsdp.0.6.0) - rm -f plugins/soswitness/src/soswitness.mlg - cp -f -- plugins/soswitness/src/soswitness_v810.mlg plugins/soswitness/src/soswitness.mlg - chmod a-w plugins/soswitness/src/soswitness.mlg - /home/bench/.opam/ocaml-base-compiler.4.07.1/bin/coq_makefile \ - -I "/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/zarith" \ - -I "/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/ocplib-simplex" \ - -I "/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/osdp" \ - -f _CoqProject -o Makefile.coq - # FIXME: This sed hack is fragile (if we do "make -B" for example) - sed -e 's/-linkall -shared -o $@ $</-linkall -shared -o $@ zarith.cmxa ocplibSimplex.cmxa osdp.cmxa $</' -i Makefile.coq - make -f Makefile.coq all - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-validsdp.0.6.0' - COQDEP VFILES - COQPP plugins/soswitness/src/soswitness.mlg - COQDEP plugins/soswitness/src/soswitness.mllib - CAMLDEP plugins/soswitness/src/soswitness.ml - CAMLOPT -c plugins/soswitness/src/soswitness.ml - COQC theories/misc.v - COQC theories/iteri_ord.v - COQC theories/bigop_tactics.v - File "plugins/soswitness/src/soswitness.mlg", line 16, characters 7-28: - Warning 3: deprecated: Coqlib.find_reference - Please use Coqlib.lib_ref - CAMLOPT -a -o plugins/soswitness/src/soswitness.cmxa - CAMLOPT -shared -o plugins/soswitness/src/soswitness.cmxs - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope - fun_scope. [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "_ + _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "_ - _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "_ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "_ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "_ >= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "_ > _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "_ < _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./theories/bigop_tactics.v", line 1, characters 0-72: - Warning: Notation "_ * _" was already used in scope nat_scope. - [notation-overridden,parsing] - COQC plugins/soswitness/theories/soswitness.v - File "./theories/iteri_ord.v", line 1, characters 0-72: - Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./theories/iteri_ord.v", line 1, characters 0-72: - Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./theories/iteri_ord.v", line 1, characters 0-72: - Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope - fun_scope. [notation-overridden,parsing] - File "./theories/iteri_ord.v", line 1, characters 0-72: - Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./theories/iteri_ord.v", line 1, characters 0-72: - Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./theories/iteri_ord.v", line 1, characters 0-72: - Warning: Notat [...] truncated ng.divalg_closed >-> GRing.subring_closed. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closed_semi] : GRing.divalg_closed >-> GRing.semiring_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedBM; GRing.subring_closed_semi] : GRing.divalg_closed >-> GRing.semiring_closed. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closedM; GRing.smulr_closedM] : GRing.divalg_closed >-> GRing.mulr_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedBM; GRing.subring_closedM; - GRing.smulr_closedM] : GRing.divalg_closed >-> GRing.mulr_closed. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closedM] : GRing.divalg_closed >-> GRing.smulr_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedBM; GRing.subring_closedM] : GRing.divalg_closed >-> GRing.smulr_closed. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closedB; GRing.zmod_closedN] : GRing.divalg_closed >-> GRing.oppr_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedZ; GRing.submod_closedB; - GRing.zmod_closedN] : GRing.divalg_closed >-> GRing.oppr_closed. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closedB; GRing.zmod_closedD] : GRing.divalg_closed >-> GRing.addr_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedZ; GRing.submod_closedB; - GRing.zmod_closedD] : GRing.divalg_closed >-> GRing.addr_closed. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closedB] : GRing.divalg_closed >-> GRing.zmod_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedZ; GRing.submod_closedB] : GRing.divalg_closed >-> GRing.zmod_closed. - [ambiguous-paths,typechecker] - File "./theories/validsdp.v", line 12, characters 0-77: - Warning: - New coercion path [GRing.Pred.subring_smul; GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing - [GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul. - [ambiguous-paths,typechecker] - File "./theories/posdef_check.v", line 14, characters 0-77: - Warning: - New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing - [GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed. - [ambiguous-paths,typechecker] - File "./theories/validsdp.v", line 12, characters 0-77: - Warning: - New coercion path [GRing.Pred.divring_sdiv; GRing.Pred.sdiv_smul; - GRing.Pred.smul_mul] : GRing.Pred.divring >-> GRing.Pred.mul is ambiguous with existing - [GRing.Pred.divring_ring; GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.divring >-> GRing.Pred.mul. - [ambiguous-paths,typechecker] - File "./theories/posdef_check.v", line 14, characters 0-77: - Warning: - New coercion path [GRing.subring_closed_semi; GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing - [GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed. - New coercion path [GRing.subring_closed_semi; GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing - [GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed. - [ambiguous-paths,typechecker] - File "./theories/posdef_check.v", line 14, characters 0-77: - Warning: - New coercion path [GRing.sdivr_closed_div; GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing - [GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed. - [ambiguous-paths,typechecker] - File "./theories/posdef_check.v", line 14, characters 0-77: - Warning: - New coercion path [GRing.subalg_closedBM; GRing.subring_closedB; - GRing.zmod_closedN] : GRing.subalg_closed >-> GRing.oppr_closed is ambiguous with existing - [GRing.subalg_closedZ; GRing.submod_closedB; GRing.zmod_closedN] : GRing.subalg_closed >-> GRing.oppr_closed. - New coercion path [GRing.subalg_closedBM; GRing.subring_closedB; - GRing.zmod_closedD] : GRing.subalg_closed >-> GRing.addr_closed is ambiguous with existing - [GRing.subalg_closedZ; GRing.submod_closedB; GRing.zmod_closedD] : GRing.subalg_closed >-> GRing.addr_closed. - New coercion path [GRing.subalg_closedBM; GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing - [GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed. - [ambiguous-paths,typechecker] - File "./theories/posdef_check.v", line 14, characters 0-77: - Warning: - New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM; - GRing.smulr_closedM] : GRing.divring_closed >-> GRing.mulr_closed is ambiguous with existing - [GRing.divring_closedBM; GRing.subring_closedM; GRing.smulr_closedM] : GRing.divring_closed >-> GRing.mulr_closed. - New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing - [GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed. - New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM; - GRing.smulr_closedN] : GRing.divring_closed >-> GRing.oppr_closed is ambiguous with existing - [GRing.divring_closedBM; GRing.subring_closedB; GRing.zmod_closedN] : GRing.divring_closed >-> GRing.oppr_closed. - [ambiguous-paths,typechecker] - File "./theories/posdef_check.v", line 14, characters 0-77: - Warning: - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closed_semi] : GRing.divalg_closed >-> GRing.semiring_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedBM; GRing.subring_closed_semi] : GRing.divalg_closed >-> GRing.semiring_closed. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closedM; GRing.smulr_closedM] : GRing.divalg_closed >-> GRing.mulr_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedBM; GRing.subring_closedM; - GRing.smulr_closedM] : GRing.divalg_closed >-> GRing.mulr_closed. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closedM] : GRing.divalg_closed >-> GRing.smulr_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedBM; GRing.subring_closedM] : GRing.divalg_closed >-> GRing.smulr_closed. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closedB; GRing.zmod_closedN] : GRing.divalg_closed >-> GRing.oppr_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedZ; GRing.submod_closedB; - GRing.zmod_closedN] : GRing.divalg_closed >-> GRing.oppr_closed. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closedB; GRing.zmod_closedD] : GRing.divalg_closed >-> GRing.addr_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedZ; GRing.submod_closedB; - GRing.zmod_closedD] : GRing.divalg_closed >-> GRing.addr_closed. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closedB] : GRing.divalg_closed >-> GRing.zmod_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedZ; GRing.submod_closedB] : GRing.divalg_closed >-> GRing.zmod_closed. - [ambiguous-paths,typechecker] - File "./theories/posdef_check.v", line 14, characters 0-77: - Warning: - New coercion path [GRing.Pred.subring_smul; GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing - [GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul. - [ambiguous-paths,typechecker] - File "./theories/posdef_check.v", line 14, characters 0-77: - Warning: - New coercion path [GRing.Pred.divring_sdiv; GRing.Pred.sdiv_smul; - GRing.Pred.smul_mul] : GRing.Pred.divring >-> GRing.Pred.mul is ambiguous with existing - [GRing.Pred.divring_ring; GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.divring >-> GRing.Pred.mul. - [ambiguous-paths,typechecker] - File "./theories/posdef_check.v", line 21, characters 0-46: - Warning: Notation "_ <=> _" was already used in scope type_scope. - [notation-overridden,parsing] - File "./theories/posdef_check.v", line 246, characters 0-29: - Warning: Use of “Require” inside a section is deprecated. - [require-in-section,deprecated] - File "./theories/validsdp.v", line 21, characters 0-46: - Warning: Notation "_ <=> _" was already used in scope type_scope. - [notation-overridden,parsing] - File "./theories/validsdp.v", line 1077, characters 0-29: - Warning: Use of “Require” inside a section is deprecated. - [require-in-section,deprecated] - Finished transaction in 0.308 secs (0.012u,0.s) (successful) - File "./theories/validsdp.v", line 1145, characters 6-58: - Warning: Duplicate clear of Hm [duplicate-clear,ssr] - Finished transaction in 268.041 secs (0.018u,0.s) (successful) - Finished transaction in 48.052 secs (0.012u,0.s) (successful) - Finished transaction in 52.558 secs (0.014u,0.s) (successful) - Finished transaction in 51.692 secs (0.017u,0.s) (successful) - Selected hypotheses (H2, H1) The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true