# 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.0 Formal proof management system
dune 3.6.2 Fast, portable, and opinionated build system
ocaml 4.12.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.12.1 Official release 4.12.1
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
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"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-certicoq.0.9~beta+8.14 coq.8.14.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 4h opam install -y --deps-only coq-certicoq.0.9~beta+8.14 coq.8.14.0opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-certicoq.0.9~beta+8.14 coq.8.14.0# 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.0 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.12.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.12.1 Official release 4.12.1 ocaml-config 2 OCaml Switch Configuration ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled 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.0). 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.12.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.12.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.12.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.12.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 LambdaANF/identifiers.v - COQC LambdaBoxMut/program.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/toplevel_theorems.v - COQC LambdaANF/LambdaBoxLocal_to_LambdaANF_correct.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.12.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.12.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.12.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.12.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.12.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.12.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 [...] truncated e elapsed in Lambda lift: 3.546945 - Debug: Time elapsed in Shrink: 1.181125 - Debug: Time elapsed in Closure conversion and hoisting: 3.879810 - Debug: Time elapsed in Shrink: 2.297579 - Debug: Time elapsed in Inline/shrink loop: 120.159637 - Debug: Time elapsed in Dead param elim: 1.370382 - Debug: Time elapsed in Shrink: 1.100201 - Debug: Time elapsed in LambdaANF Pipeline: 170.942278 - Debug: Time elapsed in Codegen: 4.504017 - 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.12.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.12.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.12.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.12.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.12.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.12.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.12.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.12.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.12.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.12.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.12.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.12.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.8 | linux/x86_64 | ocaml-base-compiler.4.12.1 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.12.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-15391-60459a.env # output-file ~/.opam/log/coq-certicoq-15391-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.12.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.12.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.12.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.12.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.12.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.12.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.12.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.0' failed. The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true