ยซ Up

certicoq 0.9~beta+8.14 Error ๐Ÿ”ฅ

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-threads        base
base-unix           base
conf-findutils      1           Virtual package relying on findutils
conf-gmp            4           Virtual package relying on a GMP lib system installation
coq                 8.14.1      Formal proof management system
dune                3.6.2       Fast, portable, and opinionated build system
ocaml               4.08.1      The OCaml compiler (virtual package)
ocaml-base-compiler 4.08.1      Official release 4.08.1
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.5       A library manager for OCaml
zarith              1.12        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "The CertiCoq Team"
homepage: "https://certicoq.org/"
dev-repo: "git+https://github.com/CertiCoq/certicoq"
bug-reports: "https://github.com/CertiCoq/certicoq/issues"
authors: ["Andrew Appel"
          "Yannick Forster"
          "Anvay Grover"
          "Joomy Korkut"
          "John Li"
          "Zoe Paraskevopoulou"
          "Matthieu Sozeau"
          "Matthew Weaver"
          "Abhishek Anand"
          "Greg Morrisett"
          "Randy Pollack"
          "Olivier Savary Belanger"
  ]
license: "MIT"
build: [
  [make "all"]
  [make "plugins"]
  [make "bootstrap"]
]
install: [
  [make "install"]
]
depends: [
  "ocaml"
  "coq" {>= "8.14" & < "8.15~"}
  "coq-compcert" {= "3.11"}
  "coq-equations" {= "1.3+8.14"}
  "coq-metacoq-erasure" {>= "1.1.1+8.14" }
  "coq-ext-lib" {>= "0.11.5"}
]
synopsis: "A Verified Compiler for Gallina, Written in Gallina "
url {
  src: "https://github.com/CertiCoq/certicoq/archive/refs/tags/v0.9-beta.tar.gz"
  checksum: "sha512=dd5269d4666cdf7410e828472584ca59bf62729c9ac9ad47fb654da5723d7d16e5b27325aa89086f880c13890a62701af40f8719889dc7be2e522aba413b14e1"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-certicoq.0.9~beta+8.14 coq.8.14.1
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-certicoq.0.9~beta+8.14 coq.8.14.1
Return code
0
Duration
3 h 31 m

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-certicoq.0.9~beta+8.14 coq.8.14.1
Return code
7936
Duration
1 h 7 m
Output
# Packages matching: installed
# Name                  # Installed # Synopsis
base-bigarray           base
base-threads            base
base-unix               base
conf-findutils          1           Virtual package relying on findutils
conf-g++                1.0         Virtual package relying on the g++ compiler (for C++)
conf-gmp                4           Virtual package relying on a GMP lib system installation
coq                     8.14.1      Formal proof management system
coq-compcert            3.11        The CompCert C compiler (64 bit)
coq-equations           1.3+8.14    A function definition package for Coq
coq-ext-lib             0.11.7      A library of Coq definitions, theorems, and tactics
coq-flocq               4.1.0       A formalization of floating-point arithmetic for the Coq system
coq-menhirlib           20220210    A support library for verified Coq parsers produced by Menhir
coq-metacoq-erasure     1.1.1+8.14  Implementation and verification of an erasure procedure for Coq
coq-metacoq-pcuic       1.1.1+8.14  A type system equivalent to Coq's and its metatheory
coq-metacoq-safechecker 1.1.1+8.14  Implementation and verification of safe conversion and typechecking algorithms for Coq
coq-metacoq-template    1.1.1+8.14  A quoting and unquoting library for Coq in Coq
dune                    3.6.2       Fast, portable, and opinionated build system
menhir                  20220210    An LR(1) parser generator
menhirLib               20220210    Runtime support library for parsers generated by Menhir
menhirSdk               20220210    Compile-time library for auxiliary tools related to Menhir
ocaml                   4.08.1      The OCaml compiler (virtual package)
ocaml-base-compiler     4.08.1      Official release 4.08.1
ocaml-config            1           OCaml Switch Configuration
ocamlfind               1.9.5       A library manager for OCaml
stdlib-shims            0.3.0       Backport some of the new stdlib features to older compiler
zarith                  1.12        Implements arithmetic and logical operations over arbitrary-precision integers
[NOTE] Package coq is already installed (current version is 8.14.1).
The following actions will be performed:
  - install coq-certicoq 0.9~beta+8.14
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/1: [coq-certicoq.0.9~beta+8.14: http]
[coq-certicoq.0.9~beta+8.14] downloaded from https://github.com/CertiCoq/certicoq/archive/refs/tags/v0.9-beta.tar.gz
Processing  1/1:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/2: [coq-certicoq: make all]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "all" (CWD=/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14)
- cd theories;coq_makefile -f _CoqProject -o Makefile
- cd libraries;coq_makefile -f _CoqProject -o Makefile
- make -C libraries -j`nproc`
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14/libraries'
- COQDEP VFILES
- COQC CpdtTactics.v
- COQC HashMap.v
- COQC MyPermutations.v
- COQC maps_util.v
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14/libraries'
- make -C theories -j`nproc`
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14/theories'
- COQDEP VFILES
- COQC common/exceptionMonad.v
- COQC common/classes.v
- COQC common/compM.v
- COQC LambdaANF/Ensembles_util.v
- COQC LambdaANF/tactics.v
- COQC LambdaANF/Frame.v
- COQC LambdaANF/PrototypeTests.v
- COQC Codegen/tactics.v
- COQC ExtractionVanilla/VanillaExtrOCamlInt63.v
- COQC ExtractionVanilla/VanillaExtrOCamlFloats.v
- COQC LambdaANF/Rewriting.v
- COQC LambdaANF/PrototypeGenFrame.v
- COQC common/RandyPrelude.v
- COQC common/AstCommon.v
- COQC LambdaANF/List_util.v
- COQC LambdaANF/functions.v
-      = "46"
-      : string
-      = "8C"
-      : string
-      = "E51"
-      : string
- COQC LambdaANF/Prototype.v
- COQC LambdaANF/MockExpr.v
- COQC common/Common.v
- COQC common/Pipeline_utils.v
- COQC LambdaANF/set_util.v
- COQC LambdaBoxMut/compile.v
- COQC LambdaBoxLocal/expression.v
- COQC LambdaANF/map_util.v
- COQC LambdaANF/cps.v
- COQC LambdaBoxMut/term.v
- COQC LambdaANF/ctx.v
- COQC LambdaANF/cps_show.v
- COQC LambdaANF/algebra.v
- COQC LambdaANF/cps_util.v
- COQC LambdaANF/relations.v
- COQC LambdaBoxLocal/LambdaBoxMut_to_LambdaBoxLocal.v
- COQC LambdaBoxLocal/fuel_sem.v
- COQC LambdaBoxMut/program.v
- COQC LambdaANF/identifiers.v
- COQC LambdaBoxMut/wcbvEval.v
- COQC LambdaBoxMut/wNorm.v
- COQC LambdaBoxMut/stripEvalCommute.v
- COQC LambdaBoxMut/toplevel.v
- COQC LambdaBoxLocal/LambdaBoxMut_to_LambdaBoxLocal_correct.v
- COQC LambdaBoxMut/LambdaBoxMut.v
- Axioms:
- PrimInt63.int : Set
- PrimFloat.float : Set
- COQC LambdaBoxLocal/toplevel.v
- COQC LambdaANF/cps_proto_univ.v
- COQC LambdaANF/rename.v
- COQC LambdaANF/state.v
- COQC LambdaANF/size_cps.v
- COQC Codegen/LambdaANF_to_Clight.v
- COQC Glue/glue_utils.v
- COQC LambdaANF/closure_conversion.v
- COQC LambdaANF/uncurry.v
- COQC LambdaANF/dead_param_elim.v
- COQC LambdaANF/freshen.v
- COQC LambdaANF/cps_proto.v
- COQC LambdaANF/stemctx.v
- COQC LambdaANF/eval.v
- COQC Glue/glue.v
- COQC Glue/ffi.v
- COQC LambdaANF/logical_relations.v
- COQC LambdaANF/LambdaBoxLocal_to_LambdaANF.v
- COQC LambdaANF/closure_conversion_util.v
- COQC LambdaANF/env.v
- COQC LambdaANF/alpha_conv.v
- COQC LambdaANF/logical_relations_cc.v
- COQC LambdaANF/exp_equiv.v
- COQC LambdaANF/inline_letapp.v
- COQC LambdaANF/LambdaBoxLocal_to_LambdaANF_util.v
- COQC LambdaANF/lambda_lifting.v
- COQC LambdaANF/lambda_lifting_util.v
- COQC LambdaANF/shrink_cps.v
- COQC LambdaANF/rel_comp.v
- COQC LambdaANF/closure_conversion_corresp.v
- COQC LambdaANF/hoisting.v
- COQC LambdaANF/LambdaBoxLocal_to_LambdaANF_corresp.v
- COQC LambdaANF/closure_conversion_invariants.v
- COQC LambdaANF/dead_param_elim_util.v
- COQC LambdaANF/closure_conversion_correct.v
- COQC LambdaANF/proto_util.v
- COQC LambdaANF/shrink_cps_correct.v
- COQC LambdaANF/inline.v
- COQC LambdaANF/inline_correct.v
- COQC LambdaANF/uncurry_proto.v
- COQC LambdaANF/toplevel.v
- COQC Codegen/LambdaANF_to_Clight_stack.v
- COQC Codegen/toplevel.v
- COQC Compiler/pipeline.v
- COQC Extraction/extraction.v
- COQC ExtractionVanilla/extraction.v
- COQC LambdaANF/uncurry_rel.v
- COQC LambdaANF/shrink_cps_corresp.v
- COQC LambdaANF/uncurry_correct.v
- COQC LambdaANF/lambda_lifting_corresp.v
- COQC LambdaANF/shrink_cps_toplevel.v
- COQC LambdaANF/lambda_lifting_correct.v
- COQC LambdaANF/dead_param_elim_correct.v
- COQC LambdaANF/bounds.v
- COQC LambdaANF/LambdaBoxLocal_to_LambdaANF_correct.v
- COQC LambdaANF/toplevel_theorems.v
- Axioms:
- PrimInt63.int : Set
- FunctionalExtensionality.functional_extensionality_dep
-   : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
-     (forall x : A, f x = g x) -> f = g
- PrimFloat.float : Set
- Axioms:
- PrimInt63.int : Set
- FunctionalExtensionality.functional_extensionality_dep
-   : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
-     (forall x : A, f x = g x) -> f = g
- PrimFloat.float : Set
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14/theories'
Processing  1/2: [coq-certicoq: make plugins]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "plugins" (CWD=/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14)
- make -C libraries -j`nproc`
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14/libraries'
- make[2]: Nothing to be done for 'real-all'.
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14/libraries'
- make -C theories -j`nproc`
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14/theories'
- make[2]: Nothing to be done for 'real-all'.
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14/theories'
- cd plugin ; coq_makefile -f _CoqProject -o Makefile
- bash ./make_plugin.sh plugin
- Building optimized ML plugin
- Plugin:  plugin
- Building optimized ML plugin
- Cleaning result of extraction
- Copying  AST.ml to ../../plugin/extraction/aST.ml
- Copying  AST.mli to ../../plugin/extraction/aST.mli
- Copying  All_Forall.ml to ../../plugin/extraction/all_Forall.ml
- Copying  All_Forall.mli to ../../plugin/extraction/all_Forall.mli
- Copying  Archi.ml to ../../plugin/extraction/archi.ml
- Copying  Archi.mli to ../../plugin/extraction/archi.mli
- Copying  Ascii.ml to ../../plugin/extraction/ascii.ml
- Copying  Ascii.mli to ../../plugin/extraction/ascii.mli
- Copying  Ast0.ml to ../../plugin/extraction/ast0.ml
- Copying  Ast0.mli to ../../plugin/extraction/ast0.mli
- Copying  AstCommon.ml to ../../plugin/extraction/astCommon.ml
- Copying  AstCommon.mli to ../../plugin/extraction/astCommon.mli
- Copying  AstUtils.ml to ../../plugin/extraction/astUtils.ml
- Copying  AstUtils.mli to ../../plugin/extraction/astUtils.mli
- Copying  BasicAst.ml to ../../plugin/extraction/basicAst.ml
- Copying  BasicAst.mli to ../../plugin/extraction/basicAst.mli
- Copying  Basics.ml to ../../plugin/extraction/basics.ml
- Copying  Basics.mli to ../../plugin/extraction/basics.mli
- Copying  BinInt.ml to ../../plugin/extraction/binInt.ml
- Copying  BinInt.mli to ../../plugin/extraction/binInt.mli
- Copying  BinNat.ml to ../../plugin/extraction/binNat.ml
- Copying  BinNat.mli to ../../plugin/extraction/binNat.mli
- Copying  BinNatDef.ml to ../../plugin/extraction/binNatDef.ml
- Copying  BinNatDef.mli to ../../plugin/extraction/binNatDef.mli
- Copying  BinNums.ml to ../../p
[...] truncated
ime elapsed in Lambda lift:  3.073716
- Debug: Time elapsed in Shrink:  1.233238
- Debug: Time elapsed in Closure conversion and hoisting:  3.673653
- Debug: Time elapsed in Shrink:  2.475203
- Debug: Time elapsed in Inline/shrink loop:  126.807197
- Debug: Time elapsed in Dead param elim:  1.427586
- Debug: Time elapsed in Shrink:  1.079795
- Debug: Time elapsed in LambdaANF Pipeline:  180.532802
- Debug: Time elapsed in Codegen:  3.882349
- coq_makefile -f _CoqProject -o Makefile.certicoqc
- Warning: ../../cplugin (used in -R or -Q) is not a subdirectory of the current directory
- 
- ocamlfind opt -package coq-core,coq-core.clib,coq-core.config,coq-core.engine,coq-core.gramlib,coq-core.interp,coq-core.kernel,coq-core.lib,coq-core.library,coq-core.toplevel,coq-core.vernac,coq-core.plugins.ltac -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/user-contrib/MetaCoq/Template -open Metacoq_template_plugin -I ../../cplugin -open Certicoq_vanilla_plugin -I . -linkpkg -dontlink str,unix,dynlink,threads,zarith  -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8 -for-pack Certicoqc_plugin certicoqc_plugin_wrapper.mli
- ocamlfind opt -c -package coq-core,coq-core.clib,coq-core.config,coq-core.engine,coq-core.gramlib,coq-core.interp,coq-core.kernel,coq-core.lib,coq-core.library,coq-core.toplevel,coq-core.vernac,coq-core.plugins.ltac -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/user-contrib/MetaCoq/Template -open Metacoq_template_plugin -I ../../cplugin -open Certicoq_vanilla_plugin -I . -linkpkg -dontlink str,unix,dynlink,threads,zarith  -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8 -for-pack Certicoqc_plugin -o certicoqc_plugin_wrapper.cmx certicoqc_plugin_wrapper.ml
- ocamlfind opt -package coq-core,coq-core.clib,coq-core.config,coq-core.engine,coq-core.gramlib,coq-core.interp,coq-core.kernel,coq-core.lib,coq-core.library,coq-core.toplevel,coq-core.vernac,coq-core.plugins.ltac -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/user-contrib/MetaCoq/Template -open Metacoq_template_plugin -I ../../cplugin -open Certicoq_vanilla_plugin -I . -linkpkg -dontlink str,unix,dynlink,threads,zarith  -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8 -for-pack Certicoqc_plugin certicoqc.mli
- ocamlfind opt -c -package coq-core,coq-core.clib,coq-core.config,coq-core.engine,coq-core.gramlib,coq-core.interp,coq-core.kernel,coq-core.lib,coq-core.library,coq-core.toplevel,coq-core.vernac,coq-core.plugins.ltac -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/user-contrib/MetaCoq/Template -open Metacoq_template_plugin -I ../../cplugin -open Certicoq_vanilla_plugin -I . -linkpkg -dontlink str,unix,dynlink,threads,zarith  -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8 -for-pack Certicoqc_plugin -o certicoqc.cmx certicoqc.ml
- coqpp g_certicoqc.mlg
- [ -f "g_certicoqc.mli" ] || ocamlfind opt -package coq-core,coq-core.clib,coq-core.config,coq-core.engine,coq-core.gramlib,coq-core.interp,coq-core.kernel,coq-core.lib,coq-core.library,coq-core.toplevel,coq-core.vernac,coq-core.plugins.ltac -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/user-contrib/MetaCoq/Template -open Metacoq_template_plugin -I ../../cplugin -open Certicoq_vanilla_plugin -I . -linkpkg -dontlink str,unix,dynlink,threads,zarith  -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8 -for-pack Certicoqc_plugin -i g_certicoqc.ml > g_certicoqc.mli
- ocamlfind opt -package coq-core,coq-core.clib,coq-core.config,coq-core.engine,coq-core.gramlib,coq-core.interp,coq-core.kernel,coq-core.lib,coq-core.library,coq-core.toplevel,coq-core.vernac,coq-core.plugins.ltac -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/user-contrib/MetaCoq/Template -open Metacoq_template_plugin -I ../../cplugin -open Certicoq_vanilla_plugin -I . -linkpkg -dontlink str,unix,dynlink,threads,zarith  -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8 -for-pack Certicoqc_plugin g_certicoqc.mli
- ocamlfind opt -c -package coq-core,coq-core.clib,coq-core.config,coq-core.engine,coq-core.gramlib,coq-core.interp,coq-core.kernel,coq-core.lib,coq-core.library,coq-core.toplevel,coq-core.vernac,coq-core.plugins.ltac -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/user-contrib/MetaCoq/Template -open Metacoq_template_plugin -I ../../cplugin -open Certicoq_vanilla_plugin -I . -linkpkg -dontlink str,unix,dynlink,threads,zarith  -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8 -for-pack Certicoqc_plugin -o g_certicoqc.cmx g_certicoqc.ml
- ocamlfind opt -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/user-contrib/MetaCoq/Template -open Metacoq_template_plugin -I ../../cplugin -open Certicoq_vanilla_plugin -I . -linkpkg -dontlink str,unix,dynlink,threads,zarith  -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8 -pack -o certicoqc_plugin.cmx certicoqc_plugin_wrapper.cmx certicoqc.cmx g_certicoqc.cmx
- ocamlfind opt -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/user-contrib/MetaCoq/Template -open Metacoq_template_plugin -I ../../cplugin -open Certicoq_vanilla_plugin -I . -linkpkg -dontlink str,unix,dynlink,threads,zarith  -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8 -a -o certicoqc_plugin.cmxa certicoqc_plugin.cmx
- clang  -fPIC -g -c -I . -I ../../plugin/runtime -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/ocaml -w -Wno-everything -O2 -o certicoqc_wrapper.o certicoqc_wrapper.c
- make[2]: clang: Command not found
- make[2]: *** [Makefile:55: certicoqc_wrapper.o] Error 127
- rm certicoqc.cmi certicoqc_plugin_wrapper.cmi g_certicoqc.cmi
- make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14/bootstrap/certicoqc'
- make[1]: *** [Makefile:6: certicoqc] Error 2
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14/bootstrap'
- make: *** [Makefile:39: bootstrap] Error 2
[ERROR] The compilation of coq-certicoq failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make bootstrap".
#=== ERROR while compiling coq-certicoq.0.9~beta+8.14 =========================#
# context              2.0.5 | linux/x86_64 | ocaml-base-compiler.4.08.1 | file:///home/bench/run/opam-coq-archive/released
# path                 ~/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14
# command              ~/.opam/opam-init/hooks/sandbox.sh build make bootstrap
# exit-code            2
# env-file             ~/.opam/log/coq-certicoq-5469-60459a.env
# output-file          ~/.opam/log/coq-certicoq-5469-60459a.out
### output ###
# [...]
# ocamlfind opt -package coq-core,coq-core.clib,coq-core.config,coq-core.engine,coq-core.gramlib,coq-core.interp,coq-core.kernel,coq-core.lib,coq-core.library,coq-core.toplevel,coq-core.vernac,coq-core.plugins.ltac -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/user-contrib/MetaCoq/Template -open Metacoq_template_plugin -I ../../cplugin -open Certicoq_vanilla_plugin -I . -linkpkg -dont[...]
# ocamlfind opt -c -package coq-core,coq-core.clib,coq-core.config,coq-core.engine,coq-core.gramlib,coq-core.interp,coq-core.kernel,coq-core.lib,coq-core.library,coq-core.toplevel,coq-core.vernac,coq-core.plugins.ltac -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/user-contrib/MetaCoq/Template -open Metacoq_template_plugin -I ../../cplugin -open Certicoq_vanilla_plugin -I . -linkpkg -d[...]
# ocamlfind opt -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/user-contrib/MetaCoq/Template -open Metacoq_template_plugin -I ../../cplugin -open Certicoq_vanilla_plugin -I . -linkpkg -dontlink str,unix,dynlink,threads,zarith  -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8 -pack -o certicoqc_p[...]
# ocamlfind opt -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/user-contrib/MetaCoq/Template -open Metacoq_template_plugin -I ../../cplugin -open Certicoq_vanilla_plugin -I . -linkpkg -dontlink str,unix,dynlink,threads,zarith  -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8 -a -o certicoqc_plug[...]
# clang  -fPIC -g -c -I . -I ../../plugin/runtime -I /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/ocaml -w -Wno-everything -O2 -o certicoqc_wrapper.o certicoqc_wrapper.c
# make[2]: clang: Command not found
# make[2]: *** [Makefile:55: certicoqc_wrapper.o] Error 127
# rm certicoqc.cmi certicoqc_plugin_wrapper.cmi g_certicoqc.cmi
# make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14/bootstrap/certicoqc'
# make[1]: *** [Makefile:6: certicoqc] Error 2
# make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-certicoq.0.9~beta+8.14/bootstrap'
# make: *** [Makefile:39: bootstrap] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-certicoq 0.9~beta+8.14
+- 
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-certicoq.0.9~beta+8.14 coq.8.14.1' failed.
The middle of the output is truncated (maximum 20000 characters)

Installation size

No files were installed.

Uninstall ๐Ÿงน

Command
true
Return code
0
Missing removes
none
Wrong removes
none