# 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.13.1 Formal proof management system
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.13.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.13.1 Official release 4.13.1
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "matthieu.sozeau@inria.fr"
homepage: "https://metacoq.github.io/metacoq"
dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.13"
bug-reports: "https://github.com/MetaCoq/metacoq/issues"
authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
"Simon Boulier <simon.boulier@inria.fr>"
"Cyril Cohen <cyril.cohen@inria.fr>"
"Yannick Forster <forster@ps.uni-saarland.de>"
"Fabian Kunze <fkunze@fakusb.de>"
"Gregory Malecha <gmalecha@gmail.com>"
"Matthieu Sozeau <matthieu.sozeau@inria.fr>"
"Nicolas Tabareau <nicolas.tabareau@inria.fr>"
"ThΓ©o Winterhalter <theo.winterhalter@inria.fr>"
]
license: "MIT"
build: [
["sh" "./configure.sh"]
[make "-j" "%{jobs}%" "template-coq"]
]
install: [
[make "-C" "template-coq" "install"]
]
depends: [
"ocaml" {>= "4.07.1"}
"coq" {>= "8.13" & < "8.14~"}
"coq-equations" { >= "1.2.3" }
]
synopsis: "A quoting and unquoting library for Coq in Coq"
description: """
MetaCoq is a meta-programming framework for Coq.
Template Coq is a quoting library for Coq. It takes Coq terms and
constructs a representation of their syntax tree as a Coq inductive data
type. The representation is based on the kernel's term representation.
In addition to a complete reification and denotation of CIC terms,
Template Coq includes:
- Reification of the environment structures, for constant and inductive declarations.
- Denotation of terms and global declarations
- A monad for manipulating global declarations, calling the type
checker, and inserting them in the global environment, in the style of
MetaCoq/MTac.
"""
url {
src: "https://github.com/MetaCoq/metacoq/archive/v1.0-beta2-8.13.tar.gz"
checksum: "sha256=15e1cfde70e6c4dbf33bff1a77266ac5c0c3e280586ef059e0cdec07bee814f2"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-metacoq-template.1.0~beta2+8.13 coq.8.13.1Dry 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-metacoq-template.1.0~beta2+8.13 coq.8.13.1opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-metacoq-template.1.0~beta2+8.13 coq.8.13.1Total: 21 M
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/metacoq_template_plugin.cmxs../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/common/uGraph.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Reflect.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Universes.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/wGraph.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Checker.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/All_Forall.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Typing.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/metacoq_template_plugin.cmi../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TypingWf.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/EnvironmentTyping.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/template_coq.cmxs../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/LiftSubst.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Typing.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/wGraph.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/common/uGraph.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCCompare.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/All_Forall.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/metacoq_template_plugin.cmx../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Kernames.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/BasicAst.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCList.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TermEquality.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Universes.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/LiftSubst.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/WcbvEval.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCPrelude.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/EnvironmentTyping.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCList.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/template_coq.cmi../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Checker.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Environment.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Ast.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TypingWf.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/UnivSubst.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/AstUtils.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/monad_utils.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Induction.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/WfInv.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Pretty.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/WcbvEval.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Reduction.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/wGraph.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/common/uGraph.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TermEquality.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCUtils.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TemplateMonad/Core.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCOption.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Normal.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Environment.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TemplateMonad/Common.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Constants.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TemplateMonad/Extractable.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Universes.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Typing.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Extraction.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Reflect.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/All.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Loader.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/LibHypsNaming.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/All_Forall.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/BasicAst.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TemplateMonad.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/AstUtils.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/UnivSubst.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Induction.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/EnvironmentTyping.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/template_coq.cmx../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Kernames.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/monad_utils.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCArith.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Pretty.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCRelations.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCList.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TypingWf.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Checker.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/WcbvEval.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCRelations.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/LiftSubst.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCString.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/WfInv.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCUtils.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MC_ExtrOCamlInt63.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Reflect.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TemplateMonad/Core.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Ast.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Normal.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TermEquality.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Constants.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCCompare.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCOption.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Environment.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/LibHypsNaming.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCProd.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/LibHypsNaming.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/BasicAst.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TemplateMonad/Extractable.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCProd.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Kernames.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/metacoq_template_plugin.cmxa../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Reduction.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/AstUtils.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/template_coq.cmxa../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Pretty.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCCompare.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Induction.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/monad_utils.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCArith.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Ast.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCUtils.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/UnivSubst.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCString.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCRelations.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/WfInv.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TemplateMonad/Core.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TemplateMonad/Common.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCPrelude.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/config.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCSquash.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCOption.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TemplateMonad/Extractable.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCEquality.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Normal.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCPrelude.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MC_ExtrOCamlInt63.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Extraction.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Reduction.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCProd.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCEquality.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/ExtractableLoader.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TemplateMonad/Common.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/number.cmi../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/config.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCArith.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCString.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCSquash.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/number.cmx../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Extraction.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/config.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/All.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/All.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Loader.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCEquality.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MCSquash.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/utils/MC_ExtrOCamlInt63.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Loader.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/Constants.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TemplateMonad.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/TemplateMonad.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/ExtractableLoader.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/MetaCoq/Template/ExtractableLoader.globopam remove -y coq-metacoq-template.1.0~beta2+8.13