# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
coq 8.12.2 Formal proof management system
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.09.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1 Official release 4.09.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.3 A library manager for OCaml
# opam file:
opam-version: "2.0"
synopsis: "Yalla library"
description: """
YALLA: an LL library for Coq
Yet Another deep embedding of Linear Logic in Coq
"""
homepage: "https://perso.ens-lyon.fr/olivier.laurent/yalla/"
dev-repo: "git+https://github.com/olaure01/yalla.git"
bug-reports: "https://github.com/olaure01/yalla/issues"
doc: "https://perso.ens-lyon.fr/olivier.laurent/yalla/"
maintainer: "olivier.laurent@ens-lyon.fr"
authors: [
"Olivier Laurent"
]
license: "LGPL-3.0-or-later"
depends: [
"coq" { >= "8.12" & < "8.13" }
]
build: [
["./configure"]
[make "-j%{jobs}%"]
]
install: [
[make "install"]
]
url {
src: "https://github.com/olaure01/yalla/archive/v2.0.1.tar.gz"
checksum: "sha256=e9239fb82cfe32374fbf58d69850fe8c5d189f5d2a814175b606bd6b487a0d9b"
}
tags: [
"keyword:linear logic"
"keyword:metatheory"
"keyword:cut elimination"
"category:Mathematics/Logic/Foundations"
"date:2020-08-07"
"logpath:Yalla"
]
trueDry install with the current Coq version:
opam install -y --show-action coq-yalla.2.0.1 coq.8.12.2Dry 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-yalla.2.0.1 coq.8.12.2opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-yalla.2.0.1 coq.8.12.2Total: 18 M
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_vs_ll.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_cut.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_cut.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/llfoc.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/bbb.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/flat_map_more.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/llpol.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_vs_ll.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_def.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/nn_foc.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_def.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/tl.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_fragments.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/llfoc.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_cut.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_fragments.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/List_Type.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/flat_map_more.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/iformulas.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/formulas.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/List_more.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/List_Type.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_cut.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/llpol.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_smp.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_vs_ll.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/mell_mset.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_prop.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_smp.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/infinite.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/mell_msetoid.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/nn_def.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/GPermutation_Type.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_Type_more.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_def.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_Type.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/nn_prop.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_prop.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/mell_Prop.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/lambek.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/CPermutation_Type.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/mell2.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/bbb.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_def.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/nn_prop.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_prop.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_Type.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/dectype.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/BOrders.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/tl.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/GPermutation_Type.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/fmsetlist.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/nn_foc.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/GPermutation.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/mell_mset.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/fmsetlist_Type.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/List_more.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/nattree.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_Type_more.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/nn_def.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/isubs.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_cut.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/llfoc.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_prop.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/subs.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/GPermutation.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/CPermutation_Type.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/transp_perm.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_cut.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_fragments.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/AFC.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Dependent_Forall_Type.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/infinite.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/fmsetoidlist_Type.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/CPermutation_more.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/llpol.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/fmformulas.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/fmiformulas.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/fmsetoidlist.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/funtheory.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/List_Type.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/iformulas.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/wf_prod.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_more.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/formulas.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_def.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/basic_misc.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/dectype.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/PermutationPropify.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/bbb.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/PermutationPropify.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_def.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/fmsetlist_Type.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/flat_map_more.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/MicroYalla/ill.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/tl.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/BOrders.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/nn_foc.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/fmsetlist.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/MicroYalla/ll.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/fmsetoidlist_Type.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/mell_msetoid.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/yalla_ax.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Dependent_Forall_Type.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/ComparisonOrder.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/List_assoc.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/fmsetoidlist.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_smp.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/List_more.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/funtheory.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_Type.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/GPermutation_Type.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/mell_mset.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/nn_prop.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/isubs.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_prop.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_Type_solve.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/nattree.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_solve.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/mell_Prop.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/subs.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/mell2.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/GPermutation.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/CPermutation_Type_solve.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/nn_def.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/CPermutation_solve.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/MicroYalla/ill.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_prop.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/infinite.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/transp_perm.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/AFC.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/iformulas.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_Type_more.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/formulas.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_smp.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/lambek.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/CPermutation_more.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/MicroYalla/ll.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/ComparisonOrder.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_more.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/CPermutation_Type.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/yalla_ax.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/dectype.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/BOrders.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/PermutationPropify.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/mell_msetoid.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ill_smp.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/fmsetlist_Type.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/mell_Prop.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/fmiformulas.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/fmformulas.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/fmsetlist.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Dependent_Forall_Type.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/List_assoc.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/funtheory.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/mell2.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/ll_smp.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_Type_solve.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/fmsetoidlist_Type.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/fmsetoidlist.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/isubs.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/nattree.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/subs.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_solve.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/lambek.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/AFC.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/yalla_ax.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/wf_prod.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_more.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/CPermutation_Type_solve.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_Type_solve.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/ComparisonOrder.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/Permutation_solve.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/CPermutation_solve.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/transp_perm.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/CPermutation_more.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/MicroYalla/ill.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/wf_prod.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/fmiformulas.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/List_assoc.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/CPermutation_Type_solve.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/fmformulas.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/OLlibs/CPermutation_solve.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/MicroYalla/ll.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/basic_misc.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Yalla/basic_misc.globopam remove -y coq-yalla.2.0.1