« Up

kami 0.0.3-rv32i 9 m 0 s 🏆

Context

# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-threads          base
base-unix             base
conf-gmp              4           Virtual package relying on a GMP lib system installation
coq                   8.18.0      The Coq Proof Assistant
coq-core              8.18.0      The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib            8.18.0      The Coq Proof Assistant -- Standard Library
coqide-server         8.18.0      The Coq Proof Assistant, XML protocol server
dune                  3.13.0      Fast, portable, and opinionated build system
ocaml                 4.14.0      The OCaml compiler (virtual package)
ocaml-base-compiler   4.14.0      Official release 4.14.0
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"
authors: [
  "Massachusetts Institute of Technology"
  "Kevix"
  "SiFive"
]
maintainer: "Jason Gross <jgross@mit.edu>"
homepage: "https://github.com/mit-plv/kami"
bug-reports: "https://github.com/mit-plv/kami/issues"
license: "MIT"
build: [
  [make "-j%{jobs}%" "EXTERNAL_DEPENDENCIES=1" "coq"]
]
install: [make "EXTERNAL_DEPENDENCIES=1" "install"]
depends: [
  "coq" {>= "8.15~"}
  "coq-riscv" {= "0.0.4"}
]
dev-repo: "git+https://github.com/mit-plv/kami.git"
synopsis: "A work-in-progress language and compiler for verified low-level programming"
tags: ["logpath:kami"]
url {
  src: "https://github.com/mit-plv/kami/archive/refs/tags/v0.0.3.tar.gz"
  checksum: "sha512=c76f047b4ade255ce22d1a25a702e69a9ae213e50b7cf3f754c32a80e3fb38ec0f4dda6217e9f34176033f6079efb0ab91b74d3e96f377c65f870f03b8d43a9d"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-kami.0.0.3-rv32i coq.8.18.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; timeout 4h opam install -y --deps-only coq-kami.0.0.3-rv32i coq.8.18.0
Return code
0
Duration
15 m 0 s

Install 🚀

Command
opam list; echo; timeout 4h opam install -y -v coq-kami.0.0.3-rv32i coq.8.18.0
Return code
0
Duration
9 m 0 s

Installation size

Total: 63 M

  • 16 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFDInl.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDecInl.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/FMap.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFInl.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/FifoCorrect.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/InlineFacts.vo
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulNormal2.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulNormal1.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker3.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker2.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker1.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulReport.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulInit.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerInit.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmPeterson2.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmPeterson1.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmDekker2.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmDekker1.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmHanoi.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBsort.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmFact.glob
  • 939 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmGcd.glob
  • 927 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Word.vo
  • 922 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Word.glob
  • 825 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/SimpleFifoCorrect.vo
  • 699 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Multiplier64.vo
  • 685 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Multiplier32.vo
  • 624 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/SemFacts.vo
  • 610 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/ModularFacts.vo
  • 588 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/InDepthTutorial.vo
  • 555 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Divider64.vo
  • 538 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Divider32.vo
  • 475 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/SCMMInv.vo
  • 403 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/SCMMInl.vo
  • 373 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Renaming.vo
  • 331 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/FMap.glob
  • 330 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Syntax.vo
  • 310 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Decomposition.vo
  • 308 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/RefinementFacts.vo
  • 273 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcThreeStage.vo
  • 246 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Specialize.vo
  • 244 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/PartialInlineFacts.glob
  • 241 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Multiplier64.glob
  • 241 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Multiplier32.glob
  • 239 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/StepDet.vo
  • 237 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Semantics.vo
  • 224 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Divider64.glob
  • 223 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Divider32.glob
  • 219 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Wf.vo
  • 212 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerInit.vo
  • 210 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker3.vo
  • 210 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker2.vo
  • 210 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker1.vo
  • 208 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcThreeStage.glob
  • 203 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/PartialInlineFacts.vo
  • 202 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulReport.vo
  • 202 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulInit.vo
  • 202 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/SC.vo
  • 199 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/InlineFacts.glob
  • 199 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulNormal2.vo
  • 198 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulNormal1.vo
  • 198 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Word.v
  • 195 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/SemFacts.glob
  • 194 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmHanoi.vo
  • 192 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBsort.vo
  • 190 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmDekker2.vo
  • 190 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmDekker1.vo
  • 189 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmPeterson1.vo
  • 189 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmPeterson2.vo
  • 188 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Decomposition.glob
  • 188 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmGcd.vo
  • 188 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmFact.vo
  • 161 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Syntax.glob
  • 157 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Tactics.vo
  • 157 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/RefinementFacts.glob
  • 146 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Semantics.glob
  • 144 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Specialize.glob
  • 143 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Renaming.glob
  • 141 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/ModuleBoundEx.vo
  • 139 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcMemCorrect.vo
  • 139 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFetchDecode.vo
  • 134 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcThreeStInv.glob
  • 134 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDec.vo
  • 129 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDecInv.vo
  • 126 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Duplicate.glob
  • 124 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32Pgm.vo
  • 121 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/SC.glob
  • 117 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/ModuleBoundEx.glob
  • 114 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32.vo
  • 105 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32.glob
  • 102 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Label.vo
  • 102 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFDCorrect.vo
  • 97 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/NatLib.vo
  • 96 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcThreeStInv.vo
  • 96 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/CommonTactics.vo
  • 93 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFetch.vo
  • 91 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Duplicate.vo
  • 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/FMap.v
  • 86 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/FifoCorrect.glob
  • 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFetchDecode.glob
  • 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/StringAsList.vo
  • 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcThreeStDec.vo
  • 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/ilist.vo
  • 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDec.glob
  • 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/ModularFacts.glob
  • 68 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32Pgm.glob
  • 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/InlineFacts.v
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Notations.vo
  • 63 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Tutorial.vo
  • 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/SimpleFifoCorrect.glob
  • 60 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ext/BSyntax.vo
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/StepDet.glob
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Tactics.glob
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/SemFacts.v
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Wf.glob
  • 56 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/PartialInlineFacts.v
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/InDepthTutorial.glob
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/ModuleBound.vo
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/NatLib.glob
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Decomposition.v
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFetch.glob
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Struct.vo
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Indexer.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Btb.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Multiplier64.v
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Multiplier32.v
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Divider64.v
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Divider32.v
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDecSC.vo
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/StringEq.vo
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcThreeStDec.glob
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/ListSupport.vo
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Renaming.v
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/RefinementFacts.v
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Fifo.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Label.glob
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFCorrect.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDecInv.glob
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/StringAsOT.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/PrimBram.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/WordSupport.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Syntax.v
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Specialize.v
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/PrimFifo.vo
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/MemAsync.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcMemCorrect.glob
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/OneEltFifo.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcThreeStInv.v
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/NativeFifo.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ext/BSyntax.glob
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Synthesize.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFourStDec.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/StringStringAsOT.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/StringAsList.glob
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Semantics.v
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFDInv.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/ModuleBoundEx.v
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/ModuleBound.glob
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Inline.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFInv.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Tactics.v
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ext/Extraction.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/RegFile.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/ilist.glob
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/FifoCorrect.v
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Names.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Duplicate.v
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/ListSupport.glob
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcThreeStage.v
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFDCorrect.glob
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Substitute.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcThreeStInl.vo
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDecSCN.vo
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Indexer.glob
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Reflection.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/StringStringAsOT.glob
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32PgmExt.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFourStDec.glob
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Nlia.vo
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/MemTypes.vo
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Concat.vo
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Kami.vo
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/N_Z_nat_conversions.vo
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Misc.vo
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDecSC.glob
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmPeterson2.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmPeterson1.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulReport.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulNormal2.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulNormal1.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulInit.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmHanoi.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmGcd.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmFact.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmDekker2.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmDekker1.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBsort.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker3.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker2.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker1.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerInit.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Notations.glob
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/SC.v
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32.v
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/WordSupport.glob
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFDInv.glob
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32Pgm.v
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/VectorFacts.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Fifo.glob
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/SimpleFifoCorrect.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Wf.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/ModularFacts.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Btb.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/InDepthTutorial.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/StepDet.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/SCMMInv.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFCorrect.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Synthesize.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/PrimFifo.glob
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Substitute.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/NativeFifo.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/OneEltFifo.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/DepEq.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/VectorFacts.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Struct.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/PrimBram.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDecInv.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Inline.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Label.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDecSC.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFInv.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/StringAsOT.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFetchDecode.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Notations.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcThreeStInl.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/StringEq.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcThreeStDec.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/NatLib.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/ModuleBound.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/ilist.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/MemAsync.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/StringAsList.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcMemCorrect.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/FinNotations.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDec.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/CommonTactics.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFetch.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ext/BSyntax.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Tutorial.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/DepEqNat.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFDCorrect.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFDInl.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/CommonTactics.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Indexer.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/DepEq.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Concat.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFDInv.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Reflection.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/RegFile.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFourStDec.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/ListSupport.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/WordSupport.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/DepEqNat.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFInl.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/StringAsOT.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Nlia.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/N_Z_nat_conversions.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFCorrect.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/SCMMInv.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/BasicLogic.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ext/Extraction.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Misc.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Tutorial.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFInv.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Struct.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/StringStringAsOT.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDecSCN.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/BasicLogic.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Names.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/PrimFifo.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Inline.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Synthesize.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/VectorFacts.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Substitute.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcThreeStInl.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/NativeFifo.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/SCMMInl.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Btb.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/PrimBram.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/StringEq.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Fifo.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/MemAsync.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/OneEltFifo.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/Names.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFDInl.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Concat.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ext/Extraction.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/MemTypes.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDecInl.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Reflection.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcFInl.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Nlia.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/DepEq.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/DepEqNat.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/RegFile.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/N_Z_nat_conversions.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDecSCN.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/Misc.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/SCMMInl.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/FinNotations.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32PgmExt.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/BasicLogic.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/ProcDecInl.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/MemTypes.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Kami.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Ex/IsaRv32PgmExt.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Kami.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Kami/Lib/FinNotations.v

Uninstall 🧹

Command
opam remove -y coq-kami.0.0.3-rv32i
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣