« Up

mirror-core 1.0.1 33 m 0 s 🏆

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-num            base        Num library distributed with the OCaml compiler
base-threads        base
base-unix           base
camlp5              7.14        Preprocessor-pretty-printer of OCaml
conf-findutils      1           Virtual package relying on findutils
conf-perl           2           Virtual package relying on perl
coq                 8.5.0       Formal proof management system
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.03.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.03.0      Official 4.03.0 release
ocaml-config        1           OCaml Switch Configuration
# opam file:
opam-version: "2.0"
maintainer: "gmalecha@gmail.com"
homepage: "https://github.com/gmalecha/mirror-core"
dev-repo: "git+https://github.com/gmalecha/mirror-core.git"
bug-reports: "https://github.com/gmalecha/mirror-core/issues"
authors: ["Gregory Malecha"]
license: "BSD"
build: [
  [make "-j%{jobs}%"]
]
install: [
  [make "install"]
]
remove: [
  ["rm" "-R" "%{lib}%/coq/user-contrib/MirrorCore"]
  ["rm" "-R" "%{lib}%/coq/user-contrib/McExamples"]
]
depends: [
  "ocaml"
  "coq" {>= "8.5.0" & < "8.5.2~"}
  "coq-ext-lib" {>= "0.9.2"}
  "coq-plugin-utils"
]
synopsis: "A framework for computational reflection"
flags: light-uninstall
url {
  src: "https://github.com/gmalecha/mirror-core/archive/v1.0.1.tar.gz"
  checksum: "md5=3c61f6c8134ec6b5d3ea0af826d5156f"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-mirror-core.1.0.1 coq.8.5.0
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-mirror-core.1.0.1 coq.8.5.0
Return code
0
Duration
2 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-mirror-core.1.0.1 coq.8.5.0
Return code
0
Duration
33 m 0 s

Installation size

Total: 22 M

  • 2 M ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/AutoSetoidRewriteRtac.vo
  • 1 M ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Minify.vo
  • 1 M ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Subst/UVarMap.vo
  • 1 M ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Ctx.vo
  • 727 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/ExprUnify_simul.vo
  • 600 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Subst/FMapSubst.vo
  • 561 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/RedAll.vo
  • 548 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Hoare/Verify.vo
  • 493 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/ExprLift.vo
  • 466 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Hoare/ImpSyntax.vo
  • 460 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/SpecLemmas.vo
  • 351 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Core.vo
  • 349 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/ExprDsimul.vo
  • 338 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/ExprSubst.vo
  • 321 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/Red.vo
  • 310 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/ExprDFacts.vo
  • 310 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/BIMap.vo
  • 299 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/reify_Lambda_plugin.cmxs
  • 299 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/reify_Lambda_plugin.cmxs
  • 277 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/SubstI.vo
  • 266 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Hoare/LogicTac.vo
  • 249 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Cancel/RtacDemo.vo
  • 240 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Views/ProdView.vo
  • 232 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/ExprUnify_simple.vo
  • 224 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/RewriteRelations.vo
  • 223 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/Expr.vo
  • 221 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/MTypes/ModularTypes.vo
  • 219 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/ExprSubstitute.vo
  • 217 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/ExprI.vo
  • 211 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/Ptrns.vo
  • 192 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Hoare/ILogicFunc.vo
  • 189 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Cancel/MonoidSyntaxWithConst.vo
  • 172 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/AppN.vo
  • 171 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/TypesI.vo
  • 167 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Cancel/MonoidSyntaxSimple.vo
  • 164 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Reduce.vo
  • 163 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Cancel/MonoidSyntaxNoDec.vo
  • 160 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lemma.vo
  • 158 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/AutoRewrite/QuantPullRtac.vo
  • 148 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/CoreK.vo
  • 147 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/RunOnGoals_list.vo
  • 141 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/EApply.vo
  • 136 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/ExprUnify_common.vo
  • 135 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/ExprCore.vo
  • 134 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/Rtac.vo
  • 133 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/LemmaApply.vo
  • 129 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Cancel/MonoidSyntaxModular.vo
  • 128 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/ExprTac.vo
  • 124 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/IsSolved.vo
  • 121 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/RTac/Demo.vo
  • 116 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/syms/SymOneOf.vo
  • 111 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Simple/Simple.vo
  • 101 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Assumption.vo
  • 94 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/SubstituteI.vo
  • 92 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Intro.vo
  • 88 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Views/ApplicativeView.vo
  • 88 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Instantiate.vo
  • 87 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Views/Ptrns.vo
  • 85 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/reify_Lambda_plugin.cma
  • 85 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/reify_Lambda_plugin.cma
  • 84 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Views/NatView.vo
  • 82 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/ExprProp.vo
  • 81 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/VariablesI.vo
  • 75 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Views/ListView.vo
  • 75 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Views/Ptrns2.vo
  • 70 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Views/FuncView.vo
  • 69 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/TypedFoldApp.vo
  • 68 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Hoare/ILogic.vo
  • 68 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/RunOnGoals.vo
  • 67 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/AutoRewrite/DemoQuantPullRtac.vo
  • 67 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/AbsAppI.vo
  • 65 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Simplify.vo
  • 64 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/VarsToUVars.vo
  • 62 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Util/ListMapT.vo
  • 61 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/MTypes/BaseType.vo
  • 61 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Views/EqView.vo
  • 61 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/EnvI.vo
  • 60 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Auto.vo
  • 58 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Interface.vo
  • 58 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/ExprVariables.vo
  • 57 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Views/StringView.vo
  • 57 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/MTypes/GenericTypes.vo
  • 56 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/StrongFoldApp.vo
  • 56 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Views/BoolView.vo
  • 55 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/ExprDAs.vo
  • 55 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/ExprDI.vo
  • 55 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/TypedFoldEager.vo
  • 55 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/syms/SymPolyEnv.vo
  • 53 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/RTac.vo
  • 53 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/SolveK.vo
  • 52 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/First.vo
  • 52 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Instantiate.vo
  • 51 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/FoldApp.vo
  • 51 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/OpenT.vo
  • 51 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/ExprD.vo
  • 50 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Rec.vo
  • 49 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Solve.vo
  • 49 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/ExprSem.vo
  • 48 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Views/View.vo
  • 48 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/runTacK.vo
  • 48 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Repeat.vo
  • 46 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Simple/SimpleReify.vo
  • 46 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Simple/SimpleExt.vo
  • 46 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/TypedFoldLazy.vo
  • 46 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/IdtacK.vo
  • 45 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/ThenK.vo
  • 45 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/syms/SymEnv.vo
  • 45 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Then.vo
  • 45 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Util/Quant.vo
  • 45 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Hoare/ImpMetaTheory.vo
  • 45 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Apply.vo
  • 44 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Try.vo
  • 44 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/UnifyI.vo
  • 44 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/Lemma.vo
  • 43 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/AtGoal.vo
  • 43 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Util/HListBuild.vo
  • 43 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Idtac.vo
  • 42 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/RTac/Fail.vo
  • 42 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Hoare/Imp.vo
  • 41 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Reify/ModularReify.vo
  • 41 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Hoare/Tests.vo
  • 41 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Simple/FoldTest.vo
  • 41 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/CtxLogic.vo
  • 39 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/Reify.vo
  • 38 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Lambda/ExprUnify.vo
  • 38 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Reify/Patterns.vo
  • 37 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Reify/Reify.vo
  • 36 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/MTypes/ProdType.vo
  • 35 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Views/ViewSumN.vo
  • 33 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/MTypes/ListType.vo
  • 32 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/syms/SymProd.vo
  • 31 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/SymI.vo
  • 29 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Util/Nat.vo
  • 29 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Simple.vo
  • 29 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Util/Iteration.vo
  • 28 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/MTypes/TSyms.vo
  • 28 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/AutoRewrite/DemoQuantPullLtac.vo
  • 27 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Views/ViewSum.vo
  • 27 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Generic.vo
  • 24 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/syms/SymSum.vo
  • 23 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/syms/SymSimple.vo
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Views/TypeView.vo
  • 19 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Util/Compat.vo
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Util/Approx.vo
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/Util/Forwardy.vo
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Cancel/LtacDemo.vo
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/reify_Lambda_shell.cmi
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/MirrorCore/reify_Lambda_shell.cmi
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/McExamples/Cancel/Monoid.vo

Uninstall 🧹

Command
opam remove -y coq-mirror-core.1.0.1
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣